10
$\begingroup$

Bounded Zermelo set theory, and many variants named for MacLane in some way, are used in equiconsistency proofs for Simple Theory of Types plus infinity, and for the Elementary Theory of the Category of Sets starting in 1969 (see Finite order arithmetic and ETCS). But did anyone formulate it before that?

Of course Bounded Zermelo could easily have been stated before that, and the analogy with Primitive Recursive Arithmetic could have suggested it. But was it formulated earlier in fact?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
9
$\begingroup$

The Princeton thesis of John Kemeny, written in 1949, was devoted to the relation between Zermelo set theory and type theory. For example, early in the thesis, there is a proof of the consistency of the simple theory of types relative to the consistency of a small fragment (nowadays known as KF) of Bounded Zermelo set theory. The comprehension scheme in KF is limited to stratifiable instances of bounded comprehension. KF was explicitly introduced and studied by Kaye and Forster in their 1991 paper in JSL entitled "End-extensions Preserving Power Set" (JSTOR).

For more detail, see subsection 8.0 of Mathias' Strength of Mac Lane Set Theory (APAL, 2001, https://doi.org/10.1016/S0168-0072(00)00031-2); indeed Mathias further discusses Kemeny's thesis in detail towards the end of section 8 of his paper.

Based on Mathias' account, it is clear that, conceptually, Kemeny "knew about" bounded Zermelo set theory, but it is not clear to me whether he explicitly formulated any fragments of Zermelo set theory.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Is there anything about weak fragments of $\sf ZF$ which doesn't appear in Mathias' paper? Incredible. $\endgroup$
    – Asaf Karagila ♦
    Commented Nov 18, 2014 at 17:38
  • $\begingroup$ And that is why Jensen would later take this route for consistency of NFU. $\endgroup$
    – Colin McLarty
    Commented Nov 18, 2014 at 18:14
2
$\begingroup$

I wish there was more direct evidence. For now, it seems likely Bounded Zermelo originated as one unnamed member of a family of theories arising from equiconsistency results.

The article

  • Jensen RB, "On the consistency of a slight (?) modification of Quine's New Foundations" Synthese 19 (1969) pp 25–63. doi:10.1007/BF00568059, JSTOR

introduces "a weak version of Zermelo set theory" which has the axioms of extensionality, pair set, sum set and power set, plus bounded separation. He gives it no usable descriptive name but and just calls it $S$. He gives no references but says it is "folklore" that this theory (or it plus infinity, or plus infinity and choice) is equiconsistent with simple type theory (plus the same).

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .