On interpretations of arithmetic and set theory^{∗}

Richard Kaye and Tin Lok Wong School of Mathematics University of Birmingham Birmingham B15 2TT U.K.

15 July, 2006

1 Introduction

The work described in this article starts with a piece of mathematical ‘folklore’ that is ‘well known’ but for which we know no satisfactory reference.^{1}

Folklore Result. The first-order theories Peano arithmetic and ZFset theory with the axiom of infinity negated are equivalent, in the sense that each is interpretable in the other and the interpretations are inverse to each other.

This would make an excellent starting point for any beginning research student working in the area of models of Peano arithmetic, since an understanding of how these interpretations work enables all coding techniques from set theory to be employed in arithmetic in a uniform way, and also places PA ‘on the map’ (in the sense of consistency and interpretation strength) relative to set theory. This, combined with the lack of suitable references, permits us, we trust, to omit any apology for investigating such folklore. In fact, when the details were finally uncovered, there were surprises for both authors—this is the reason for the quotation marks when we said that the folkloric result above is ‘well known’.

We should be more precise and highlight exactly where the imprecision in the folkloric result lies. There are two places: firstly, the notion of ‘ZF set theory with the axiom of infinity negated’ turns out to be dependent in quite an important way on the preferred choice of the initial presentation of ZF; secondly, the idea of interpretations being ‘inverse to each other’ admits important variations. For example, Chang and Keisler [5, §A.31] specify one particular choice of axiomatisation of ZF; for this axiomatisation a weak form of interpretation-equivalence of ‘ZF with infinity negated’ and PAcan be proved, but for stronger notions of interpretation-equivalence a different axiomatisation of ZFseems to be required.

∗This is a slightly expanded version of a paper to appear in the Notre Dame Journal of Formal Logic under the same title. We have taken the opportunity in this web version of the paper to add a few additional comments and references to some additional material.

1Further references. Świerczkowski [20] wrote a detailed exposition of the equivalence of PAand “the theory of hereditarily finite sets”, which uses an additional adduction operator. This theory of sets is said be adapted from Tarski and Givant [25] with slight variations. The adduction operator ◁, defined by

x ◁ y = x ∪ {y}, is also studied by Kirby [13] in the context of ZFwithout the axiom of infinity.

Another theory of sets that was proved to be “equivalent” to PAis PSintroduced by Previale [17]. However, the interpretations there seem to be the Ackermann one and the ordinal one (cf. Kirby [13, §2] and Sections 3, 4).

Our notation and terminology is standard. For a text on set theory we have used Drake [7], though many others would be suitable. For background on Peano arithmetic we refer the reader to Kaye [12], and especially Chapter 10 for background on subsystems of PA.

2 Interpretations

The first issue to address here is what we shall mean by ‘interpretation’ and when interpretations are ‘inverse’ to one another. In fact, for the folkloric result we are addressing, the notion of interpretation required is very straightforward and concrete, but in general the word ‘interpretation’ is used in many contexts and with many different meanings in logic and model theory.

As pointed out elsewhere, notably by Visser [26], notions of interpretation can be best brought together using a category theoretic framework, though in this paper we use category theory simply as a notational device. For us, an interpretation 𝔦 of a theory T_{2} in a theory T_{1} is a morphism 𝔦: T_{2} → T_{1} in a particular category being studied.

To define the particular category we will use in this paper, let us agree that an ℒ -theory is a consistent set of ℒ -sentences (not necessarily complete or closed under deduction) and we make the convenient assumptions that all languages are purely relational, equality (=) being one of the relation symbols, and a further unary relation Dom() for the domain is always present. Full first-order logic is assumed, including all the rules for equality and the additional logical axiom ∀xDom(x). For us here, an interpretation 𝔦: T_{2} → T_{1} of an ℒ_{2}-theory T_{2} in an ℒ_{1}-theory T_{1} is given by a mapping of atomic formulas R(x_{1},x_{2},...,x_{n}) of ℒ_{2} to formulas R(x_{1},x_{2},...,x_{n})^{𝔦} of ℒ_{1} in the same free variables. In particular, the domain and equality on this domain are defined by Dom(x)^{𝔦} and (x = y)^{𝔦}. The mapping extends to all first-order formulas in the natural way by setting (¬θ(x̄))^{𝔦} to be ¬ θ(x̄)^{𝔦}, (ϕ(x̄) → ψ(x̄))^{𝔦} to be ϕ(x̄)^{𝔦} → ψ(x̄)^{𝔦}, and (∀yθ(x̄,y))^{𝔦} to be ∀y(Dom(y)^{𝔦} → θ(x̄,y)^{𝔦}). For this to define an interpretation, we shall insist that T_{1} ⊢ ∃xDom(x)^{𝔦} and T_{1} ⊢ σ^{𝔦} for every axiom σ ∈ T_{2}. Visser calls such interpretations relative interpretations.

The category of theories and interpretations is obtained by taking theories as objects and such mappings 𝔦 as morphisms, where we choose to say that 𝔣: T_{2} → T_{1} and 𝔤: T_{2} → T_{1} are equal if T_{1} ⊢ ∀x̄(R(x̄)^{𝔣} ↔ R(x̄)^{𝔤}) for all R in ℒ_{2}. This makes a category, where the identity interpretation 1 = 1_{T}: T → T is the morphism given up to this equality by the mapping R(x̄)^{1} = R(x̄) for all R. The composition 𝔤𝔣: T_{3} → T_{1} of morphisms 𝔣: T_{3} → T_{2} and 𝔤: T_{2} → T_{1} is given by (R(x̄))^{(𝔤𝔣)} = (R(x̄)^{𝔣})^{𝔤}, and associativity holds as can easily be checked. (It is somewhat annoying that the convenient notation of writing interpretation-applications as superscripts is at odds with the usual mapson-left convention for morphisms.) As usual, two morphisms 𝔣: T → S and 𝔤: S → T are said to be inverse to each other if 𝔣𝔤 = 1_{S} and 𝔤𝔣 = 1_{T}. An interpretation is then a morphism in this category, i.e., a mapping as described in the last paragraph modulo the equivalence given by this notion of equality.

As for many kinds of interpretations, ours respects derivability in first-order logic because of the way our mappings were defined on non-atomic formulas. Thus we have, Proposition 1. Let 𝔣: T_{2} → T_{1} and suppose T_{2} ⊢ σ. Then T_{1} ⊢ σ^{𝔣}.

The next proposition follows from the definitions just given and an induction on formulas.

Proposition 2. Let 𝔣: T_{2} → T_{1} and 𝔤: T_{2} → T_{1} be equal as interpretations. Then for each formula θ(x̄) of ℒ_{2} we have T_{1} ⊢ ∀x̄(θ(x̄)^{𝔣} ↔ θ(x̄)^{𝔤}). In particular, for each sentence σ of ℒ_{2}, T_{1} ⊢ σ^{𝔣} if and only if T_{1} ⊢ σ^{𝔤}.

3 The Ackermann interpretation

By ZF−inf we mean the theory in the first-order language ℒ_{∈} of set theory with all the usual axioms of ZFexcept infinity, which is negated. More specifically, and following Baratella and Ferro [2], let the set theory ESThave the usual axioms or axiom schemes of extensionality, existence of the empty set, pair set, sum set, separation and replacement^{2}; denote the axiom of power set by Pow, the axiom of foundation, expressed as ∀x(x ≠ ∅ → ∃y ∈ x ∀z ∈ x z ∉ y), by Found; and the usual axiom of infinity, i.e., ∃w(∅ ∈ w ∧ ∀x ∈ w (x ∪ {x} ∈ w)), by Inf. Then ZF−inf is ESTtogether with Pow, Found, ¬Inf.

It was observed in 1937 by Wilhelm Ackermann [1] that ℕ with the membership relation defined by

n ∈ m iff the n^{th} digit in the binary representation of m is 1

satisfies ZF−inf. This interpretation, formalised in ZF with ω in place of ℕ yields a bijection between ω and the collection V_{ω} of hereditarily finite sets.

This interpretation has been given extensive treatment in the literature. Working in PA(or a suitable fragment of PA) one may define the interpretation by setting Dom(x)^{𝔞} to be ‘Dom(x)’, (x = y)^{𝔞} to be ‘x = y’, and (x ∈ y)^{𝔞} to be

∃w < y ∃p ⩽ y ∃r < p ( p = 2^{x} ∧ y = (2w + 1)p + r).

We will refer to this interpretation throughout the rest of the paper as the Ackermann interpretation.

All that is required for this to work is a suitable formula p = 2^{x} that represents ‘p is the x^{th} power of 2’. In fact many such formulas are known which have the necessary inductive definition

1 = 2^{0} ∧ ∀x∀p(p = 2^{x} → 2p = 2^{x+1})  (1)

and partial-function nature

∀x∀p∀q(p = 2^{x}∧ q = 2^{x} → p = q)  (2)

provable in PAor even much weaker systems, including Δ_{0} formulas p = 2^{x} for which the above statements are provable in the subsystem of PAwith induction on Δ_{0} formulas only (see Gaifman and Dimitracopoulos [9] or Hájek and Pudlák [11, §I.1(b)]).

Making extensive use of the axiom scheme of induction, it is straightforward to check that every model of PAwith this binary relation defined satisfies ZF−inf.

Theorem 3. 𝔞: ZF−inf→ PA.

More information on this interpretation in subsystems of PAis given in Section 7 below.

2The axiom scheme of separation is redundant in the presence of replacement.

4 The ordinal interpretation

The finite ordinals in the standard model of ZFCresemble the usual natural numbers. In a world without infinite numbers, one would expect the class of all ordinals to satisfy the ordinary rules of arithmetic.

Definition 4. Trans(x) (‘x is transitive’) is the formula

∀y,z(z ∈ y ∧ y ∈ x → z ∈ x),

and x ∈ On(‘x is an ordinal’) is

Trans(x) ∧ ∀y,z ∈ x (y ∈ z ∨ y = z ∨ z ∈ y).

Most ordinal theory can be done inside our theory of sets just as it is in ZF. See for example Chapter 2 of Drake [7] for details. However, as an easy consequence of ¬Inf, every nonzero ordinal is a successor ordinal—there are no limit ordinals in ZF−inf.

Theorem 5. ZF−inf⊢ ∀x(x ∈ On↔ x = ∅ ∨ ∃y ∈ On(x = y ∪ {y})).

As a corollary, every set of ordinals in ZF−inf has a maximum element.

Corollary 6. ZF−inf⊢ ∀x ⊆ On(x ≠ ∅ → ⋃ x ∈ x).

Arithmetic of ordinals can be defined in the usual way, and there is no problem at all in showing that the ordinals with usual arithmetic yields an interpretation of PAin ZF−inf.

Definition 7. Let Dom(x)^{𝔬} be ‘x ∈ On’, (x = y)^{𝔬} be ‘x = y’, (x < y)^{𝔬} be ‘x ∈ y’, (x + y = z)^{𝔬} be ‘x + y = z’ (ordinal addition), and (x · y = z)^{𝔬} be ‘x × y = z’ (ordinal multiplication).

Theorem 8. 𝔬: PA→ ZF−inf.

Thus PAand ZF−inf have the same consistency strength, but this interpretation is clearly not inverse to the Ackermann interpretation.

5 Epsilon induction and transitive containment

In order to define an inverse to the Ackermann interpretation we shall need to consider the principle of ∈-induction.^{3}

Definition 9. For an ℒ_{∈}-formula ϕ(x,ȳ), I_{∈}ϕ is the sentence

∀ȳ(∀x(∀w ∈ x ϕ(w,ȳ) → ϕ(x,ȳ)) → ∀xϕ(x,ȳ)).

∈-Inddenotes the scheme {I_{∈}ψ : ψ(x,ȳ) is an ℒ_{∈}-formula }.

It turns out that not every model of ZF−inf admits ∈-induction. This is proved using the closely related notion of the transitive closure of a set.

3Further references. The adduction operator previously mentioned gives rise to another scheme of induction

ϕ(∅) ∧ ∀x∀y(ϕ(x) ∧ ϕ(y) → ϕ(x ◁ y)) → ∀xϕ(x), which is said to have originated from Givant and Tarski [10] (cf. Kirby [13, §2]).

Definition 10. Define y = TC(x) (‘y is the transitive closure of x’) to be

y ⊇ x ∧ Trans(y) ∧ ∀y′(y′⊇ x ∧ Trans(y′) → y′⊇ y).

TCis the axiom ∀x∃u ⊇ x Trans(u).

It is easy to check (using extensionality) that the transitive closure y = TC(x) of a set x, if it exists, is unique. The ℒ_{∈}-sentence TCsays that every set is contained in a transitive set. This turns out to be equivalent to the apparently stronger statement that every set has a transitive closure over a weak fragment of ZF−inf, because the transitive closure of a set x can alternatively be defined as the intersection of all transitive sets containing x.

Lemma 11. EST⊢ ∀x(∃y(y ⊇ x ∧ Trans(y)) → ∃y(TC(x) = y)).

Over EST+ Found, the axiom of transitive containment or closure is equivalent to ∈-induction. In fact, a single instance of ∈-induction is enough to prove the whole schema ∈-Ind.

Proposition 12. For all V ⊨ EST+ Found,

V ⊨ ∈-Ind⇔ V ⊨ TC.

Proof. (Sketch.) Let V ⊨ EST∪ ∈-Ind. We prove the equivalent statement

V ⊨ ∀x∃y(y = TC(x))

by ∈-induction on x in V.

Let x ∈ V such that every element of x has a transitive closure. By the axioms of ESTand the induction hypothesis, the set

⋃ {z: ∃x′∈ x (z = TC(x′))} ∪ x

exists and is a transitive superset of x. So Lemma 11 implies x has a transitive closure, completing the induction.

The proof of the converse requires the axiom of foundation but is the same as the standard proof of ∈-induction in ZF. See, for example, Chapter 2 of Drake [7].

The statement TCis not however provable from ZF−inf. We sketch a proof here due to Mancini. (See Mancini and Zambella’s article [15] for more details.)

Theorem 13. ZF−inf∪ {¬TC} is consistent.

Proof. (Sketch.) Consider the hereditarily finite sets (V_{ω} ,∈), and the set of ordinals ω in V_{ω}. Let

ω^{∗} = {{x ∪ {x}} ∈ V_{ω} : x ∈ ω},

the set of singletons of nonzero elements of ω. Define F : V_{ω} → V_{ω} by

F (x) = {x ∪ {x}} and F ({x ∪ {x}}) = x

for x ∈ ω and F (x) = x for x ∉ ω ∪ ω^{∗}. Thus, F is an involution, i.e., a permutation of V_{ω} which is a disjoint product of 2-cycles. Now define the binary relation ∈_{F} by

∀x,y ∈ V_{ω} (x ∈_{F} y ⇔ x ∈ F (y)).

It can be verified that (V_{ω} ,∈_{F}) ⊨ ZF−inf. In addition, (V_{ω} ,∈_{F}) ⊨ ¬TC. In particular,

(V_{ω} ,∈_{F}) ⊨ ¬∃u(u ⊇ ∅ ∧ Trans(u))

since any such set is necessarily infinite.

Thus, one really needs to add the extra hypothesis TCfor the ∈-induction argument to work.

It seems that this result, or ones like it, were known before Mancini and Zambella’s paper. Kunen [14, p149(29)] attributes a result like this to Barwise though this model fails to satisfy the power set axiom, it seems. And Baratella and Ferro [2, p345] point out that the independence of transitive containment relative to other axioms of finite set theory was proved in the context of the Alternative Set Theory by Sochor. They also construct a related model (which they attribute to Kunen) in which transitive containment fails, but one in which the axiom of foundation also fails.

The following easy but important proposition shows that any inverse to the Ackermann interpretation must use TC in some form, even for rather weak systems of arithmetic.

Proposition 14. Let 𝔞: ZF−inf → PAbe the Ackermann interpretation. Then IΔ_{0} ⊢ TC^{𝔞}.

Proof. For x ∈ M ⊨ IΔ_{0}, let y ∈ M be one less than the smallest power of 2 that is bigger than x. (Such a y exists by Δ_{0} induction as there must be a greatest u such that the Δ_{0} formula ∃z ⩽ x 2^{u} = z holds.) If M ⊨ (u ∈ v ∧ v ∈ y)^{𝔞} then u < v < y so the u^{th} binary digit of y is 1.

In other words, 𝔞: ZF−inf+ TC→ PA. If 𝔟: PA→ ZF−inf is inverse to 𝔞 then we would have ZF−inf ⊢ (TC^{𝔞})^{𝔟} hence ZF−inf ⊢ TCby Proposition 2, which is impossible. Thus we must consider the theory ZF−inf^{∗} = ZF−inf+ TCrather than ZF−inf itself.

6 The inverse Ackermann interpretation

Equipped with ∈-induction, we shall obtain an inverse interpretation 𝔟: PA→ ZF−inf^{∗}. The plan is to define a natural bijection 𝔭: V → On between the whole universe and the ordinals. The required interpretation can then be obtained by composing this map with the map 𝔬 defined on On.^{4}

At first, it appears difficult to see how to use ∈-induction at all, since the required inductive definition of 𝔭 is 𝔭(x) = ∑_{y∈x}2^{𝔭(y)}and this seems to need a separate induction on the cardinality of x—just the sort of induction we don’t yet have and are trying to justify. However there is a way round this problem using ordinal summation.

Definition 15. Working in V ⊨ ZF−inf, let 𝒫(On) denote the class of sets of ordinals, and let Σ̂ : On× 𝒫(On) → Onbe the function defined recursively by

Σ̂(0,x) = 0

for all x ∈ 𝒫(On), and

Σ̂(c ∪ \{c\},x) = \{ \begin{matrix}Σ̂(c,x), & if c ∪ \{c\} ∉ x, \\ Σ̂(c,x) + (c ∪ \{c\}), & if c ∪ \{c\} ∈ x \end{matrix}

for all c ∈ Onand x ∈ 𝒫(On). Also, let Σ: 𝒫(On) → Onbe the function defined by

∀x ⊆ OnΣ(x) = Σ̂(⋃ x,x).

4Further references. The inverse Ackermann interpretation is said to have been conjectured to exist in 1964 by Beth [4], and it was found by Mycielski [16] in the same year (cf. Kirby [13, §2]).

Informally, this defines

Σ(x) = ∑_{y∈x}y

for a set of ordinals x, where the summation on the right hand side of the equation refers to ordinal addition. Using induction on the ordinals, it can be proved that both Σ̂ and Σ are class functions definable over ZF−inf. The following definition is the place where TCcomes in.

Definition 16. In V ⊨ ZF−inf^{∗}, define 𝔭: V → Onrecursively by

𝔭(x) = Σ({2^{𝔭(y)} ∈ On: y ∈ x}).

As indicated, 𝔭 is again a class function that can be defined by ∈-recursion on all sets over ZF−inf^{∗}. Informally, in ZF−inf^{∗} we have

𝔭(x) = ∑_{y∈x}2^{𝔭(y)}.

This is precisely the bijection we are looking for.

Proposition 17. ZF−inf^{∗} proves that 𝔭 is a bijective class function V → On.

Proof. The injectivity part is proved by ∈-induction on all sets. The surjectivity part is proved by ∈-induction on the ordinals.

Definition 18. Define a mapping 𝔟 of atomic sentences of arithmetic into set theory by saying Dom(x)^{𝔟} is ‘Dom(x)’, (x = y)^{𝔟} is ‘x = y’, (x < y)^{𝔟} is ‘𝔭(x) < 𝔭(y)’, (x+y = z)^{𝔟} is ‘𝔭(x)+𝔭(y) = 𝔭(z)’, and (x·y = z)^{𝔟} is ‘𝔭(x)×𝔭(y) = 𝔭(z)’, where the target relations and operations of <, + and × are the usual operations on the ordinals.

Theorem 19. 𝔟: PA→ ZF−inf^{∗}.

Proof. This follows from Theorem 8 and Propositions 14 and 17.

It remains to prove the following.

Theorem 20. The interpretations 𝔞: ZF−inf^{∗} → PAand 𝔟: PA→ ZF−inf^{∗} are inverse to each other.

Proof. We must show that 𝔞𝔟 = 1_{PA}and 𝔟𝔞 = 1_{ZF−inf}^{∗}, i.e., that

PA⊢ ∀x̄((σ(x̄)^{𝔟})^{𝔞} ↔ σ(x̄))

and

ZF−inf^{∗} ⊢ ∀x̄((τ(x̄)^{𝔞})^{𝔟} ↔ τ(x̄))

for all atomic formulas σ(x̄) of ℒ_{A} and τ(x̄) of ℒ_{∈}. The details are routine; we make only a few comments on them here.

Note first that both interpretations preserve the logical symbols (they map domains to domains and do not alter equality), thus we need only look at non-logical symbols.

To see 𝔞𝔟 = 1_{PA}, work in PAand write x <′y for (x < y)^{(𝔞𝔟)}, 0′ for the <′-least number, 1′ for the <′-least number not equal to 0′, x +′y for the unique z such that (x + y = z)^{(𝔞𝔟)}, and x ·′y for the unique w such that (x · y = w)^{(𝔞𝔟)}. It can be checked that 0′= 0, 1′= 1, and ∀x x + 1 = x +′1′, and by an induction on y this implies that ∀x,y x + y = x +′y. Since x < y ↔ ∃z y = x + z + 1 and x <′y ↔ ∃z x = y +′z +′1′, it follows that ∀x,y(x < y ↔ x <′y). Similarly x · (y + 1) = (x · y) + x and x ·′(y +′1′) = (x ·′y) +′x, so by induction on y we can show that ∀x,y x · y = x ·′y, as required.

To see 𝔟𝔞 = 1_{ZF−inf}^{∗}, work in ZF−inf^{∗} and write x ∈′y for (x ∈ y)^{(𝔟𝔞)}. Then by ∈-induction we may show ∀x∀y(x ∈ y ↔ x ∈′y) and the result then follows.

7 Fragments of arithmetic and set theory

As with many results for models of Peano arithmetic, the results presented above have hierarchical variations for subsystems of PAand ZF. It seems worthwhile to briefly survey what one can say about this here. Our results along these lines are not really new since they are essentially contained in Ressayre’s Sous-systèmes remarquables de ZF [19].

First, we fix a Δ_{0} formula for p = 2^{x} which defines a partial-function (formula (2) above), and for which the recursive definition (formula (1) above) and its ‘downward’ version,

∀x∀p(p = 2^{x+1} → ∃q(p = 2q ∧ q = 2^{x}))  (3)

are all provable in IΔ_{0}. This latter sentence appears necessary and more than just a convenience. But we cannot think of a natural example where the upward recursion holds but the downward one fails. However, the additional assumption is quite mild, for if a formula θ(x,y) for y = 2^{x} satisfies (1) and (2) provably in IΔ_{0}, then θ(x,y) ∧ ∀u< x ∃v< y θ(u,v) satisfies (1), (2) and (3) provably in IΔ_{0}, as the reader may check.

With such a definition of exponentiation chosen, the domain of definition of the exponentiation operation y ↦ 2^{y} is an initial segment of the model of IΔ_{0}, necessarily closed under successor and addition, but not in general closed under multiplication. We can prove in IΔ_{0} that for each x there is a power of two, 2^{y}, that is greater than x, and in fact there is a least such power of two. With a slight misuse of notation we denote the least y such that 2^{y} > x by logx.

It is fairly straightforward to see that IΔ_{0} proves the Ackermann interpretation of many set theory axioms, including: extensionality; empty set; sum set; foundation; transitive closure; and the negation of the axiom of infinity.

Adding the further arithmetic axiom exp, ∀x∃yy = 2^{x}, stating the totality of the function x ↦ 2^{x} we may prove the Ackermann interpretation of the pair set axiom and the power set axiom. Moreover, expis necessary as well as sufficient for these: to show IΔ_{0} ⊢ Pair^{𝔞} → expand IΔ_{0} ⊢ Pow^{𝔞} → exp, take a number y and 2^{x}, the smallest power of two greater than y. Then as 2^{x} codes the set {x}, by pair set or power set the set {{x},{}} must also be coded, and this code can only be 2^{2^{x}}+1. Thus 2^{2^{x}} exists and so therefore does 2^{y}.^{5}

To study the remaining axioms for set theory, we introduce a hierarchy of formulas related to Lévy’s but more convenient for weak systems where the power set axiom may fail. Say a formula of the language of set theory is Δ_{0}^{𝒫} if it is formed from atomic formulas by boolean operations and bounded quantifiers of the form Qx ∈ y ... and Qx ⊆ y .... A formula is Σ_{n}^{𝒫} (respectively Π_{n}^{𝒫} ) if it is ∃x̄_{1}∀x̄_{2} ... Qx̄_{n} θ (respectively ∀x̄_{1}∃x̄_{2} ... Q^{∗}x̄_{n}θ) where θ is Δ_{0}^{𝒫} . With a symbol for power set, the quantifier Qx ⊆ y ... can be replaced by Qx ∈ 𝒫(y) ... and as the power set of a set x is Π_{1}- definable (in the sense of Lévy) this means that the Σ_{n}^{𝒫} / Π_{n}^{𝒫} hierarchy agrees with the Lévy hierarchy for n ⩾ 2 in the presence of the power set axiom.

With these definitions in place, we can readily prove by induction that IΔ_{0} proves the Ackermann interpretation of the Δ_{0}^{𝒫} -separation axiom scheme, Δ_{0}^{𝒫} –Sep, and for n ⩾ 1, IΣ_{n} proves both Σ_{n}^{𝒫} –Sep^{𝔞} and Π_{n}^{𝒫} –Sep^{𝔞}. Also, using the least number principle we have that IΔ_{0} proves Δ_{0}^{𝒫} –Ind^{𝔞}, the Ackermann interpretation of the Δ_{0}^{𝒫} -epsilon induction axiom scheme

5Further references. As mentioned by Enayat [personal communication], two theories of sets were proved to be equivalent to IΔ_{0} + exp by Gaifman and Dimitracopoulos [9], one of which is the theory of exponentially finite sets.

∀ā(∀y(∀x∈ y θ(x,ā) → θ(y,ā)) → ∀yθ(y,ā))

for θ in Δ_{0}^{𝒫} , and similarly IΣ_{n} proves Σ_{n}^{𝒫} –Ind^{𝔞} and Π_{n}^{𝒫} –Ind^{𝔞}.

The collection and replacement axiom schemes are a little more delicate. Let Σ_{n}^{𝒫} –Collbe the scheme

∀a,c̄(∀x∈ a ∃y θ(x,y,c̄) → ∃b ∀x∈ a ∃y∈ b θ(x,y,c̄))

for θ in Σ_{n}^{𝒫} , etc. To justify the Ackermann interpretation of axioms like this, we need fast growing functions. For example, taking a ⊇ {l − 1} where l = loga and letting θ(x,y) be the Δ_{0} formula y = {x} we trivially have (∀x∈ a ∃y θ(x,y))^{𝔞} in all models of IΔ_{0}, but the code for any b with (∃b ∀x∈ a ∃y∈ b θ(x,y))^{𝔞} must be at least as large as 2^{2^{l−1}} ≈ 2^{a} so exponentiation is required. On the other hand, it is straightforward to see that (Σ_{n}^{𝒫} –Coll)^{𝔞} is provable in IΔ_{0} + exp+BΣ_{n}. Similar remarks apply to the replacement axioms, which we might as well take here to be

∀a,c̄(∀x∈ a ∃y θ(x,y,c̄) → ∃f ∀x∈ a θ(x,f(x),c̄)).

Then (Σ_{n}^{𝒫} –Rep)^{𝔞} is provable in IΣ_{n}, for each n ⩾ 1, but for n = 0 the best result seems to be IΔ_{0}+ exp+BΣ_{1} ⊢ (Δ_{0}^{𝒫} –Rep)^{𝔞}.

The inverse 𝔟 to the Ackermann interpretation is a somewhat more complicated affair, and we make no effort here to even to attempt to say what happens here in the absence of the axioms corresponding to exponentiation, namely pair set and power set. We shall simply state our results, which are based on a straightforward but rather tedious analysis of the proofs given in Sections 4, 5 and 6, and leave the verification to the reader. (The presentation of Kripke–Platek set theory given in Chapter I of Barwise [3] may be found helpful.) It turns out that for the results that follow, the usual Lévy hierarchy (where bounded quantifiers take the form Qx ∈ y ... only) gives the sharpest result. We denote the levels in this hierarchy by Δ_{n}^{L}, Σ_{n}^{L} and Π_{n}^{L}.

The first stage is to define the ordinals, in particular the arithmetic structure on the ordinals, and to define the bijection 𝔭: V → Onbetween the universe and the ordinals. We take as our base theory, the set theory consisting of the axioms of extensionality, empty set, sum set, and the negation of the axiom of infinity, and the axiom schemes of: Δ_{0}^{L}-separation, Δ_{0}^{L}-collection, and both Σ_{1}^{L}-epsilon induction and Π_{1}^{L}-epsilon induction. With this base theory, the class of ordinals is defined (as the transitive sets linearly ordered by ∈) by a Δ_{0}^{L} formula, and the arithmetic operations on the ordinals including +, ×, expare all functions with Δ_{1}^{L} graph. Moreover the scheme of Σ_{1}^{L}-induction proves the axiom of foundation and the axiom of transitive containment, and hence we may define the bijection 𝔭: V → On, also with Δ_{1}^{L} graph, and that this map is inverse to the Ackermann interpretation of sets from the ordinals. The base axioms for arithmetic, i.e., the axioms for nonnegative parts of discretely ordered rings, can then be shown to hold in the ordinals.

To prove the induction scheme we need somewhat stronger axioms showing that the ordinals satisfy IΣ_{n}, etc. Perhaps the simplest option is to take stronger instances of the separation scheme. Given a Σ_{n}-definable subclass A of the ordinals containing 0 and closed under successor, and given n ∈ On, let a be the set of ordinals in A less than n, by Σ_{n}^{L}-separation. Then by ordinal induction a = n so, as n was arbitrary, A = On.

Putting all this together, we have Theorem 21. Let n ⩾ 1 and let Σ_{n}^{L}–Sepdenote the set theory consisting of Σ_{n}^{L}-separation together with base theory Ext, Emp, Sum, ¬Inf, Δ_{0}^{L}–Coll, Σ_{1}^{L}–Ind, and Π_{1}^{L}–Ind. Then the Ackermann interpretation 𝔞 and its inverse 𝔟 are defined for IΣ_{n} and Σ_{n}^{L}–Sep, with

𝔞: Σ_{n}^{L}–Sep→ IΣ_{n}

and

𝔟: IΣ_{n} → Σ_{n}^{L}–Sep

and these are inverse to each other.

Thus, the Ackermann interpretation behaves well for the ‘traditional’ subtheories IΣ_{n} of PA. For weaker theories the pair set and power set axioms behave like the axiom expexpressing the totality of exponentiation.

To close this section, we should remark that for systems of arithmetic without exp, there are other choices of interpretations of set theory. The Ackermann interpretation is of course valid, and in some sense represents the smallest collection of sets or smallest model of set theory one might take, but we could transform a model M of IΔ_{0} to a different model of set theory by taking as sets all bounded Δ_{0}-definable subsets of M, and identifying an a ∈ M with the set of x ∈ M such that M ⊨ (x ∈ a)^{𝔞}. In the (apparent) absence of a formalised notion of truth for Δ_{0} formulas in IΔ_{0} (this itself an open problem) this does not appear to be an interpretation in the formal sense used above. It is essentially the approach taken by Diaconescu and Kirby [6] and, as they point out, counting principles and pigeonhole principles become highly relevant. (It is still not known if IΔ_{0} alone can prove the pigeonhole principle for Δ_{0} functions.) Of course if M ⊨ expthis interpretation and the Ackermann one coincide since

IΔ_{0}+ exp⊢ ∀a∃y∀x< a((x ∈ y)^{𝔞} ↔ θ(x))

for each Δ_{0} formula θ(x), possibly with further parameters.

8 Conclusions for finite set theories and arithmetic

Perhaps the first and most obvious conclusion is that statements concerning the equivalence of ‘Peano Arithmetic’ and ‘ZF with the axiom of infinity negated’ require some care to formulate and prove. It is certainly true that PAand ‘ZF with the axiom of infinity negated’ are equiconsistent for just about any sensible axiomatisation of the latter, in the sense that interpretations exist in both directions.^{6} Probably this is the ‘folklore result’ that most people remember. But for the finer result with interpretations inverse to each other, careful axiomatisation of the set theory is required. A category theoretic framework for interpretations is useful to direct attention to these refinements.

The reader will have noticed that the axiom of choice (AC) has been completely absent from the discussion here. It wasn’t necessary at all for the inverse Ackermann interpretation, though it comes for free with the Ackermann interpretation itself: 𝔞: ZF−inf^{∗}+ AC→ PA. This shows ZF−inf^{∗} ⊢ AC. In fact ACcan be proved in much less than this, as Baratella and Ferro [2] point out.

The universe of hereditarily finite sets has been an important source of analogies, inspiration and axioms for set theory with infinite sets, from the time of Cantor onwards. In the case of the work here we have learnt that models of ZF−inf^{∗} are categorical with respect to their ordinals, in the sense that the model of set theory can be reconstructed from the ordinals as a model of arithmetic. The analogous case for models of full ZFis a result due to Harvey Friedman [8] that characterises ZF+ V = L as the first-order theory extending ZFin which any two models with the same ordinals are isomorphic. (See Friedman’s paper for a precise statement of this result.)^{7}

6Further references. It is mentioned in Kirby’s article [13, §5] that PS(which was proved to be “equivalent” to PAby Previale [17] as previously mentioned) is interpretable in ZF\{Inf} (attributed to Mycielski).

Results like this provide evidence that models of ZFin which V = L holds are actually the ‘uninteresting’ models of ZF, and a similar remark holds for models of finite set theory too. Arguably, the uninteresting models of ZF−inf are the ones in which the axiom of transitive containment holds, and the interesting ones are those for which TC fails. It would be nice to know more about such models, but very few have appeared in the literature. Note that every model M of ZF−inf has a transitive submodel V ⊆ M, V ⊨ ZF−inf+ TC, with the same ordinals, defined to be the image of the function f: On→ V given by the recursion on ordinals

f(x) = {f(y) : On⊨ (y ∈ x)^{𝔞}}.

One way to think about the submodel V ⊆ M is that this is the collection of sets in M with a rank, i.e., they are the sets in the cumulative hierarchy. (Hence the name V we have used for this submodel.)

Whether the theory of models with M ≠ V will have any consequence for arithmetic itself is not clear, as the ordinals in models of ZF−inf+¬TCare of course just the usual models of PA.

Finite set theories in which the axiom of power set fails are an altogether more difficult proposition—apparently for some very good reasons possibly related to the coding problems and complexity theory issues one gets with models of arithmetic without exponentiation.

It is not quite clear to us exactly how this might arise from the point of view of the Ackermann interpretation considered here. However, one view of the inverse Ackermann interpretation in a model M of some fragment of finite set theory is that it sets out to define suitable arithmetic structure for + and · on the whole universe of sets, in a way that is compatible with the Ackermann interpretation that maps ordinals to sets in the cumulative hierarchy V ⊆ M. (V will in general be a subclass of the class of all sets because the transitive containment axiom may fail in M.) But it is clear that if one did have a general process for achieving this, or even for defining + and · on a significant part of the whole universe, this arithmetic model would have to be an end-extension of the image of the ordinals given by the Ackermann interpretation.^{8}

Such a general method for producing end-extensions of models of arithmetic might be very significant for models of IΔ_{0} + ¬exp. There are several open questions concerning when models of IΔ_{0} + ¬exp have end-extensions [28]. More significantly, success in the naïve attempt at producing an inverse Ackermann interpretation would give end-extensions M ⊆_{e} K of M ⊨ IΔ_{0} + ¬exp where each element x ∈ M has an exponential y = 2^{x} ∈ K. Such a construction might be applied in the case when the model of finite set theory is of the type studied by Diaconescu and Kirby [6], that is formed from Δ_{0}-definable bounded subsets. This would in turn have consequences for the Π_{1}-theory of the base model M. In particular this would have consequences for the Π_{1}-theory provable in IΔ_{0} with a single application of exponentiation. This Π_{1}-theory contains some statements not known in IΔ_{0} itself, such as the Δ_{0} pigeonhole principle, and also contains consistency statements such as the tableau consistency of Q, known not to be provable in IΔ_{0} alone. (See for example papers by Pudlák [18], and Paris and Wilkie [27] for much more information.)

7Further references. The first-order theory of ordinals in models of ZFwas studied by Takeuti [21, 22, 23, 24] in a language extending ℒ_{A}.

8Further references. Kirby’s article [13] gives a definition of addition and multiplication on all sets in a model of ZF\{Inf}, which is a apparently not isomorphic to the Ackermann one.

Finally, leaving arithmetic aside, the Axiom of Choice becomes interesting for systems of finite set theory that do not have the power set axiom. Apparently power set is required for the equivalence of the well-ordering principle (WO) and AC, though WO→ AC can be proved by the usual proof without power set. However, we were unable to find a model of AC+ ¬WO.^{9} Using the notation of Baratella and Ferro introduced above, we can ask

Question 22. Does EST+ ¬Inf+ Found⊢ AC?

Note that, as Baratella and Ferro point out, EST+ ¬Inf+ Pow⊢ WOby a straightforward argument mapping sets bijectively onto ordinals. They also provide a model of EST+ ¬Inf+ ¬WO.

References

[1] Ackermann, Wilhelm (1937). Die Widerspruchsfreiheit der allgemeinen Mengenlehre. Mathematische Annalen, 114:305–315.

[2] Baratella, Stefano and Ferro, Ruggero (1993). A theory of sets with the negation of the axiom of infinity. Mathematical Logic Quarterly, 39(3):338–352.

[3] Barwise, Jon (1975). Admissible Sets and Structures: An Approach to Definability Theory. Perspectives in Mathematical Logic. Springer-Verlag, Berlin.

[4] Beth, E. W. (1964). Axiomatique de la théorie des ensembles sans axiome de l’infini. Bulletin de la Société Mathématique de Belgique, 16:127–136. In French. Inaccessible.

[5] Chang, Chen Chung and Keisler, H. Jerome (1977). Model Theory, Studies in Logic and the Foundations of Mathematics, vol. 73. North-Holland Publishing Company, Amsterdam, second edition.

[6] Diaconescu, Radu and Kirby, Laurence A. S. (1987). Models of arithmetic and categories with finiteness conditions. Annals of Pure and Applied Logic, 35(2):123–148.

[7] Drake, Frank R. (1974). Set Theory: An Introduction to Large Cardinals, Studies in Logic and the Foundations of Mathematics, vol. 76. North-Holland Publishing Company, Amsterdam.

[8] Friedman, Harvey (1978). Categoricity with respect to ordinals. In Higher Set Theory: Proceedings, Oberwolfach, Germany, April 13-23, 1977 (Müller, Gert H. and Scott, Dana S., eds.), Lecture Notes in Mathematics, vol. 669, pp. 17–20. Springer-Verlag, Berlin.

9Further references. Zarach [29, §4] proved that if ZF\{Pow} is consistent, then so is (ZF\{Pow}) + AC+ ¬WO. He attributed this to Zbigniew Szczepaniak.

[9] Gaifman, Haim and Dimitracopoulos, Constantine (1982). Fragments of Peano’s arithmetic and the MRDP theorem. In Logic and Algorithmic: Papers from an International Symposium in honor of Ernst Specker held at Eidgenössische Technische Hochschule, Zurich, February 5-11, 1980, no. 30 in Monographies de L’Enseignement Mathématique, pp. 187–206. Université de Genève, Geneva.

[10] Givant, S. and Tarski, A. (1977). Peano arithmetic and the Zermelo-like theory of sets with finite ranks. Notices of the American Mathematical Society, 77T–E51:A–437. Inaccessible.

[11] Hájek, Petr and Pudlák, Pavel (1993). Metamathematics of First-Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin.

[12] Kaye, Richard (1991). Models of Peano Arithmetic, Oxford Logic Guides, vol. 15. Clarendon Press, Oxford.

[13] Kirby, Laurence (2007). Addition and multiplication of sets. Mathematical Logic Quarterly, 53(1):52–65.

[14] Kunen, Kenneth (1980). Set Theory: An Introduction to Independence Proofs, Studies in Logic and the Foundations of Mathematics, vol. 102. North-Holland Publishing Company, Amsterdam.

[15] Mancini, Antonella and Zambella, Domenico (2001). A note on recursive models of set theories. Notre Dame Journal of Formal Logic, 42(2):109–115.

[16] Mycielski, Jan (1964). The definition of arithmetic operations in the Ackermann model. Algebra i Logika Seminar, 3:64–65. In Russian. Inaccessible.

[17] Previale, Flavio (1994). Induction and foundation in the theory of the hereditarily finite sets. Archive for Mathematical Logic, 33:213–241. Inaccessible.

[18] Pudlák, Pavel (1985). Cuts, consistency statements and interpretations. The Journal of Symbolic Logic, 50(2):423–441.

[19] Ressayre, Jean-Pierre (1987). Modèles non standard et sous-systèmes remarquables de ZF. In Modèles non Standard en Arithmétique et théorie des Ensembles, Publications Mathématiques de l’Université Paris VII, vol. 22, pp. 47–147. Université de Paris VII U.E.R. de Mathématiques, Paris.

[20] Świerczkowski, S. (2003). Finite sets and Gödel’s incompleteness theorems. Dissertationes Mathematicae (Rozprawy Matematyczne), 422:1–58.

[21] Takeuti, Gaisi (1954). Construction of the Set Theory from the Theory of Ordinal Numbers. Journal of the Mathematical Society of Japan, 6(2):196–220.

[22] Takeuti, Gaisi (1957). On the Theory of Ordinal Numbers. Journal of the Mathematical Society of Japan, 9(1):93–113.

[23] Takeuti, Gaisi (1958). On the Theory of Ordinal Numbers, II. Journal of the Mathematical Society of Japan, 10(1):106–120.

[24] Takeuti, Gaisi (1965). A Formalization of the Theory of Ordinal Numbers. The Journal of Symbolic Logic, 30(3):295–317.

[25] Tarski, A. and Givant, S. (1987). A Formalization of Set Theory Without Variables, American Mathematical Society Colloquium Publications, vol. 41. American Mathematical Society, Providence. Inaccessible.

[26] Visser, Albert (2004). Categories of theories and interpretations. Logic Group Preprint Series 228, Faculteit Wijsbegeerte, Universiteit Utrecht,

http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint228.pdf.

Published in Logic in Tehran: Proceedings of the Workshop and Conference on Logic, Algebra, and Arithmetic, held October 18-22, 2003 (Enayat, Ali, Kalantari, Iraj and Moniri, Mojtaba, eds.), Lecture Notes in Logic, vol. 26, pp. 284–341. Association for Symbolic Logic, La Jolla, CA, 2006.

[27] Wilkie, Alex J. and Paris, Jeff B. (1987). On the scheme of induction for bounded arithmetic formulas. Annals of Pure and Applied Logic, 35(3):261–302.

[28] Wilkie, Alex J. and Paris, Jeff B. (1989). On the existence of end extensions of models of bounded induction. In Logic, Methodology and Philosophy of Science, VIII (Moscow, 1987) (Fenstad, Jens Erik, Frolov, Ivan T. and Hilpinen, Risto, eds.), Studies in Logic and the Foundations of Mathematics, vol. 126, pp. 143–161. North-Holland Publishing Company, Amsterdam.

[29] Zarach, Andrzej (1982). Unions of ZF^{−} -models which are themselves ZF^{−} - models. In Logic Colloquium ’80 (van Dalen, D., Lascar, D. and Smiley, J., eds.), Studies in Logic and the Foundations of Mathematics, pp. 315–342. North-Holland Publishing Company, Amsterdam.