7
$\begingroup$

Zbierski "Models for Higher Order Arithmetics" (BULL. DE L'ACAD. POLONAISE DES SCIENCES Serie des sciences math., astr. et phys. - Vol. XIX, No. 7, 1971) defines ZF$_n$ as ZFC with the power set axiom limited to $n$ successive power sets starting from the natural numbers $\mathbb{N}$. Note this includes the axiom of choice. He proves ZF$_n$ is a conservative extension of $n+2$ order arithmetic with the axiom scheme of choice.. He notes Gandy had proved already ZF$_2$ is not conservative over $4$th order arithmetic without the axiom scheme of choice.

But what is known about the case where the axiom of choice is also removed from ZF$_2$?

Sochor "Constructibility in higher order arithmetics" (Arch. Math. Logic (1993) 32:381-389) shows that $n$-th order arithmetic without choice can interpret $n$-th order arithmetic with choice.though obviously it is not a conservative extension. So the issue is not equiconsistency. It is conservativity.

$\endgroup$
15
  • $\begingroup$ Since collection and replacement are no longer equivalent without full power set, could you clarify exactly what the theory is? e.g. jdh.hamkins.org/what-is-the-theory-zfc-without-power-set $\endgroup$ Dec 11, 2014 at 14:09
  • 1
    $\begingroup$ @JoelDavidHamkins Actually Zbierski is not explicit about those issues, and following the tradition of proof theory his proofs are telegraphic and rest heavily on what it is "easy to see." So it is not easy to see exactly what axioms he has in mind for ZFC. His arithmetic axiom scheme of choice says wherever a formula $F(x,y)$ relates every order $n$ set to at least one order $n+1$ set then there is some single order $n+1$ set $z$ collecting codes for order $n$ pairs such that each $x$ is $F$-related to the set $z^{(x)}$ of all $u$ such that code for $\langle x,u\rangle$ is in $z$. $\endgroup$ Dec 11, 2014 at 14:33
  • 1
    $\begingroup$ There is no way to express the well-orderability of the highest sort in $n$th order arithmetic without using an extra $(n+1)$th order relation symbol, or something to that effect. This is why the standard formulation of AC in higher-order arithmetic is the choice functions version. $\endgroup$ Dec 11, 2014 at 14:47
  • 1
    $\begingroup$ Zbierski is specific about choice in $\mathrm{ZFC}_n$ in this paper: matwbn.icm.edu.pl/ksiazki/fm/fm112/fm112118.pdf $\endgroup$ Dec 11, 2014 at 16:57
  • 2
    $\begingroup$ The replacement/collection issue is irrelevant to Zbierski. The goal is to show that every model of $(n+2)$-nd order arithmetic is the $(n+2)$-nd order arithmetical part of a model of $\mathrm{ZFC}_n$. All of this happens in sets of rank bounded $\omega+n+2$, where replacement/collection issues are nonexistent. $\endgroup$ Dec 11, 2014 at 17:04

1 Answer 1

4
$\begingroup$

The usual way to prove something like this is to take a model of $(n+1)$-st order arithmetic $\mathcal{A}$ and interpret a model of set theory $\mathcal{V}$ in $\mathcal{A}$ such a the usual interpretation of $(n+1)$-st order arithmetic in $\mathcal{V}$ leads to a model isomorphic to $\mathcal{A}$. There are a few recipes to do this, using graph, trees and other convenient encodings of sets. See the discussion here, I will use wellfounded accessible pointed graphs (WAPGs), though Zbierski probably uses trees (I don't know since I haven't found the paper).

The model $\mathcal{A}$ of $(n+1)$-st order arithmetic has sorts $N = S_0,S_1,\ldots,S_n$, where $N$ is the number sort and each $S_{i+1}$ consists of subsets of the previous sort $S_i$. The number sort $N$ has the usual arithmetic structure with full induction for the implied language. Each sort $S_i$ ($i \geq 1$) has full comprehension within the implied language. I'll refrain from making choice assumptions to see how far things go. Each sort has a definable pairing function, so we can talk about tuples, relations and functions. In particular, we can talk about WAPGs coded in $S_n$.

The model $\mathcal{V}$ is obtained by collecting all WAPGs in the top sort $S_n$. Equality $G \equiv H$ between two WAPGs $G$ and $H$ is interpreted as the existence of a bisimulation between $G$ and $H$, and membership $G \in H$ is interpreted as the existence of a bisimulation between $G$ and an immediate subgraph $H/x$ of $H$. After quotienting by $\equiv$ if desired, the result is an interpretation of the language of set theory which is automatically extensional and wellfounded (in the internal sense). Furthermore, since WAPGs coded in $S_n$ and bisimulations between them are definable in $(n+1)$-th order arithmetic, every formula $\phi$ in the language of set theory has a translation $\phi^V$ in the language of $(n+1)$-th order arithmetic such that $\mathcal{V} \vDash \phi \iff \mathcal{A} \vDash \phi^V$.

Furthermore, we can define canonical WAPGs for each sort $\omega,\mathcal{P}(\omega),\ldots,\mathcal{P}^{n-1}(\omega)$. Specifically, the WAPG for $\omega$ is the graph of the ordering relation on the sort $N$; the WAPG for $\mathcal{P}(\omega)$ is built on top of that one by adding a node for each $X \in \mathcal{S}_1$ and linking it to its elements; etc. Using the fact that $\mathcal{A}$ has full comprehension and the translation, we see that each $\mathcal{P}^{i+1}(\omega)$ really is the powerset of the previous one as understood in $\mathcal{V}$. So the natural interpretation of the arithmetical sorts $\omega,\mathcal{P}(\omega),\ldots,\mathcal{P}^{n-1}(\omega)$ in $\mathcal{V}$ are canonically isomorphic to the original sorts $N,S_1,\ldots,S_{n-1}$ from $\mathcal{A}$. The top sort $\mathcal{P}^n(\omega)$ is not necessarily a set in $\mathcal{V}$ but it is a definable class. Again, full comprehension can be used to argue that $\mathcal{P}^n(\omega)$ is canonically isomorphic to the original top sort $S_n$.

So far, we haven't needed any choice; I only used full comprehension in $\mathcal{A}$. It remains to check which axioms $\mathcal{V}$ satisfies. Many are straightforward to check. We already checked extensionality, foundation and infinity. Pairing and union correspond to simple combinatorial manipulations of WAPGs. Comprehension follows from comprehension in $\mathcal{A}$. Replacement/collection are problematic without further assumptions about $\mathcal{A}$. There is a good reason for that since we have just shown one half of:

Theorem. The theory $\mathrm{Z}^-_{n-1}$ (extensionality, foundation, pairing, union, comprehension and the existence of $\omega,\mathcal{P}(\omega),\ldots,\mathcal{P}^{n-1}(\omega)$) is a conservative extension of $(n+1)$-th order arithmetic (without choice).

The missing half is the straightforward proof that $\mathrm{Z}^-_{n-1}$ is an extension of $(n+1)$-th order arithmetic. In other words, that the interpretation $N = \omega, S_1 = \mathcal{P}(\omega), \ldots, S_n = \mathcal{P}^n(\omega)$ always yields a model of $(n+1)$-th order arithmetic.


Here is a reason why some choice principles might be necessary. For simplicity, I will assume we are working in $2$-nd order arithmetic. I will show that if collection holds in $\mathcal{V}$ then countable choice holds in $\mathcal{A}$. Say $\phi(n,x)$ is a formula in $2$-nd order arithmetic that relates each natural number $n$ with a set $x$ of natural numbers. We can translate $\phi(n,x)$ to a synonymous formula $\psi(n,x)$ in $\mathcal{V}$ such that $(\forall n \in \omega)(\exists x \subseteq \omega)\psi(n,x)$. Every set in $\mathcal{V}$ is countable, by construction, so if there is a set $b \in \mathcal{V}$ such that $(\forall n \in \omega)(\exists x \in b)\psi(n,x)$, then back in $\mathcal{A}$ there is a countable sequence $\langle x_n \rangle$ coded in $S_1$ such that $\phi(n,x_n)$ holds for every $n$.

In a similar fashion, for any $n$, if $S_{n-1}$ is wellorderable in a model $\mathcal{A}$ of $(n+1)$-st order arithmetic, then collection in $\mathcal{V}$ gives choice for definable $S_{n-1}$-indexed families in $\mathcal{A}$.

$\endgroup$
7
  • $\begingroup$ Could you say precisely what theory is "$(n+1)$-th order arithmetic"? $\endgroup$ Dec 11, 2014 at 23:15
  • $\begingroup$ It's debatable but what I wrote in the second paragraph is pretty standard. The sort $N$ satisfies basic arithmetic ($0,1,+,\times$) with induction for all formulas (including formulas that involve quantifiers or parameters of higher sorts). Full comprehension for each set sort $S_1,\ldots,S_n$ (again, for all formulas). I think some would include some choice, in particular choice over $N$, but Colin specifically asked about omitting choice. $\endgroup$ Dec 11, 2014 at 23:24
  • $\begingroup$ And, of course, the set sorts are required to satisfy extensionality. Technically, they don't have to be actual sets, we just have membership relations $\in_i$ from $S_{i-1}$ to $S_i$, but with extensionality we may as well assume that they consist of actual sets. $\endgroup$ Dec 11, 2014 at 23:28
  • $\begingroup$ The argument gives a little more than just $\mathrm{Z}_{n-1}^-$. Namely, the Mostowski Beta axiom (every extensional wellfounded relation on a set has a Mostowski collapse) is valid in $\mathcal{V}$. This gives a little bit of replacement but not much. $\endgroup$ Dec 11, 2014 at 23:49
  • $\begingroup$ This is the right technology, but I do not think it will give replacement without considerations of constructibility and hereditary constructible countability and its analogues to make each higher order correspond to one higher cardinal. $\endgroup$ Dec 12, 2014 at 0:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.