pith. sign in

arxiv: 2604.01139 · v2 · submitted 2026-04-01 · 🧮 math.LO · math.CT

Makkai's lost proof of projectivity of N in the free topos

Henrik Forssell , Peter LeFanu Lumsdaine , Andrew W. Swan This is my paper

Pith reviewed 2026-05-13 21:47 UTC · model grok-4.3

classification 🧮 math.LO math.CT
keywords free toposnatural numbers objectprojectivitycountable choiceintuitionistic logichigher-order logiccategorical logic
0
0 comments X

The pith

The natural numbers object is projective in the free topos, establishing the countable choice rule for intuitionistic higher-order logic.

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

This paper reconstructs Michael Makkai's unpublished proof that the natural numbers object N is projective in the free topos. Projectivity of N means every epimorphism onto N admits a section, which translates directly in the internal logic to the validity of countable choice for arbitrary formulas. The argument is carried out entirely within the language of elementary toposes and their logic, with the goal of self-contained accessibility for readers already familiar with these structures. If the proof holds, it confirms that the free topos satisfies a non-trivial choice principle without any classical assumptions or extra axioms.

Core claim

We give a categorical proof of the projectivity of N in the free topos -- in proof-theoretic terms, the rule of countable choice for intuitionistic higher-order logic -- based on the unpublished proof of Michael Makkai (c.1980). The presentation aims to be self-contained and accessible to any reader acquainted with elementary toposes and their logic.

What carries the argument

The free topos together with its natural numbers object N, whose projectivity is established by showing that epimorphisms onto N always split using the universal properties of the free topos.

If this is right

  • Countable choice holds for every formula in the internal logic of the free topos.
  • The free topos supplies a concrete model of intuitionistic higher-order logic in which countable choice is admissible.
  • Any further consequence derived from countable choice in constructive logic is realized inside the free topos.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same technique may adapt to establish projectivity of free objects built from other signatures in toposes.
  • Connections could be explored to realizability models or other constructive universes where analogous choice principles are known to hold.

Load-bearing premise

The free topos is an elementary topos containing a natural numbers object that behaves according to the standard internal logic of toposes.

What would settle it

Constructing, inside the free topos, an epimorphism onto N that has no section would show the claim is false.

read the original abstract

We give a categorical proof of the projectivity of $N$ in the free topos -- in proof-theoretic terms, the rule of countable choice for intuitionistic higher-order logic -- based on the unpublished proof of Michael Makkai (c.1980). The presentation aims to be self-contained and accessible to any reader acquainted with elementary toposes and their logic.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript reconstructs Makkai's unpublished circa-1980 proof that the natural numbers object N is projective in the free topos. In proof-theoretic terms this establishes the rule of countable choice for intuitionistic higher-order logic. The argument proceeds by exhibiting lifts along epimorphisms using the universal property of the free topos together with the internal logic of an elementary topos, and is presented as self-contained for readers familiar with topos theory.

Significance. If the derivation is correct, the result supplies a direct categorical confirmation that countable choice holds in the free topos without external choice principles. This makes an important but previously inaccessible argument available to the community and strengthens the understanding of the internal logic of the free topos.

minor comments (2)
  1. [Introduction] The introduction would benefit from a short roadmap paragraph outlining the main steps of the reconstruction before the detailed argument begins.
  2. [Section 4] A few internal references to lemmas in the free topos construction could be made more explicit by adding equation numbers.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading and positive recommendation to accept the manuscript. The report contains no major comments requiring response.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper reconstructs Makkai's argument for projectivity of N in the free topos by exhibiting lifts along epis via the universal property of the free topos and the internal logic of elementary toposes. No load-bearing step reduces by construction to a fitted input, self-definition, or self-citation chain; the central claim derives countable choice for intuitionistic higher-order logic directly from standard topos axioms without circular appeal to the result. The presentation is explicitly self-contained for readers familiar with elementary toposes, with no renaming of known results or ansatz smuggling.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proof rests on the standard axioms of elementary toposes and their internal logic; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • standard math Standard axioms and properties of elementary toposes and their internal logic
    Invoked as the background for the categorical proof of projectivity.

pith-pipeline@v0.9.0 · 5356 in / 1054 out tokens · 40449 ms · 2026-05-13T21:47:41.393787+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages

  1. [1]

    Algebraic theories of quasivari- eties

    [AP98] Jiří Adámek and Hans-E. Porst. “Algebraic theories of quasivari- eties”. In:J. Algebra208(2) (1998), pp. 379–398.issn: 0021-8693. doi:10.1006/jabr.1998.7499. [AR94] Jiří Adámek and Jiří Rosický.Locally presentable and accessible categories. Vol

    work page doi:10.1006/jabr.1998.7499 1998

  2. [2]

    Ad \'a mek and J

    London Mathematical Society Lecture Note Series. Cambridge: Cambridge University Press, 1994, pp. xiv+316. isbn: 0-521-42261-2.doi:10.1017/CBO9780511600579. [Bir+98] Lars Birkedal et al. “Type theory via exact categories”. Exten- ded abstract. In:Proc. 13th Annual IEEE Symposium on Logic in Computer Science. Los Alamitos, CA: IEEE Computer Soc., 1998, pp....

    work page doi:10.1017/cbo9780511600579 1994

  3. [3]

    On derived rules of intuitionistic second order arithmetic

    North-Holland Mathematical Library. North-Holland Publishing Co., Amsterdam, 1990, pp. xviii+296.isbn: 0-444-70368-3; 0-444- 70367-5.doi:10.1016/S0924-6509(08)70048-5.url:https://www. sciencedirect.com/bookseries/north- holland- mathematical- library/vol/39/. [Hay77] Susumu Hayashi. “On derived rules of intuitionistic second order arithmetic”. In:Comment....

    work page doi:10.1016/s0924-6509(08)70048-5.url:https://www 1990

  4. [4]

    Amsterdam: North- Holland Publishing Co., 1999, pp

    Studies in Logic and the Foundations of Mathematics. Amsterdam: North- Holland Publishing Co., 1999, pp. xviii+760.isbn: 0-444-50170- 3.doi:10. 1016/S0049- 237X(98)80030- X.url:https: //www. sciencedirect . com / bookseries / studies - in - logic - and - the - foundations-of-mathematics/vol/141/. REFERENCES 43 [Joh02] Peter T. Johnstone.Sketches of an ele...

    work page 1999

  5. [5]

    Oxford Univer- sity Press (2018).https://doi.org/10.1093/oso/9780198814788.001.0001

    Oxford Logic Guides. New York: The Clarendon Press Oxford University Press, 2002.isbn: 9780198524960.doi: 10.1093/oso/9780198515982.001.0001. [JW79] André Joyal and Gavin Wraith. “Arithmetic universes and the Gödel incompleteness theorem”. Unpublished notes by Wraith from lectures of Joyal

    work page doi:10.1093/oso/9780198515982.001.0001 2002

  6. [6]

    Intuitionist type theory and the free topos

    [LH+19] Peter LeFanu Lumsdaine, Simon Henry et al.Free models of finitely presented essentially algebraic theories in elementary toposes?Math Overflow Q&A thread. 2019.url:https://mathoverflow.net/q/ 346687(visited on 15/04/2025). [LS80] Joachim Lambek and Philip J. Scott. “Intuitionist type theory and the free topos”. In:J. Pure Appl. Algebra19 (1980), p...

    work page doi:10.1016/0022-4049(80)90102-4 2019

  7. [7]

    2003 , note =

    Cambridge Studies in Advanced Mathem- atics. Cambridge University Press, Cambridge, 1986, pp. x+293. isbn: 0-521-24665-2. [Mai03] Maria Emilia Maietti. “Joyal’s arithmetic universes via type the- ory”. In:Electronic Notes in Theoretical Computer Science69 (2003). CTCS’02, Category Theory and Computer Science, pp. 272–286. issn: 1571-0661.doi:10.1016/S1571...

    work page doi:10.1016/s1571-0661(04)80569-3 1986

  8. [8]

    Lex sketches in an arithmetic universe

    Amsterdam: Elsevier, 2005, pp. 105–126.url: www.sciencedirect.com/science/article/pii/S1571066105000356. [Mai06] Maria Emilia Maietti. “Lex sketches in an arithmetic universe”. Unpublished preprint

    work page 2005

  9. [9]

    Joyal’s arithmetic universe as list-arithmetic pretopos

    [Mai10] Maria Emilia Maietti. “Joyal’s arithmetic universe as list-arithmetic pretopos”. In:Theory Appl. Categ.24 (2010), No. 3, 39–83.issn: 1201-561X.url:http://www.tac.mta.ca/tac/volumes/24/3/24- 03abs.html. [Mak80] Michael Makkai. “N is projective in the initial topos”. Unpublished notes, original date uncertain. Ca. 1980? [Men00] Matías Menni. “Exact ...

    work page 2010

  10. [10]

    Review of ‘From sets and types to topology and analysis—towards practicable foundations for constructive mathematics’, ed. Crosilla, Schuster, 2005

    url:http://ncatlab.org/nlab/revision/internally%20projective% 20object/12. [Oos06] Jaap van Oosten. “Review of ‘From sets and types to topology and analysis—towards practicable foundations for constructive mathematics’, ed. Crosilla, Schuster, 2005”. In:Bulletin of Symbolic Logic12(4) (2006), pp. 611–612.doi:10.1017/S107989860000250X. [Oos08] Jaap van Oos...

    work page doi:10.1017/s107989860000250x 2005

  11. [11]

    Partial horn logic and Cartesian categories

    [PV07] Erik Palmgren and Steven J. Vickers. “Partial horn logic and Cartesian categories”. In:Ann. Pure Appl. Logic145(3) (2007), pp. 314–353.issn: 0168-0072.doi:10.1016/j.apal.2006.10.001. [ŠS82] Andrej Ščedrov and Philip J. Scott. “A Note on the Friedman Slash and Freyd Covers”. In:The L. E. J. Brouwer Centenary Symposium. Ed. by A.S. Troelstra and D.va...

    work page doi:10.1016/j.apal.2006.10.001 2007

  12. [12]

    Universes in toposes

    Studies in Logic and the Foundations of Mathematics. Elsevier, 1982, pp. 443–452. doi:10.1016/S0049-237X(09)70142-9. [Str05] Thomas Streicher. “Universes in toposes”. In:From sets and types to topology and analysis. Towards practicable foundations for con- structive mathematics. Based on the workshop, Venice, Italy, May 12–16,

    work page doi:10.1016/s0049-237x(09)70142-9 1982

  13. [13]

    Oxford Univer- sity Press (2018).https://doi.org/10.1093/oso/9780198814788.001.0001

    Oxford University Press, 2005, pp. 78–90.isbn: 0-19- 856651-4.doi:10.1093/acprof:oso/9780198566519.003.0005. [Thu42] James Thurber. “Here lies Miss Groby”. In:The New Yorker(21st Mar. 1942).url:https://www.newyorker.com/magazine/1942/03/21/ here-lies-miss-groby. [Tro18] Anne S. Troelstra.Corrections to some publications. X-2018-02. Institute for Logic, La...

    work page doi:10.1093/acprof:oso/9780198566519.003.0005 2005

  14. [14]

    Springer Berlin Heidelberg, 1973.doi:10.1007/bfb0066739

    Lect. Notes Math. Springer, Cham, 1973.doi:10.1007/BFb0066739. eprint:https://eprints.illc. uva.nl/id/eprint/622. [Tro98] Anne S. Troelstra. “Realizability”. In:Handbook of Proof Theory. Ed. by Samuel R. Buss. Vol

    work page doi:10.1007/bfb0066739 1973

  15. [15]

    Chap. VI, pp. 407–473.doi: 10.1016/S0049-237X(98)80021-9. Institutt for informatikk, Universitetet i Oslo, Oslo, Norway Matematiska institutionen, Stockholms universitet, Stockholm, Sweden Fakulteta za matematiko in fiziko, Univerza v Ljubljani, Ljubljana, Slovenia

    work page doi:10.1016/s0049-237x(98)80021-9