Coinductive well-foundedness

Iosif Petrakis

REVIEW 2 major objections 3 minor 30 references

Coinductive well-foundedness

T0 review · 2 major / 3 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read An inhabited complemented subset of the natural numbers has a least element exactly when it is downset located, proved by a coinductive descent principle in minimal logic.

desk verdict Genuinely new positive least-number principle for complemented subsets, but the advertised 'within minimal logic' proof is overstated: DWF_N is an extra premise in MIN, and Cor 5.5(iii) uses disjunctive syllogism. read the letter →

arxiv 2506.16433 v2 pith:5SZQDXQA submitted 2025-06-19 math.LO

Iosif Petrakis This is my paper · ORCID

classification math.LO MSC 03F6503B20

keywords coinductivewell-foundednessleastnumberprinciplecomplementedsubsetsminimallogicdownsetlocateddescentnaturalnumbersconstructivemathematics

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to make the least number principle constructive by replacing the classical “every nonempty subset of $\mathbb{N}$ has a least element” with a positive statement about complemented subsets: an inhabited complemented subset $A$ has a least element if and only if it is downset located. The work is carried out in minimal logic, with the coinductive descent scheme $\mathrm{DWF}_{\mathbb{N}}$ doing the work that the classical principle does by choosing a minimum. A sympathetic reader should care because the equivalence turns an existence assertion into a checkable local condition, and the proof of the “if” direction is a terminating descent algorithm: from any prover in $A$, either a smaller prover exists or the current element is least. The same scheme is then generalised to arbitrary sets with an inequality and an order, where it yields a coinductive notion of well-foundedness.

What carries the argument

The central object is the scheme $\mathrm{DWF}_{\mathbb{N}}$, a coinductive, existential counterpart to strong induction on $\mathbb{N}$. It states that if a predicate $Q$ is inhabited and every $x$ satisfying $Q$ either satisfies $P$ or has a smaller $y$ satisfying $Q$, then some $x$ satisfies $P$. This scheme carries the argument by encoding a descent algorithm: start at a witness of $Q$, and whenever the current element does not satisfy $P$, move to a strictly smaller witness of $Q$, so after finitely many steps a $P$-witness is reached. Complemented subsets $A=(A_1,A_0)$ supply the positive vocabulary: elements of $A_1$ are provers, elements of $A_0$ refuters, and downset locatedness is exactly the local hypothesis that lets $\mathrm{DWF}_{\mathbb{N}}$ start the descent from any chosen prover.

What would settle it

Build a Kripke model of minimal arithmetic containing a complemented subset $A=(A_1,A_0)$ with a prover $a_1>0$ such that downset locatedness holds at every stage but no element is least across all stages; if $\mathrm{DWF}_{\mathbb{N}}$ is valid in the model, the theorem's conclusion would fail, and such a model would show exactly where the descent scheme is doing the work.

Watch

Extended reading notes

Core claim

The central claim is Theorem 5.6: for a complemented subset $A=(A_1,A_0)$ of $\mathbb{N}$ with $a_1\in A_1$ and $a_1>0$, $A$ has a least element if and only if it is downset located. Downset located means that for every prover $x\in A_1$, either the whole downset $D_A(x)=\{y\in A_1\cup A_0\mid y<x\}$ is contained in the refuter part $A_0$, or some element of the downset is itself a prover. Under this condition, the descent scheme $\mathrm{DWF}_{\mathbb{N}}$ produces the least element: starting from $a_1$, if the downset is not entirely in $A_0$, a smaller prover is found, and the scheme guarantees the search terminates. Conversely, a least element forces the disjunction at every prover. The paper also states the constructive least number principle CLNP for every inhabited complemented subset of $\mathbb{N}$, notes that classically it is equivalent to the ordinary least number principle, and proves it within minimal logic.

Load-bearing premise

The load-bearing premise is that the descent scheme $\mathrm{DWF}_{\mathbb{N}}$ is a valid principle: termination of the descent is delegated to it, and its constructive justification, along with the case $0\in A_1$, invokes the ex-falso rule that a contradiction proves anything.

Editorial extensions

If this is right

The classical least number principle becomes a constructively valid equivalence: an inhabited complemented subset of $\mathbb{N}$ has a least element exactly when it is downset located, so the existence of a least element can be verified locally.
The descent scheme $\mathrm{DWF}_{\mathbb{N}}$ gives a terminating algorithm for finding the least element: from any prover, each non-terminal step produces a strictly smaller prover, bounding the search by the initial element.
Arithmetic facts classically proved by choosing a least counterexample, such as the existence of a prime divisor of a composite number, can be proved in minimal logic using $\mathrm{DWF}_{\mathbb{N}}$ instead of the least number principle.
The generalisation to arbitrary sets with an inequality and an order yields D-well-founded sets, and these are closed under images, substructures, products, sums, lexicographic products, and indexed sums, giving a toolbox for coinductive well-foundedness.
Within $\mathrm{DWF}_{\mathbb{N}}$, every sequence in $\mathbb{N}$ has a term no larger than its successor; classically the principle is equivalent to the absence of infinite descending sequences.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A testable extension: the same equivalence may hold for any dichotomous, strong D-well-founded order, with downset located defined using that order's provers and refuters; checking it on a lexicographic product would show whether the descent principle composes as cleanly as the closure theorems suggest.
The proof suggests the computational content of the least number principle is a bounded linear search rather than a global minimum oracle: Theorem 5.6 can be read as saying that a starting prover plus downset locatedness is enough to compute the least element in at most $a_1+1$ descent steps.
Because the paper's constructive justification of $\mathrm{DWF}_{\mathbb{N}}$ passes through strong induction and an ex-falso step, a natural next question is whether CLNP can be derived from a weaker descent principle; a realizability model separating the two would locate the exact logical strength needed.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: there's a real idea here—a positive, negation-free least-number principle for complemented subsets of N, with a coinductive descent principle doing the work—but the advertised 'minimal logic' proof is not what the paper actually delivers. The main theorem is a conditional in MIN + DWF_N, and one case of the full CLNP uses a disjunctive syllogism that minimal logic doesn't allow.

The genuinely new bits: DWF_N (a descent scheme: if Q is inhabited and every Q point either satisfies P or has a smaller Q point, then P is inhabited) and the equivalence in Theorem 5.6 that a complemented subset with a1>0 has a least element iff it is downset located. That's a clean, positive counterpart to LNP, in the same spirit as locatedness for suprema. Section 6 generalizes to D-well-founded sets and gives closure properties (subsets, product, sum, Sigma-type) that look correct in the intended semi-formal framework. The analogy is apt and the positive formulation is a real improvement over negated formulations.

The soft spots are the logical hygiene claims. The stress-test is right: Proposition 3.1(i) proves DWF_N from strong induction @WF_N, and the paper itself notes IND_N → @WF_N needs EFQ at the base case (the vacuous proof of ∀y<0 P(y) uses K_N → P(y), which is exactly ex falso). So within MIN, DWF_N is an extra axiom, not a consequence. The formal proof of (ii)→(i) in Theorem 5.6 invokes DWF_N directly, so the theorem is proved in MIN + DWF_N, not MIN. Separately, Corollary 5.5(iii) derives x∈A0 from x∈A1∨x∈A0 and ¬(x∈A1); that's disjunctive syllogism, invalid in minimal logic. The full CLNP covering the case 0∈A1 leans on this. So the abstract overstates the logic.

None of this kills the mathematical content. If DWF_N is accepted as a primitive coinductive principle (or as a consequence of strong induction in intuitionistic logic), the equivalence is solid. The paper would be improved by stating Theorem 5.6 as 'within MIN plus DWF_N', by flagging Corollary 5.5(iii) as requiring intuitionistic (or classical) logic, and by making the dependence on earlier BST works explicit enough that a referee can check the key steps without reading the habilitationsschrift.

Who should read it: constructive mathematicians and proof theorists interested in descent principles. It deserves a serious referee; the logic claims need revision, but the core idea is worthy. I'd send it to review with a request to fix the minimal-logic framing.

Referee Report

2 major / 3 minor

Summary. The paper introduces a coinductive well-foundedness scheme DWF_N for the natural numbers, a 'dual' to induction whose conclusion is existential and whose hypothesis allows a backward descent step. It then states and proves CLNP: an inhabited complemented subset A of N has a least element if and only if it is downset located. The paper also generalizes DWF_N to D-well-founded sets, proves several preservation properties (embeddings, restrictions, products, coproducts, lexicographic products, and Sigma-sets), and presents a case study on divisibility by primes. The central claimed logical strength is that CLNP is proved within minimal logic, with DWF_N as a constructive descent principle.

Significance. If the logical claims are corrected, the paper makes a useful contribution. DWF_N is a clearly described, algorithmically meaningful descent scheme, and the equivalence between least-element existence and downset locatedness for complemented subsets is a genuine positive reformulation of the classical least number principle. The generalization to D-well-founded sets, with preservation under products, sums, lexicographic products, and Sigma-sets, is a coherent and instructive development. The paper is, however, not machine-checked, and its central 'within minimal logic' claim is not supported as stated; the results are best read as theorems of minimal logic plus the explicitly named scheme DWF_N together with certain disjunctive-syllogism instances.

major comments (2)

[Abstract; Section 3, Proposition 3.1; Section 5, Theorem 5.6] The claim that CLNP (Theorem 5.6) is proved 'within minimal logic' is not supported as stated. The formal direction (ii) to (i) invokes DWF_N directly ('Hence, by DWF_N there is x...'), and DWF_N is not derived from the stated minimal-logic axioms. Proposition 3.1(i) derives DWF_N only from the strong induction scheme @WF_N, and the paper itself notes that IND_N to @WF_N requires EFQ at the base case. Theorem 5.6 is therefore a theorem of MIN plus the additional scheme DWF_N, not of MIN alone. Please either supply a derivation of DWF_N within MIN, or state the abstract and theorem with the explicit extra axiom DWF_N.
[Section 5, Corollary 5.5(iii)] The proof of Corollary 5.5(iii), which is used for the '0 in A1' case of CLNP, is not minimal. From x in A1 or x in A0 and the derived not(x in A1), the proof concludes x in A0. This is a disjunctive syllogism, which is not derivable in minimal logic without an explosion principle. Since the full if-and-only-if statement of CLNP covers inhabited complemented subsets with 0 in A1, this is a second place where the 'within MIN' claim requires a non-minimal step.

minor comments (3)

[Section 2, Proposition 2.1] Proposition 2.1 is labelled (MIN), but its step from 0 in A_P, i.e. (0=1) or (0=0 and P), together with 0 not equal to 1, to P is again a disjunctive syllogism. Since this proposition is not used in the proof of the main theorem, it should be restated with the needed assumption or explicitly relegated to a remark about non-minimal logical strength.
[Abstract and throughout] There are several typographical errors that should be corrected in a revision, including 'Generealising' in the abstract, 'anrgument' in Section 3, 'tohether' and 'ther is' and 'exluded' in Section 5, and 'disjumction' in Section 6.
[Section 5, formal proof of Theorem 5.6] The informal proof of (ii) to (i) describes a descent of at most a1+1 steps, but the formal proof delegates termination to DWF_N. It would improve clarity to state explicitly that DWF_N is being used as a primitive descent axiom in this proof, rather than as a consequence of the minimal-logic framework.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: CLNP is a genuine derivation from the explicitly stated DWF_N scheme.

full rationale

The paper's central derivation, Theorem 5.6, proves CLNP from DWF_N. DWF_N is introduced in Section 3 as a separate coinductive scheme, and Proposition 3.1(i) derives DWF_N from strong induction @WF_N. Neither of these inputs is the target statement CLNP, and CLNP is not assumed in the proof of DWF_N. Downset locatedness (Definition 5.1) and least element (Definition 5.4) are defined independently, so the equivalence is not true by definition. No parameter is fitted to data and no 'prediction' is a renamed input. The paper's reliance on the author's earlier Bishop Set Theory framework [20,22,24] and complemented-subset work [9,11,12,25] is background infrastructure; those works are not claimed to contain CLNP, and no load-bearing argument reduces to a self-citation. The only substantive caveat is that the abstract's 'within minimal logic' claim is sensitive to the status of DWF_N: Proposition 3.1(i) obtains DWF_N from strong induction, and the paper itself notes that IND_N -> @WF_N requires EFQ at the base case; moreover the 0 in A1 case of CLNP uses Corollary 5.5(iii)'s disjunctive syllogism. That is a correctness or scope concern about the exact logical system, not a circularity, because the proof is conditional on DWF_N rather than on CLNP itself.

Assumptions & free parameters 0 free parameters · 5 assumptions · 2 invented entities

No free parameters: the paper is pure mathematics with no numerical fits. The axioms are the standard BISH and Peano background (section 2), the order properties (I1)-(I5), the author-developed BST framework of [20, 22, 24] in which everything is formalized, plus two assumptions specific to the minimal-logic claims: DWF_N used as an unproved premise (provable in INT via strong induction) and EFQ-like disjunctive syllogism steps in Prop 2.1 and Cor 5.5(iii). The new notions (DWF_N, downset locatedness, D-wfs) are definitions and derived principles, not empirical postulates.

assumptions (5)

standard math Peano axioms (Peano1-3) including induction scheme IND_N; Bishop equality and decidable apartness axioms for N
Section 2 sets out N with 0 not equal 1, successor embedding, induction, and decidable apartness; all later results are built on these.
standard math Order properties (I1)-(I5) of less-than on N: dichotomy, transitivity, x<y implies x not equal y, weak-negated x<y implies x at least y
Stated in section 2 as 'expected properties'; used in Cor 5.5, Prop 3.1(iii), Example 5.2 and Theorem 5.6.
domain assumption Bishop Set Theory (BST) as developed in [20, 22, 24]: assignment routines, dependent assignment routines, extensional formulas, separation scheme
The paper says it works within BST and refers to the author's prior works for all BST notions; Section 6's family and Sigma-set machinery depends on this framework.
ad hoc to paper DWF_N: (exists x Q(x)) and forall x (Q(x) implies P(x) or exists y<x Q(y)) implies exists x P(x), for extensional Q and P
Introduced in section 3 as the main principle and used in the (ii) to (i) direction of Theorem 5.6. It is provable in INT from strong induction (Prop 3.1(i)), but in the minimal-logic reading it is an unproved extra premise.
ad hoc to paper EFQ_N (K_N implies Q for arbitrary Q) inside the 'within MIN' proofs of Prop 2.1 and Cor 5.5(iii)
Both proofs close a case by a disjunctive syllogism from A or B and A implies K_N to B, which is not a rule of minimal logic; Example 5.2(i) explicitly flags EFQ usage elsewhere, showing the framework allows it only when stated.

invented entities (2)

DWF_N, the coinductive well-foundedness scheme for N independent evidence
purpose: Engine for the (ii) to (i) direction of CLNP and the base instance of D-well-foundedness
Provably derived from strong induction in INT (Prop 3.1(i)), so its validity is anchored to the standard induction principle independently of this paper; it also yields a checkable consequence, namely that every sequence has a local minimum (Prop 3.1(iii)).
D-well-founded sets (D-wfs)
purpose: Generalization of DWF_N to arbitrary sets with inequality and relation; closure properties proved in section 6
A new definition whose content is the internal closure theorems (Propositions 6.3 to 6.7); there is no falsifiable handle outside the paper, short of a machine-checked formalization, which is not provided.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Coinductive well-foundedness." pith.science (2026). https://pith.science/paper/5SZQDXQA

@misc{pith2026250616433,
  author       = {Pith},
  title        = {Pith review of: Coinductive well-foundedness},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5SZQDXQA}},
  note         = {Machine review of arXiv:2506.16433}
}

abstract

We introduce a coinductive version of the well-foundedness of N that is used in our proof within minimal logic of the constructive counterpart CLNP to the standard least number principle LNP. According to CLNP, an inhabited complemented subset of N has a least element if and only if it is downset located. The use of complemented subsets of N in the formulation of CLNP, instead of subsets of N, allows a positive approach to the subject that avoids negation. Generalising the coinductive well-foundedness of N, we define $\exists$-well-founded sets and we prove their fundamental properties.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 9 canonical work pages

[1]

Aczel, M

P. Aczel, M. Rathjen:Notes on Constructive Set Theory, Report No. 40, 2000/2001, ISSN 1103- 467X. Institut Mittag-Leffler. 14

work page 2000
[2]

Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967

E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967

1967
[3]

Bishop, H

E. Bishop, H. Cheng:Constructive Measure Theory, Mem. Amer. Math. Soc. 116, 1972

1972
[4]

Bishop, D

E. Bishop, D. S. Bridges: Constructive Analysis, Grundlehren der math. Wissenschaften 279, Springer-Verlag, Heidelberg-Berlin-New York, 1985

1985
[5]

D. S. Bridges, F. Richman:Varieties of Constructive Mathematics, Cambridge University Press, 1987

1987
[6]

D. S. Bridges and L. S. Vîţă:Techniques of Constructive Analysis, in: Universitext, Springer, New York, 2006

work page 2006
[7]

Coquand, H

T. Coquand, H. Lombardi, S. Neuwirth: Constructive theory of ordinals, in M. Benini et. al. (Eds.) Mathematics for Computation - M4C, World Scientific, 2023, 287–318

work page 2023
[8]

Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020

H. Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020

arXiv 2020

Show all 30 references

[9]

N. Köpp, I. Petrakis: Strong negation in the theory of computable functionals TCF, Logical Methods in Computer Science, Volume 21, Issue 2 - https://doi.org/10.46298/lmcs-21(2:1)2025

2025 doi
[10]

Mines, F

R. Mines, F. Richman, W. Ruitenburg:A course in constructive algebra, Springer Science` Busi- ness Media New York, 1988

1988
[11]

Misselbeck-Wessel, I

D. Misselbeck-Wessel, I. Petrakis: Complemented subsets and Boolean-valued, partial functions, Computability, vol. 13, no. 3-4, 2024, pp. 399–431

2024
[12]

Misselbeck-Wessel, I

D. Misselbeck-Wessel, I. Petrakis: Constructive Stone representations for separated swap and Boolean algebras, submitted, 2025

2025
[13]

Myhill: Constructive Set Theory, J

J. Myhill: Constructive Set Theory, J. Symbolic Logic 40, 1975, 347–382

1975
[14]

Palmgren: Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic 163, 2012, 1384–1399

E. Palmgren: Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets, Annals of Pure and Applied Logic 163, 2012, 1384–1399

2012
[15]

Palmgren: Bishop-style constructive mathematics in type theory - A tutorial, Slides, 2013

E. Palmgren: Bishop-style constructive mathematics in type theory - A tutorial, Slides, 2013. http://staff.math.su.se/palmgren/

2013
[16]

Palmgren: Lecture Notes on Type Theory, manuscript, 2014

E. Palmgren: Lecture Notes on Type Theory, manuscript, 2014

2014
[17]

Palmgren, O

E. Palmgren, O. Wilander: Constructing categories and setoids of setoids in type theory, Logical Methods in Computer Science. 10 (2014), Issue 3, paper 25

2014
[18]

Palmgren: Constructions of categories of setoids from proof-irrelevant families, Archive for Mathematical Logic 56, 2017, 51–66

E. Palmgren: Constructions of categories of setoids from proof-irrelevant families, Archive for Mathematical Logic 56, 2017, 51–66

2017
[19]

Palmgren: From type theory to setoids and back, preprint, 2019

E. Palmgren: From type theory to setoids and back, preprint, 2019

2019
[20]

Petrakis: Families of Sets in Bishop Set Theory, Habilitationsschrift, LMU, Munich, 2020, available athttps://www.mathematik.uni-muenchen.de/~petrakis/content/Theses.php

I. Petrakis: Families of Sets in Bishop Set Theory, Habilitationsschrift, LMU, Munich, 2020, available athttps://www.mathematik.uni-muenchen.de/~petrakis/content/Theses.php

2020
[21]

Petrakis: Constructive Combinatorics of Dickson’s Lemma, 2022, available at https://arxiv.org/abs/2204.11298v1

I. Petrakis: Constructive Combinatorics of Dickson’s Lemma, 2022, available at https://arxiv.org/abs/2204.11298v1

2022 arXiv
[22]

Petrakis: Proof-relevance in Bishop-style constructive mathematics, Mathematical Structures in Computer Science, Volume 32, Issue 1, 2022, 1–43

I. Petrakis: Proof-relevance in Bishop-style constructive mathematics, Mathematical Structures in Computer Science, Volume 32, Issue 1, 2022, 1–43. doi:10.1017/S0960129522000159

2022 doi
[23]

Petrakis: Categories with dependent arrows, arXiv:2303.14754v1, 2023

I. Petrakis: Categories with dependent arrows, arXiv:2303.14754v1, 2023

2023 arXiv
[24]

Petrakis: Sets Completely Separated by Functions in Bishop Set Theory, Notre Dame Journal of Formal Logic, 65(2): 151-180 (May 2024) DOI: 10.1215/00294527-2024-0010

I. Petrakis: Sets Completely Separated by Functions in Bishop Set Theory, Notre Dame Journal of Formal Logic, 65(2): 151-180 (May 2024) DOI: 10.1215/00294527-2024-0010. 15

2024 doi
[25]

Petrakis, D

I. Petrakis, D. Wessel: Algebras of complemented subsets, in U. Berger et.al. (Eds):Revolutions and Revelations in Computability, CiE 2022, Lecture Notes in Computer Science 13359, Springer, 2022, 246–258

2022
[26]

A. M. Pitts: Categorical logic, in S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (Eds.)Handbook of Logic in Computer Science, Vol. 5, Clarendon Press, Oxford, 2000, 39–128

2000
[27]

Richman, G

F. Richman, G. Stolzenberg: Well Quasi-Ordered Sets, Advances in Mathematics 97, 145–153, 1993

1993
[28]

Shulman: Affine logic for constructive mathematics, The Bulletin of Symbolic Logic, Volume 28, Number 3, 2022, 327–386

M. Shulman: Affine logic for constructive mathematics, The Bulletin of Symbolic Logic, Volume 28, Number 3, 2022, 327–386

2022
[29]

A. S. Troelstra, D. van Dalen: Constructivisim in Mathematics, An Introduction, Volume 1, North-Holland, 1988

1988
[30]

The Univalent Foundations Program:Homotopy Type Theory: Univalent Foundations of Mathe- matics, Institute for Advanced Study, Princeton, 2013. 16

2013

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.

[1] [1]

Aczel, M

P. Aczel, M. Rathjen:Notes on Constructive Set Theory, Report No. 40, 2000/2001, ISSN 1103- 467X. Institut Mittag-Leffler. 14

work page 2000

[2] [2]

Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967

E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967

1967

[3] [3]

Bishop, H

E. Bishop, H. Cheng:Constructive Measure Theory, Mem. Amer. Math. Soc. 116, 1972

1972

[4] [4]

Bishop, D

E. Bishop, D. S. Bridges: Constructive Analysis, Grundlehren der math. Wissenschaften 279, Springer-Verlag, Heidelberg-Berlin-New York, 1985

1985

[5] [5]

D. S. Bridges, F. Richman:Varieties of Constructive Mathematics, Cambridge University Press, 1987

1987

[6] [6]

D. S. Bridges and L. S. Vîţă:Techniques of Constructive Analysis, in: Universitext, Springer, New York, 2006

work page 2006

[7] [7]

Coquand, H

T. Coquand, H. Lombardi, S. Neuwirth: Constructive theory of ordinals, in M. Benini et. al. (Eds.) Mathematics for Computation - M4C, World Scientific, 2023, 287–318

work page 2023

[8] [8]

Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020

H. Diener: Constructive Reverse Mathematics, arXiv:1804.05495, 2020

arXiv 2020