Pith. sign in

REVIEW 2 major objections 3 minor 1 cited by

Lifting countable to uncountable mathematics

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

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

Pith's one-line read The paper claims that recursive-counterexample proofs from countable mathematics lift directly to uncountable mathematics, so that the monotone convergence theorem for nets indexed by Baire space implies the strong comprehension axiom BOOT.

desk verdict The flagship lifting proof has a genuine directedness gap, but the paper is honest, contains new algebra and ring liftings, and deserves refereeing. read the letter →

arxiv 1908.05677 v4 pith:MXMDK2GJ submitted 2019-08-15 math.LO cs.LO

Sam Sanders This is my paper · ORCID
classification math.LOcs.LO MSC 03F3503D6503B3003D80
keywords higher-orderarithmeticnetsmonotoneconvergencetheoremcomprehensionaxiomsrecursivecounterexamplesuncountablemathematicsBairespacealgebraicclosures
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 is trying to establish that proofs originating in countable mathematics—recursive counterexamples and reversals that show a theorem implies a set-existence axiom—can be carried over to uncountable mathematics with little modification. The flagship result is that the monotone convergence theorem for increasing nets in $[0,1]$ indexed by Baire space implies a comprehension axiom called BOOT, which is far stronger than the arithmetical comprehension axiom obtained from the classical sequence version. The same template is applied to compactness of metric spaces, closed sets, a selection lemma for families indexed by Baire space, ordering and algebraic closure of fields, and maximal ideals of rings. A sympathetic reader should care because, if the transfer is sound, the boundary between countable and uncountable mathematics is not a proof-technical barrier: arguments about sequences can be recycled as arguments about nets.

What carries the argument

The load-bearing mechanism is the net constructed from finite sequences of elements of Baire space. Given a functional $Y^2$, the paper forms a directed set $D$ of finite sequences $w$ whose $Y$-values are pairwise distinct, ordered by subsequence, and on this set defines the net $c_w := \sum_{i<|w|} 2^{-Y(w(i))}$. Pairwise distinctness keeps $c_w$ inside $[0,2]$, so monotone convergence supplies a limit $c$; comparing $c_w$ with $c$ turns the statement 'some $f$ has $Y(f)=k$' into a universal condition on all sufficiently long $w$. The higher-order comprehension rule $\Delta\text{-}\mathrm{CA}$—an equivalence between an existential and a universal formula over Baire space yields a set of natural numbers—then converts that equivalence into the range set $\{k : \exists f (Y(f)=k)\}$. The same directed-set-plus-net pattern, with different finite-extension constructions, carries the metric-space and algebra lifts.

What would settle it

Let $Y(f)=0$ for every $f\in\mathbb{N}^{\mathbb{N}}$. Then condition (3.5) forces every finite sequence in $D$ to have at most one element, and two distinct singleton sequences have no common upper bound, so $D$ is not directed and $\mathrm{MCT}[0,1]^{\mathrm{net}}$ cannot be invoked. Checking whether the proof supplies a reduction from arbitrary $Y$ to an injective $Y$ settles whether the theorem is established as stated.

Watch

Extended reading notes

Core claim

The paper's central discovery is that replacing 'sequence' by 'net' and 'function' by 'functional' in certain reversals yields theorems about uncountable objects from essentially the same proof. Concretely, over $\mathrm{ACA}_0^\omega + \Delta\text{-}\mathrm{CA}$, the statement $\mathrm{MCT}[0,1]^{\mathrm{net}}$—every increasing net in the unit interval indexed by Baire space converges—implies BOOT, the comprehension axiom that from any type-two functional $Y$ one can form the set $\{n \in \mathbb{N} : \exists f \in \mathbb{N}^{\mathbb{N}} (Y(f,n)=0)\}$. The proof mirrors the classical recursive-counterexample argument for the sequence version: one builds an increasing net whose limit codes the range of $Y$, uses convergence to convert an existential statement into a universal one, and applies $\Delta\text{-}\mathrm{CA}$ to obtain the desired set. The paper also lifts analogous reversals for metric compactness, closed sets, the selection lemma, field ordering and algebraic closure, and ring ideals, and observes that increasing the index set to higher finite types yields still stronger range-comprehension axioms.

Load-bearing premise

The proof applies the monotone convergence theorem to the directed set of finite sequences with pairwise distinct $Y$-values; for a general functional $Y$ this set need not be directed—if $Y$ is constant, no two distinct singletons have an upper bound—so the argument as written depends on an injectivity condition on $Y$ that the paper states no reduction to.

Editorial extensions

If this is right

  • If the monotone convergence theorem holds for increasing nets indexed by Baire space, then BOOT follows (over $\mathrm{ACA}_0^\omega + \Delta\text{-}\mathrm{CA}$), so the range of any type-two functional exists.
  • Repeating the construction with nets indexed by $\mathbb{N}^{\mathbb{N}} \to \mathbb{N}$ yields the range of type-three functionals and hence a correspondingly stronger comprehension principle.
  • Heine-Borel or sequential compactness of a complete metric space over Baire space implies BOOT, and when total boundedness is given by an effective sequence, countable choice follows as well.
  • The higher-order versions of the selection lemma, ordering of formally real fields, existence and uniqueness of algebraic closures, and existence of maximal ideals in commutative rings over Baire space imply BOOT or separation of disjoint ranges of functionals, mirroring the countable reversals.
  • Because the lifted statements can be pushed to index sets of any finite type, the results scale beyond Baire space to any cardinality expressible in the language.

Reading between the lines

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

  • Beyond the paper, the directedness failure for constant functionals suggests that a fully general lifting would require a normalization step that quotients the index set by equality of functional values; proving such a reduction would remove the implicit injectivity assumption from the proof of the monotone-convergence result.
  • If the template is as systematic as the examples suggest, any second-order reversal whose proof only uses convergence of bounded increasing sequences should admit a net version over an arbitrary index set, provided the directed set can be defined; the algebra examples hint that finite-extension compactness arguments are the right tool.
  • The countable sub-fields that appear in the field-theory sections suggest a testable reading of the 'uncountable algebra' results: they may really be about countable sub-fields presented through uncountably many labels, and it is an open question whether the liftings survive when the fields are presented as sets of reals.
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.

Referee Report

2 major / 3 minor

Summary. This paper argues that recursive counterexamples and reversals from second-order (countable) reverse mathematics can be lifted, with minimal changes, to higher-order (uncountable) mathematics. The main showcase is Theorem 3.7: over ACA_0^omega + Delta-CA, the monotone convergence theorem for increasing nets in [0,1] indexed by Baire space implies BOOT, a strong comprehension axiom. Further sections lift proofs concerning compactness of metric spaces, closed sets, the Rado selection lemma, field orderings, algebraic closures, and maximal ideals. The paper is part of a larger project with companion papers [45,46] and emphasizes that no systematic meta-theorem is claimed.

Significance. If the proofs were complete, the paper would provide a substantial contribution: it gives a concrete transfer mechanism from countable to uncountable mathematics, identifies natural higher-order principles (BOOT, RANGE, SEP1), and shows that they are implied by standard uncountable theorems. The axiomatic transparency and the side-by-side comparison with Simpson's proof in Section 3.1.2 are strengths. However, the flagship proof currently has a genuine gap, so the significance is conditional; the underlying claims may be correct and are partly established in the companion paper [45], but this manuscript does not yet supply complete proofs of all of its advertised liftings.

major comments (2)
  1. [Section 3.1.2, Eq. (3.5) / Theorem 3.7] The directed set D defined by (3.5) is not directed for arbitrary Y^2, so MCT[0,1]^net cannot be applied to the Specker net c_w. For constant Y, D contains only the empty sequence and singletons, and two distinct singletons <f> and <g> have no common upper bound, since any admissible sequence containing both would have two entries with equal Y-value. The proof therefore silently assumes injectivity of Y. Footnote 4 promises a modification for non-injective Y but does not supply it, and the reduction in Theorem 3.6 does not produce an injective G. This gap is load-bearing: it is the flagship instance of the lifting thesis, and without a directed index set the derivation of (3.6) and RANGE collapses. The theorem is proved in companion paper [45], so the underlying claim may be true, but the proof as written is incomplete.
  2. [Section 3.4, Theorem 3.23 / Eq. (3.9)] The chain of implications in (3.9) applies Rado(NN) to the family F_w, but the agreement property in Rado(NN) only compares F with F_K on the finite set J. To infer F(~n)=1 from F_{w0}(~n)=1, the proof needs a finite set J containing both ~n and the witness g, together with a compatible choice of F_K for K superset of J; none of this is stated. As written, the middle implication in (3.9) is not justified. Please supply the missing instantiation of Rado(NN) or revise the argument.
minor comments (3)
  1. [Title and Section 1] The full-text title contains 'COUNT ABLE' and 'UNCOUNT ABLE' with spurious spaces; please fix this typography.
  2. [Section 3.2, Theorem 3.13 proof] The phrase 'One seems to need IND to form the finite sub-cover' is imprecise; specify the induction instance used to select finitely many balls covering the finitely many Y-values below the threshold.
  3. [Throughout, Section 3.5] The notation '4√p' for a fourth root is nonstandard and should be typeset as \sqrt[4]{p} to avoid confusion.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central MCT^net→BOOT proof is self-contained; self-citations are provenance, and the flagged directedness gap is a correctness flaw, not a circular reduction.

full rationale

The derivation chain MCT[0,1]^net→RANGE→BOOT is presented in the paper itself. Theorem 3.7 constructs the Specker net c_w, applies the monotone convergence theorem, derives equivalence (3.6), and applies Δ-CA; Theorem 3.6 proves RANGE↔BOOT in line. References to [45] are explicitly provenance rather than load-bearing: for example, 'This theorem was first proved as [45, Theorem 3.19]' follows a complete proof, and 'A much less detailed proof was first published in [45]' accompanies the full proof of Theorem 3.7. Even where a later proof says 'yielding BOOT by [45, Theorem 3.19]', the same equivalence was already proved in this paper as Theorem 3.6, so the citation is redundant rather than load-bearing. BOOT and RANGE are not defined in terms of MCT^net, and no parameter is fitted to data and then renamed a prediction. The flagged defect in Theorem 3.7—that the set D defined by (3.5) need not be directed for arbitrary Y, so MCT^net cannot be applied, and the promised modification in Footnote 4 is not supplied—is a genuine correctness gap in the self-contained proof. That footnote says: 'The proof in items (i)-(iv) goes through for (c_n) replaced by (d_n), while the proof of Theorem 3.7 can be modified similarly.' This limitation is real, but it is not a circularity: the gap does not make the theorem's conclusion equal to an assumption, nor does the argument reduce by definition to its input. Under the evidentiary standard of quoting an explicit reduction, no circular step is exhibited.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper contributes no empirical parameters or hidden model constants. Its dependence is on the formal framework of higher-order reverse mathematics and on previously established results in second-order RM (Simpson) and the author's own prior work. The central claim rests on the choice of net-based formulations and on the correctness of the lifted proofs.

assumptions (4)
  • domain assumption RCA0^omega, Kohlenbach's base theory of higher-order reverse mathematics, including QF-AC^{1,0}, primitive recursion, and extensionality, is the formal base system.
    All theorems are proved in this framework (Section 2.1); the results are relative to this formal system and to the language of finite types.
  • domain assumption The systems ACA0^omega, Delta-CA, BOOT, QF-AC^{0,1}, and IND are used as axioms or assumptions in the lifted implications.
    These are standard higher-order comprehension and choice principles introduced in Section 2.2; the paper proves implications of the form A to B over these systems, not from first principles.
  • standard math The countable reverse mathematics results from Simpson's book [51], such as the Specker sequence proof of MCT[0,1]^seq to ACA0 and the algebraic closure lemmas, are taken as established.
    The liftings start from proofs in [51]; the paper relies on those derivations without reproving them, and uses them as the countable benchmark.
  • domain assumption The notion of a net over Baire space is the correct uncountable generalization of a sequence, and the statements MCT^net, CLO, ORD, ALCL, UACL, and AUTO are the natural higher-order analogues of the countable theorems.
    The paper chooses these formulations in Sections 3.1 through 3.7; other formalizations could change the resulting implications.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Lifting countable to uncountable mathematics." pith.science (2026). https://pith.science/paper/MXMDK2GJ

@misc{pith2026190805677,
  author       = {Pith},
  title        = {Pith review of: Lifting countable to uncountable mathematics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MXMDK2GJ}},
  note         = {Machine review of arXiv:1908.05677}
}
read the original abstract

Turing's famous 'machine' framework provides an intuitively clear conception of 'computing with real numbers'. A recursive counterexample to a theorem shows that the theorem does not hold when restricted to computable objects. These counterexamples are often crucial in establishing reversals in the Reverse Mathematics program. All the previous is essentially limited to a language that can only express countable mathematics directly. The aim of this paper is to show that reversals and recursive counterexamples, countable in nature as they might be, directly yield new and interesting results about uncountable mathematics with little-to-no modification. We shall treat the following topics/theorems: the monotone convergence theorem/Specker sequences, compact and closed sets in metric spaces, the Rado selection lemma, the ordering and algebraic closures of fields, and ideals of rings. The higher-order generalisation of sequence is of course provided by nets (aka Moore-Smith sequences ).

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Plato and the foundations of mathematics

    math.LO 2019-08 conditional novelty 7.0 of 10

    A higher-order hierarchy built from net convergence and a bootstrap axiom maps via the ECF interpretation onto the Big Five of second-order Reverse Mathematics.

Reference graph

Works this paper leans on

59 extracted references · 59 canonical work pages · cited by 1 Pith paper

  1. [45]

    , Plato and the foundations of mathematics , Submitted, arxiv: https://arxiv.org/abs/1908.05676 (2019), pp. 44

    work page Pith review arXiv 2019

  2. [46]

    , Lifting recursive counterexamples to higher-order arithm etic, Proceedings of LFCS2020, Lecture Notes in Computer Science 11972, Springe r (2020)

    work page 2020

  3. [1]

    Dialectica

    Jeremy Avigad and Solomon Feferman, G¨ odel’s functional (“Dialectica”) interpretation, Handbook of proof theory, Stud. Logic Found. Math., vol. 137 , 1998, pp. 337–405

    work page 1998

  4. [2]

    Bartle, Nets and filters in topology , Amer

    Robert G. Bartle, Nets and filters in topology , Amer. Math. Monthly 62 (1955), 551–557

    work page 1955

  5. [3]

    Pure Appl

    Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A functional interpretation for nonstandard arithmetic , Ann. Pure Appl. Logic 163 (2012), no. 12, 1962–1994

    work page 2012

  6. [4]

    Brown, Notions of closed subsets of a complete separable metric spa ce in weak subsystems of second-order arithmetic , Logic and computation (Pittsburgh, PA, 1987), Con- temp

    Douglas K. Brown, Notions of closed subsets of a complete separable metric spa ce in weak subsystems of second-order arithmetic , Logic and computation (Pittsburgh, PA, 1987), Con- temp. Math., vol. 106, Amer. Math. Soc., Providence, RI, 199 0, pp. 39–50

    work page 1987

  7. [5]

    Notes Log., vol

    , Notions of compactness in weak subsystems of second order ar ithmetic, Reverse mathematics 2001, Lect. Notes Log., vol. 21, Assoc. Symbol. Logic, 2005, pp. 47–66

    work page 2001

  8. [6]

    Wilfried Buchholz, Solomon Feferman, W olfram Pohlers, and Wilfried Sieg, Iterated inductive definitions and subsystems of analysis: recent proof-theor etical studies , LNM 897, Springer, 1981

    work page 1981

Show all 59 references
  1. [7]

    19 (1895), 1–61

    Pierre Cousin, Sur les fonctions de n variables complexes , Acta Math. 19 (1895), 1–61

  2. [8]

    Dorais, Jeffry Hirst, and Paul Shafer, Reverse mathematics and algebraic field extensions, Preprint, arxiv: https://arxiv.org/abs/1209.4944 (2013), pp

    Fran ccois G. Dorais, Jeffry Hirst, and Paul Shafer, Reverse mathematics and algebraic field extensions, Preprint, arxiv: https://arxiv.org/abs/1209.4944 (2013), pp. 25

    2013 arXiv

  3. [9]

    2, 75–92

    , Reverse mathematics and algebraic field extensions , Computability 2 (2013), no. 2, 75–92

    2013

  4. [10]

    Yu. L. Ershov, Theorie der Numerierungen. III , Z. Math. Logik Grundlagen Math. 23 (1977), no. 4, 289–371

    1977

  5. [11]

    Yu. L. Ershov, S. S. Goncharov, A. Nerode, J. B. Remmel, a nd V. W. Marek (eds.), Handbook of recursive mathematics. Vol. 1 , Studies in Logic and the Foundations of Mathematics, vol. 138, North-Holland, Amsterdam, 1998. Recursive model theory

    1998

  6. [12]

    unpublished notes from 1977-1981 with updated intro duction, https://math.stanford.edu/~feferman/papers/pfa(1).pdf

    Solomon Feferman, How a Little Bit goes a Long Way: Predicative Foundations of Analysis , 2013. unpublished notes from 1977-1981 with updated intro duction, https://math.stanford.edu/~feferman/papers/pfa(1).pdf

    2013

  7. [13]

    C ., 1974), Vol

    Harvey Friedman, Some systems of second order arithmetic and their use , Proceedings of the International Congress of Mathematicians (Vancouver, B. C ., 1974), Vol. 1, 1975, pp. 235–242

    1974

  8. [14]

    Symbolic Logic 41 (1976), 557–559

    , Systems of second order arithmetic with restricted inducti on, I & II (Abstracts) , J. Symbolic Logic 41 (1976), 557–559

    1976

  9. [15]

    Simpson, and Rick L

    Harvey Friedman, Stephen G. Simpson, and Rick L. Smith, Countable algebra and set exis- tence axioms , Ann. Pure Appl. Logic 25 (1983), no. 2, 141–181

    1983

  10. [16]

    Fr¨ ohlich and J

    A. Fr¨ ohlich and J. C. Shepherdson, Effective procedures in field theory , Philos. Trans. Roy. Soc. London. Ser. A. 248 (1956), 407–432

    1956

  11. [17]

    Robin Gandy, General recursive functionals of finite type and hierarchie s of functions , Ann. Fac. Sci. Univ. Clermont-Ferrand No. 35 (1967), 5–24

    1967

  12. [18]

    Symbolic Logic 56 (1991), no

    Kostas Hatzikiriakou, Minimal prime ideals and arithmetic comprehension , J. Symbolic Logic 56 (1991), no. 1, 67–70

    1991

  13. [19]

    Thesis (Ph.D.)–The Pennsylvania State University

    Jeffry Lynn Hirst, Combinatorics In Subsystems Of Second Order Arithmetic , ProQuest LLC, Ann Arbor, MI, 1987. Thesis (Ph.D.)–The Pennsylvania State University

    1987

  14. [20]

    1876, Springer, 2006

    Horst Herrlich, Axiom of choice , Lecture Notes in Mathematics, vol. 1876, Springer, 2006

    2006

  15. [21]

    I , Zweite Auflage

    David Hilbert and Paul Bernays, Grundlagen der Mathematik. I , Zweite Auflage. Die Grundlehren der mathematischen Wissenschaften, Band 40, S pringer, 1968

    1968

  16. [22]

    II , Zweite Auflage

    , Grundlagen der Mathematik. II , Zweite Auflage. Die Grundlehren der mathematis- chen Wissenschaften, Band 50, Springer, 1970

    1970

  17. [23]

    Thesis (Ph.D.)–The University of Wisconsin - Madison

    James Hunter, Higher-order reverse topology , ProQuest LLC, Ann Arbor, MI, 2008. Thesis (Ph.D.)–The University of Wisconsin - Madison

    2008

  18. [24]

    87, American Mathematical Society, Providen ce, RI; Mathematics Advanced Study Semesters, University Park, PA, 2018

    Matthew Katz and Jan Reimann, An introduction to Ramsey theory , Student Mathematical Library, vol. 87, American Mathematical Society, Providen ce, RI; Mathematics Advanced Study Semesters, University Park, PA, 2018. Fast functions , infinity, and metamathematics

    2018

  19. [25]

    Kelley, General topology, Springer-Verlag, 1975

    John L. Kelley, General topology, Springer-Verlag, 1975. Reprint of the 1955 edition; Gradu ate Texts in Mathematics, No. 27

    1975

  20. [26]

    Notes Log., vol

    Ulrich Kohlenbach, Foundational and mathematical uses of higher types , Reflections on the foundations of mathematics, Lect. Notes Log., vol. 15, Asso c. Symbol. Logic, 2002, pp. 92–116

    2002

  21. [27]

    Notes Log., vol

    , Higher order reverse mathematics , Reverse mathematics 2001, Lect. Notes Log., vol. 21, Assoc. Symbol. Logic, 2005, pp. 281–295. 26 LIFTING PROOFS FROM COUNTABLE TO UNCOUNTABLE MATHEMATIC S

    2001

  22. [28]

    Kreisel and A

    G. Kreisel and A. S. Troelstra, Formal systems for some branches of intuitionistic analysi s, Ann. Math. Logic 1 (1970), 229–387

    1970

  23. [29]

    Mark Mandelkern, Brouwerian counterexamples, Math. Mag. 62 (1989), no. 1, 3–27

    1989

  24. [30]

    E. H. Moore and H. Smith, A General Theory of Limits , Amer. J. Math. 44 (1922), 102–121

    1922

  25. [31]

    Muldowney, A general theory of integration in function spaces, includi ng Wiener and Feynman integration, Vol

    P. Muldowney, A general theory of integration in function spaces, includi ng Wiener and Feynman integration, Vol. 153, Longman Scientific & Technical, Harlow; John Wile y, 1987

    1987

  26. [32]

    Dag Normann and Sam Sanders, On the mathematical and foundational significance of the uncountable, Journal of Mathematical Logic, https://doi.org/10.1142/S0219061319500016 (2019)

    2019 doi

  27. [33]

    , Representations in measure theory , Submitted, arXiv: https://arxiv.org/abs/1902.02756 (2019)

    2019 arXiv

  28. [34]

    , Open sets in Reverse Mathematics and Computability Theory , Journal of Logic and Computability 30 (2020), no. 8, pp. 40

    2020

  29. [35]

    Pure Appl

    , Pincherle’s theorem in reverse mathematics and computabil ity theory , Ann. Pure Appl. Logic 171 (2020), no. 5, 102788, 41

    2020

  30. [36]

    , The Axiom of Choice in Computability Theory and Reverse Math ematics, Submit- ted, arxiv: https://arxiv.org/abs/2006.01614 (2020), pp. 25

    2020 arXiv

  31. [37]

    , On the uncountability of R, Submitted (2020), pp. 29

    2020

  32. [38]

    Rado, Axiomatic treatment of rank in infinite sets , Canadian J

    R. Rado, Axiomatic treatment of rank in infinite sets , Canadian J. Math. 1 (1949), 337–343

    1949

  33. [39]

    H. L. Royden, Real analysis, 3rd ed., Macmillan Publishing Company, 1988

    1988

  34. [40]

    W alter Rudin, Real and complex analysis , 3rd ed., McGraw-Hill, 1987

    1987

  35. [41]

    Nobuyuki Sakamoto and Takeshi Yamazaki, Uniform versions of some axioms of second order arithmetic , MLQ Math. Log. Q. 50 (2004), no. 6, 587–593

    2004

  36. [42]

    Sam Sanders, Nets and Reverse Mathematics: initial results , LNCS 11558, proceedings of CiE19, Springer (2019), pp. 12

    2019

  37. [43]

    , Reverse Mathematics and computability theory of domain the ory, LNCS 11541, pro- ceedings of W oLLIC19, Springer (2019), pp. 20

    2019

  38. [44]

    , Nets and Reverse Mathematics: a pilot study , Computability, doi:10.3233/COM-190265 (2019), pp. 34

    2019 doi

  39. [47]

    , Splittings and disjunctions in reverse mathematics , Notre Dame J. Form. Log. 61 (2020), no. 1, 51–74

    2020

  40. [48]

    , Reverse Mathematics of topology: dimension, paracompactn ess, and splittings , To appear in: Notre Dame Journal for Formal Logic, arXiv: https://arxiv.org/abs/1808.08785 (2020), pp. 21

    2020 arXiv

  41. [49]

    Simpson and J

    Stephen G. Simpson and J. Rao, Reverse algebra, Handbook of recursive mathematics, Vol. 2, Stud. Logic Found. Math., vol. 139, North-Holland, 1998, pp. 1355–1372

    1998

  42. [50]

    Simpson (ed.), Reverse mathematics 2001 , Lecture Notes in Logic, vol

    Stephen G. Simpson (ed.), Reverse mathematics 2001 , Lecture Notes in Logic, vol. 21, Assoc. Symbol. Logic, La Jolla, CA, 2005

    2001

  43. [51]

    , Subsystems of second order arithmetic , 2nd ed., Perspectives in Logic, CUP, 2009

    2009

  44. [52]

    Symbolic Logic 14 (1949), 145–158 (German)

    Ernst Specker, Nicht konstruktiv beweisbare S¨ atze der Analysis, J. Symbolic Logic 14 (1949), 145–158 (German)

    1949

  45. [53]

    Stillwell, Reverse mathematics, proofs from the inside out , Princeton Univ

    J. Stillwell, Reverse mathematics, proofs from the inside out , Princeton Univ. Press, 2018

    2018

  46. [54]

    Charles Swartz, Introduction to gauge integrals , W orld Scientific, 2001

    2001

  47. [55]

    81, North-Holland, 1987

    Gaisi Takeuti, Proof theory, 2nd ed., Studies in Logic and the Foundations of Mathematic s, vol. 81, North-Holland, 1987. With an appendix containing c ontributions by Georg Kreisel, W olfram Pohlers, Stephen G. Simpson and Solomon Feferman

    1987

  48. [56]

    Lecture Notes in Mathematics, Vol

    Anne Sjerp Troelstra, Metamathematical investigation of intuitionistic arithm etic and anal- ysis, Springer Berlin, 1973. Lecture Notes in Mathematics, Vol. 344

    1973

  49. [57]

    Anne Sjerp Troelstra and Dirk van Dalen, Constructivism in mathematics. Vol. I , Studies in Logic and the Foundations of Mathematics, vol. 121, North-H olland, 1988

    1988

  50. [58]

    Alan Turing, On computable numbers, with an application to the Entscheid ungs-problem, Proceedings of the London Mathematical Society 42 (1936), 230-265

    1936

  51. [59]

    Leopold Vietoris, Stetige Mengen , Monatsh. Math. Phys. 31 (1921), no. 1, 173–204 (German)

    1921

Pith tools

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