Invariants, Boolean Algebras and ACA_{0}^{+}

Richard A. Shore^{∗} Department of Mathemcatics Cornell Univeristy Ithaca NY 14853

July 1, 2004

Abstract

The sentences asserting the existence of invariants for mathematical structures are usually third order ones. We develop a general approach analyzing the strength of such statements in second order arithmetic in the spirit of reverse mathematics. We discuss a number of simple examples that are equivalent to ACA_{0}. Our major results are that the existence of elementary equivalence invariants for Boolean algebras and isomorphism invariants for dense Boolean algebras are both of the same strength as ACA_{0}^{+}. This system corresponds to the assertion that X^{(ω)} (the arithmetic jump of X) exists for every set X. These are essentially the first theorems known to be of this proof theoretic strength. The proof begins with an analogous result about these invariants on recursive (dense)Boolean algebras coding 0^{(ω)}.

1 Introduction

We are interested in measuring the complexity of standard mathematical theorems and constructions in various ways. Our two primary approaches are recursion theoretic and proof theoretic. The first is the domain of Recursive Mathematics as in Ershov et al. [1998]. the second is that of reverse mathematics as in Simpson [1999]. The typical theorem to be analyzed is an existence theorem of the form ∀n ∈ ℕ∃m ∈ ℕ … or ∀f ∈ ℕ^{ℕ}∃g ∈ ℕ^{ℕ}. The first corresponds to a function h : ℕ → ℕ and the second to a functional H : ℕ^{ℕ} → ℕ^{ℕ}. From the recursion theoretic point of view, we want to know the complexity of h, or of H (in the sense of measuring the complexity of a witness g relative to that of the given f). In either case, we would like lower and upper bounds on the complexity. The standard measure of (relative) complexity here is that of Turing as given by Turing reducibility and the usual benchmarks along the Turing degrees (the recursive functions, 0; the halting problem, 0′; true arithmetic, 0^{(ω)}; the hyperarithmetic hierarchy to Kleene’s O, etc.). The classical methods of proving high complexity include diagonalization, coding, priority arguments, index set and other hierarchy type theorems.

∗Partially supported by NSF Grant DMS-0100035.

Reverse Mathematics, on the other hand, studies the (proof theoretic) complexity of mathematical theorems by determining the axioms needed to establish them. This involves determining first the appropriate setting for such axioms. The choice is almost always second order arithmetic and one restricts one’s interest to countable, or at least “separable” structures. Next, one must isolate particular systems of axioms in which one can prove (most of) the classical theorems of countable mathematics. The intuition here is that the axiom systems correspond to a hierarchy of construction or existence principles and are usually graded by types of comprehension (i.e. set existence) assertions. Finally, one hopes to give a precise calibration of the complexity of a given theorem by showing that (relative to some weak base theory of arithmetic) it is actually equivalent to the axiom system used to prove the theorem. (This means that over the base theory one can prove the other axioms of the system from the statement of the classical theorem being studied. This reversal of proving “axioms” from “theorems” is the source of the name, Reverse Mathematics.)

In fact, the two approaches are closely connected in both their methods and results with each of the standard systems of reverse mathematics corresponding to one of the classical markers of complexity in recursion theory. Proofs of reversals very often correspond to proofs that any witness for particular instances of the existence theorem in question would compute (in the sense of Turing degree) some degree such as 0′ or O. Proofs of the theorem in the systems often correspond to proofs that solutions can be found that are, e.g. recursive, recursive in 0′, etc. At times both proof theoretic (e.g. conservation results) and model theoretic (e.g. nonstandard models) are used as well. We will list the standard systems of reverse mathematics and explain their recursion theoretic counterparts in the next section. Our goal will then be to explore a type of mathematical classification of structures – the existence of invariants – that often provides central and fundamental theorems and is naturally related to issues of complexity. This type of theorem, however, presents unusual challenges to the subject of reverse mathematics.

Typically, such theorems begin with a class K of structures which we want to classify up to some equivalence relation. The classification is embodied by an assertion of the form that there is an assignment of invariants to members of the class such that two structures have the same invariant if and only if they are equivalent. For this to have some content the invariants (and equality on them) should be somehow simpler than the structures (and the equivalence relation of interest on them). The archetypical equivalence relation is, of course, isomorphism and the invariant is generally viewed as a type of dimension or degree. Standard examples here include vector spaces (dimension) and algebraically closed fields (transcendence degree). Of course, other equivalence relations are studied as well and one looks for invariants up to homotopy, homeomorphism, elementary equivalence or other restricted types of identification of structures. Frequently, the invariants are cardinal numbers corresponding to the size of some sort of basis for the structure. If the structures are countable then these are numbers in ω or ω itself. At other times (e.g. Ulm invariants for p-groups) the analysis of the structures proceeds by some kind of ordinal decomposition and the invariants are then ordinals (below ω_{1} for countable structures). In other situations the invariants may be real numbers or other objects though in the countable case these may be as complicated as the structures themselves and so not provide too much information.

In any case, formalizing the existence of invariants for a class K of even countable mathematical structures is beyond the scope of the setting for Reverse Mathematics. It typically asserts the existence of a functional F from a class K of mathematical structures to the set of invariants such as ℕ, ℵ_{1} etc. that classifies A up to ≡, the equivalence relation of interest, in the sense that F (A) = F (B) ⇔ A ≡ B. Even when the invariants are numbers and K is definable in second order arithmetic this basic assertion of the existence of invariants for K is a third order existential one as F is a map from an uncountable class of countable structures:

(∗) ∃ (F : K → ℕ)(∀A_{1}, A_{2} ∈ K)( F (A_{1}) = F (A_{2}) ⇔ A_{1} ≡ A_{2}).

(We denote this as (∗K, ≡) when we want to make the class and equivalence relation explicit.) Reverse mathematics only allows one to discuss numbers and sets of numbers, not sets of sets of numbers as are needed here. Thus to even begin our analysis we must first find a way to capture the assertion in some second order way.

In the standard direction of proving the existence of invariants there is usually not much to worry about. A classical proof provides an analysis that specifies a particular procedure for identifying the invariant. One can analyze first this procedure as recursive, arithmetic, hyperarithmetic, etc. and then (in terms of axiom systems) the proof that the procedure produces the same invariant for two structures if and only if they are equivalent. Thus, the assertion that this particular procedure works as desired can be proven in some appropriate subsystem Ax of second order arithmetic, and so gives us an upper bound on the (recursion and proof theoretic) complexity of the existence of invariants. Formally, we produce a formula Φ(A, n) of second order arithmetic such that Ax ⊢ ϕ where ϕ is the sentence saying that Φ properly defines the invariant n associated with A:

ϕ : (∀A ∈ K)(∃n ∈ ℕ)Φ(A, n) &
(∀A_{1}, A_{2} ∈ K)(∀n_{1}, n_{2} ∈ ℕ)(Φ(A_{1}, n_{1})&Φ(A_{2}, n_{2}) → (n_{1} = n_{2} ↔ A_{1} ≡ A_{2}).

Here we are assuming that our class K is definable in second order arithmetic and use A ∈ K as an abbreviation for quantification over sets satisfying this definition. Similarly, we are assuming that the equivalence relation ≡ being considered is also definable in second order arithmetic. In all the cases we consider, coding the class of structures of interest in second order arithmetic will be routine and we will simply assume that we have such a coding. The notion of isomorphisms is even easier. That of elementary equivalence will, however, take some care (see Definitions 4.5-4.7).

For example, consider the case where K is the set of countable (and so, without loss of generality, with domain ℕ) vector spaces over the rationals and the equivalence relation of interest is isomorphism. Here the invariant is the dimension and the required definition Φ says that n (possibly ω) is the cardinality of a maximal independent set of vectors. As each of the questions of whether there exists an independent set of size n is at the same level of complexity (Σ_{2}^{0}), arithmetic comprehension (or the iterated Turing jump) is clearly sufficient to produce the answer and so the invariant. (The proof that two vector spaces with the same dimension are isomorphic is even simpler.) Thus we have a sentence ϕ as required above for the class of vector spaces which is provable using arithmetic comprehension (ACA_{0}).

For the reverse direction we need some second order consequence of the existence of invariants that implies the axiom system Ax used to prove the correctness of the particular procedure used in the forward direction. Our proposal is to use the special case of the theorem for countable subclasses of our class of structures. More precisely, we consider the following sentence which will play a central role in our analysis and to which we will refer repeatedly as ψ :

ψ : ∀⟨A_{i}|i ∈ ℕ⟩(∀i(A_{i} ∈ K) → ∃⟨n_{i}|i ∈ ℕ⟩(∀i(n_{i} ∈ ℕ) &∀i, j ∈ ℕ(A_{i} ≡ A_{j} ↔ n_{i} = n_{j}).

(We are again using membership in K as a shorthand for its definition.) This assertion is obviously weaker than the existence of number invariants for the class K. We can now hope to prove that it implies whatever system was used to prove the forward direction of the existence result (in the sense of providing a specific procedure defining the invariant from the structure). In the case of vector spaces over ℚ with isomorphism, it is not difficult to show (Theorem 2.1) that, for this choice of K and ≡, ψ does imply arithmetic comprehension in RCA_{0}, the standard weak base theory of reverse mathematics. Thus we are justified in asserting that the existence of number invariants for isomorphism of countable vector spaces over ℚ is equivalent to arithmetic comprehension (ACA_{0}).

We believe the plan proposed here should be intuitively convincing for the claim that we capture the strength of the existence of invariants by these results (at least for the specific choices of ϕ and ψ that we present). From a recursion theoretic point of view, there will be no difficulty in that we can (and do) show that the procedure for computing the invariant of A is recursive in the recursion theoretic counterpart of Ax (the jump, the ω-jump or the hyperjump of A as the case may be). On the other hand we can (and will) show that for any given set X there are instances of ψ for sequences ⟨A_{i}⟩ recursive in X for which any witness sequence ⟨n_{i}⟩ computes the corresponding jump of X.

For the proof theoretic point of view, however, we should say a few words about the formalities of what types of sentences should be acceptable and where the “mathematical” proofs that ϕ → (∗) and (∗) → ψ take place. The issue here is, as Carl Jockusch pointed out to us, that in the cases of interest all these sentences are theorems of ZFC. What would then prevent us from choosing any theorems of ZFC (expressible in second order arithmetic) as ϕ and ψ. Such choices, of course, would be nonsensical and irrelevant to any claims of capturing the complexity of some instance of (∗). (All the other ingredients in our claim for the equivalence of (∗) and Ax are assertions in second order arithmetic and can take place unproblematically in RCA_{0}.)

First we suggest that any possible dependence on the mathematical content of the assertion be removed by making the implication ϕ → (∗) independent of the choices of K and ≡. Formally we require that

ZF C ⊢ (∀class of structures K)(∀equivalence relation ≡ on K)[ϕ → (∗)]  (1)

where here, of course, we leave A ∈ K in ϕ as a formula of set theory. This seems to be sufficient to support the claim that ϕ is at least as strong as (∗) and is certainly true of the class of sentences that we have proposed as candidates for ϕ.

We should, of course, make the same requirement for the implication (∗) → ψ but this is not sufficient. Here we are asserting that ψ contains some of the strength of (∗) but want to also prove that it is itself strong. We must take care not to allow some theorem of ZFC (not mentioning K or ≡ say) as a candidate that itself proves Ax without any connection to (∗). Indeed the sentence ψ that we have proposed to use is a theorem of ZFC for every K and ≡ . (As there are only countably many A_{i} there are only countably many equivalence classes, and so we can number them accordingly.) Thus our worry here is that the strength asserted for ψ has no connection to its dependence on (∗) but is induced by the use of comprehension in ZFC. To eliminate this possibility we require that the proof that (∗) → ψ take place in a version of set theory with very limited comprehension. A very strong version of this proposal is that the implication be provable in rudimentary set theory. This is the system B_{0}^{set} of Simpson [1999, VII.3] whose only axioms are extensionally, infinity and that the universe is closed under the rudimentary operations which are essentially the standard ones for the primitive recursive functions on ℕ without the recursion scheme. This system corresponds to Δ_{0} comprehension (see Jensen [1972]) so no application of comprehension in the metatheory can be the source of the strength of ψ. Rather, the only source of the power of comprehension is the existential assertion of (∗) itself. For our proposed ψ, it is clear that the implication (∗) → ψ is provable with only Δ_{0} comprehension. It only asserts the existence of the composition of two given functions – F given by (∗) and the one from ω → ω corresponding to the given sequence ⟨A_{i}⟩ – and so is easily seen to exist by Δ_{0} comprehension. A final desideratum for ψ might be that the axiom system Ax claimed to be of the same strength as (∗) also prove ψ (all for the same choice of K and ≡, of course).

Thus we will be willing to claim that the existence of invariants for some K and ≡ has the same strength as an axiom system Ax (of second order arithmetic) if we have formulas ϕ(K, ≡) and ψ(K, ≡) (both of third order arithmetic or its set theoretic analog but with the only nonsecond order atomic subformulas being of the form A ∈ K and A_{1} ≡ A_{2} and no third order quantification allowed) such that RCA_{0} ⊢ Ax → ϕ and RCA_{0} ⊢ ψ → Ax (both with appropriate definitions replacing the occurrences of K and ≡), Ax ⊢ ψ, ZF C ⊢ (∀class of structures K)(∀equivalence relation ≡ on K)[(∗) → ϕ] and B_{0}^{set} ⊢ (∗) → ψ.

Now that we have an approach to analyzing the strength of the existence of invariants for different classes of structures we can consider particular classes of interest. As we have indicated, the case of vector spaces is easily seen to be equivalent to the standard system ACA_{0} (Theorem 2.1). The situation is the same for algebraically closed fields (Theorem 2.2). Our goal here is to consider a class that presents a second challenge to the standard approach of reverse mathematics by being provably equivalent to an axiomatic system that lies strictly between two of the standard systems. The class of structures that we analyze is that of Boolean algebras. Now the isomorphism relation for arbitrary Boolean algebras is Σ_{1}^{1} complete (see §3) so no simply defined invariants for isomorphism can exist. Indeed, the existence of invariants for isomorphisms, even for countable sequences of structures in the sense of ψ, implies Π_{1}^{1} − CA_{0}, the system of reverse mathematics corresponding to the existence of Kleene’s O (or equivalently the hyperjump). On the other hand, Π_{1}^{1} − CA_{0} is enough to prove ψ for isomorphism for any class K. However, it is a classical result of Tarski [1949] (see Monk [1989, 18] or Goncharov [1997, 2.3]) that there are number invariants for elementary equivalence of Boolean algebras. Our goal is to prove (Theorem 6.10) that the existence of any number invariants, in the sense of (∗), is equivalent (over RCA_{0}), in the sense of our analysis above in terms of ϕ and ψ, to an axiom system ACA_{0}^{+} that is intermediate between two of the standard systems, ACA_{0} and ATR_{0}. We believe that this is the first real example of a theorem known to be equivalent to ACA_{0}^{+}. This system corresponds to the existence of the arithmetic jump, A^{(ω)}, for each set A and the recursion theoretic version of our main theorem (Theorem 5.10) is that determining the elementary invariants for recursive Boolean algebras is of the same complexity (in the sense of Turing degree) as 0^{(ω)}.

Some might say that the use of the logical notion of elementary equivalence is the source of the problem and that it alone might require ACA_{0}^{+}. Indeed, one must be careful to develop a reasonable notion of elementary equivalence that makes sense in RCA_{0}. Following the approach to satisfaction from Simpson [1999], we do this in Definitions 4.5-4.7. Another objection might stem from a possible general aversion (which we do not share) to logical notions as the proper objects of study for reverse mathematics. This concern can be alleviated by noting that these invariants are, in fact, isomorphism invariants for an algebraically defined subclass of Boolean algebras. These are the dense Boolean algebras as presented in Goncharov [1997]. The required algebraic notions are given in Definitions 4.1-4.3. Intuitively these algebras play the same role for Boolean algebras that dense linear orderings play for linear orderings. The prime example is the atomless Boolean algebra but there are, of course, countably many others. (From the logical or model theoretic point of view these are just the saturated countable Boolean algebras.) We will show that the existence of isomorphism invariants for this class also implies the existence of the ω-jump, and so has the same strength as the existence of elementary equivalence invariants for all countable Boolean algebras. These results will be Theorems 5.10 and 5.19 for the recursion theoretic version and Theorems 6.6 and 6.9 for the reverse mathematics one.

2 Axiom Systems and Examples

All our axiom systems for reverse mathematics are phrased in terms of the language of second order arithmetic, that is the usual first order language of arithmetic augmented by set variables and the membership relation ∈. Each system also contains the standard basic axioms for +, · and < (which say that N is an ordered semiring). In addition, they all include one of two forms of induction. The first form is the full induction scheme I.

(I) φ(0) ∧ ∀n(φ(n) → φ(n + 1)) → ∀nφ(n), for every formula . The other form of induction that we consider is an axiom that permits the application of induction only to sets (that one knows to exist):

(I_{0}) 0 ∈ X ∧ ∀n(n ∈ X → n + 1 ∈ X) → ∀n(n ∈ X).

We call the system consisting of (I) and the basic axioms of ordered semirings P. If we replace (I) by (I_{0}), we call the system P_{0}. In general, if we have any system S containing (I), we denote by S_{0} the system in which (I) is replaced by (I_{0}) . All the systems we shall consider will be defined by adding various types of set existence axioms to P or P_{0}. We begin with a base theory strong enough to do basic arithmetic and elementary combinatorics.

(RCA): RCA, for recursive comprehension axiom, is a system just strong enough to prove the existence of the recursive sets but not of ∅′ nor indeed of any nonrecursive set. In addition to P its axioms include the schemes of Δ_{1}^{0} comprehension and Σ_{1}^{0} induction:

(Δ_{1}^{0} − CA_{0}) ∀n(φ(n) ↔ ψ(n)) → ∃X∀n(n ∈ X ↔ φ(n))

for all Σ_{1}^{0} formulas φ and Π_{1}^{0} formulas ψ in which X is not free.

(Σ_{1}^{0} − I)(φ(0) ∧ ∀n(φ(n) → φ(n + 1)) → ∀nφ(n))

for all Σ_{1}^{0} formulas φ.

The next system says that every infinite binary tree has an infinite path. It is connected to the low basis theorem of recursion theory which says that every such tree has an infinite path whose jump is recursive in that of the tree itself.

(WKL): WKL, for weak König’s lemma, asserts, in addition to RCA, that every infinite subtree of 2^{<ω} has an infinite path.

We next move up to arithmetic comprehension.

(ACA): ACA, for arithmetic comprehension axioms, consists of P plus the comprehension scheme for arithmetic formulas:

(ACA) ∃X∀n(n ∈ X ↔ φ(n)) for every arithmetic formula φ in which X is not free.

In recursion theoretic terms, ACA_{0} proves the existence of ∅′ and by relativization it proves and, in fact is equivalent to, the existence of X′ for every set X. The next system corresponds to the existence of all (relativized) H-sets, i.e. the existence of the H_{e}^{X} (and so the hyperarithmetic hierarchy up to e) for each e ∈ O^{X} for every set X.

(ATR): ATR, for arithmetical transfinite recursion, consists of P plus the assertion that arithmetic comprehension can be iterated along any countable well ordering.

(ATR) If X is a set coding a well ordering <_{X} with domain D and Y is a code for a set of arithmetic formulas φ_{x}(z, Z) ( indexed by x ∈ D) each with one free set variable and one free number variable, then there is a sequence ⟨K_{x}|x ∈ D⟩ of sets such that if y is the immediate successor of x in <_{X}, then ∀n(n ∈ K_{y} ↔ φ_{x}(n, K_{x})) and if x is a limit point in <_{X} then K_{x} is ⊕{K_{y}|y <_{X} x}.

The systems climbing up to full second order arithmetic (i.e. comprehension for all formulas) are classified by the syntactic level of the second order formulas for which we assume a comprehension axiom.

(Π_{n}^{1}-CA): Π_{n}^{1}-CA, for Π_{n}^{1} comprehension axiom, is the system P plus comprehension for Π_{n}^{1} formulas:

(Π_{n}^{1}-CA) ∃X∀k(k ∈ X ↔ φ(k)) for every Π_{n}^{1} formula φ in which X is not free.

The recursion theoretic equivalent of the simplest of these systems, Π_{1}^{1} − CA, is the existence of O^{X}, the hyperjump of X, for every set X. Together with the four systems listed above, it makes up the standard list of axiomatic stems of reverse mathematics. Almost all theorems of classical mathematics whose proof theoretic complexity has been determined have turned out to be equivalent to one of them.

As simple examples of our approach to invariants, we now analyze the existence of number invariants for isomorphism of vector spaces over a fixed field and algebraically closed fields of fixed characteristic.

Theorem 2.1 Let F be a field and V the class of countable vector spaces over F. The existence of number invariants for the isomorphism relation on V, (∗V, ≅), is of the same complexity as ACA_{0}. This is also true if we restrict our class to vector spaces of any fixed set of dimensions as long as the set has cardinality at least 2.

Proof. Our formula says that V has dimension n − 1 for n > 0 and ∞ for n = 0:

ϕ(V, n) : [n > 0 & ∃⟨x_{2}, … x_{n}⟩ ∈ V^{n−1}∀⟨c_{2}, … c_{n}⟩ ∈ F^{n−1}(c_{2}x_{2} + … c_{n}x_{n} = 0 ⇔
c_{2} = … c_{n} = 0) & ¬∃⟨x_{1}, … x_{n}⟩ ∈ V^{n}∀⟨c_{1}, … c_{n}⟩ ∈ F^{n}(c_{1}x_{1} + … c_{n}x_{n} = 0 ⇔
c_{1} = … c_{n} = 0) ] ∨ [ n = 0 & ∀m[∃⟨x_{2}, … x_{m}⟩ ∈ V^{m−1}∀⟨c_{2}, … c_{m}⟩ ∈ F^{m−1}(c_{2}x_{2} + … c_{m}x_{m} = 0 ⇔
c_{2} = … c_{m} = 0)].

One can easily develop enough of the usual theory of vector spaces in ACA_{0} to prove that every vector space has a unique dimension (in this sense) and that any two of the same dimension are isomorphic. (See Simpson [1999, III.4 for a sketch and Friedman, Simpson and Smith [1983] for more details.) For the other direction, consider any two dimensions n < m and the class K of vector spaces with dimensions in A with n, m ∈ A (where we allow ∞ as a value of m for the countable vector space of largest dimension). We need to build a sequence V_{i} of vector spaces such that any witness to ψ will compute 0′ (and so, by relativization, ψ implies the existence of X′ for every X). We take V_{0} and V_{1} to be fixed spaces of dimension n and m, respectively. We define the rest of the V_{i} uniformly recursively so that we build V_{i} as a space of dimension n until we see that i ∈ 0′ at which point we start extending the space so that at the end it will have dimension m. Now if ⟨n_{i}⟩ is any witness for ⟨V_{i}⟩ as required by ψ, it is clear that, for i > 1, i ∈ 0′ ⇔ n_{i} = m. □

Theorem 2.2 Let A be the class of countable algebraically closed fields of characteristic p. The existence of number invariants for the isomorphism relation on A, (∗A, ≅), is of the same complexity as ACA_{0}. This is also true if we restrict our class to fields of any fixed set of transcendence degrees as long as the set has cardinality at least 2.

Proof. The proof is the same as for vector spaces except that we replace linear (in)dependence by algebraic (in)dependence (over the prime field). □

We next introduce the system ACA^{+} that captures the instances of the existence of elementary invariants for Boolean algebras that we analyze. Recursion theoretically, it corresponds to the existence of the arithmetic (or ω) jump of X for every set X.

(ACA^{+}): ∀X∃A(A^{[0]} = X & (∀n)[A^{[n+1]} = (A^{[n]})′].

As an axiomatic system in reverse mathematics ACA^{+} was first studied in Blass, Hirst and Simpson [1987]. They proved in RCA_{0} that Hindman’s theorem implies ACA_{0} and is implied by ACA_{0}^{+}. The precise strength of this theorem is still open. We do not know of any other theorems that are even candidates for equivalence with ACA_{0}^{+}. (We are leaving out uniform infinite versions of theorems that are each equivalent to ACA_{0} such as Ramsey’s theorem for n-tuples, RT_{2}^{n}. Each one for n ≥ 3, is equivalent to ACA_{0} in such a way that the assertion that for any sequence F_{n} of colorings of n-tuples there is a sequence H_{n} so that each H_{n} is homogeneous for F_{n} is equivalent to ACA_{0}^{+}.)

3 Boolean Algebras

We take the standard definition of the class B of Boolean algebras B with constants 0 and 1 and operations ∨, ∧ and ¬. For convenience we also use the (Δ_{0}) defined relation ≤ and function −: x ≤ y ⇔ x ∧ y = x and x − y = x ∧ ¬y. A general reference for information about Boolean algebras is Monk [1989].

As we mentioned in the introduction, the isomorphism problem for Boolean algebras is Σ_{1}^{1} complete, and so has no reasonable notion of invariant. In fact, there is a single recursive Boolean algebra B (the Harrison Boolean algebra) such that for any Σ_{1}^{1} formula Ω(n) there is a recursive sequence of algebras B_{n} such that Ω(n) ↔ B_{n} ≅ B. (This result is presumably folklore.() A proof for the analogous statement about linear orderings can be found in White [2000, 5.4]. The result for Boolean algebras follows by taking the interval algebras (Definition 5.3) of the linear orderings constructed there.) Thus the existence of invariants even for all countable sets of Boolean algebras up to isomorphism, i.e. ψ for B and ≅ implies Π_{1}^{1} − CA_{0}. Of course, ψ is provable in Π_{1}^{1} − CA_{0} for any (definable) class K of structures as isomorphism is a Σ_{1}^{1} relation. Thus there is not much to say about isomorphism invariants for arbitrary classes of Boolean algebras. We will investigate a coarser relation – elementary equivalence – on all Boolean algebras and isomorphism restricted to a subclasses of Boolean algebras – the “dense” Boolean algebras.

Tarski [1949] showed that there are only countably many completions T_{i} of the theory T of Boolean algebras and they are uniformly axiomatizable. Thus the theory of Boolean algebras is decidable. This, of course, supplies number invariants for elementary equivalence of countable Boolean algebras in the sense of (∗): F(A) = i ⇔ A ⊧ T_{i} and so F(A) = F(B) ⇔ A ≡ B. Our tasks are now first to analyze a proof of this theorem to see that we can define this relation Φ(A, i) and prove in ACA_{0}^{+} that it has the properties described in ϕ. For the reversal we want to construct a uniformly recursive sequence B_{i} of Boolean algebras so that any witness function assigning them number invariants for elementary equivalence in the sense of ψ computes 0^{(ω)}. Together these will prove our main result:

Theorem 6.10: The existence of number invariants for elementary equivalence of countable Boolean algebras or for isomorphism of dense countable Boolean algebras has the same complexity in the sense of reverse mathematics as ACA_{0}^{+}.

We begin with a series of definitions that are needed just to describe the theories T_{i} and the Tarski invariants.

Definition 3.1 Let a be an element of a Boolean algebra B. a is an atom if and only if 0 < a but ¬∃x(0 < x < a). The set of atoms of B is denoted by At(B). The element a is atomic if and only if ∀x ≤ a∃z ≤ x(x ≠ 0 → z is an atom). It is atomless if and only if no x ≤ a is an atom.

Now Tarski’s analysis of a Boolean algebra B proceeds by taking successive quotients by uniformly defined ideals much the way the Cantor-Bendixson analysis of a topological space or a Boolean algebra works (Monk [1989, 6]. The difference is that the Cantor-Bendixson analysis uses at each step the ideal generated by atoms. Now, Tarski’s analysis uses a larger ideal. We follow the analysis as in Monk [1989, 7] which is very neat or Goncharov [1997] which is more constructive, and so often better suited to our purposes. We refer to these sources for many basic algebraic facts. For example, the ideal we want is generated by the atomic and the atomless elements. That it can also be defined via single joins is 2.2.1 of Goncharov [1997].

Definition 3.2 For B a Boolean algebra, I(B) = {x ∈ B| ∃y, z(y is atomic & z is atomless & x = y ∨ z}. We let B′ = B/I(B). We call B′ the Tarski derivative of B.

We now define the sequence of Boolean algebras constructed by successively taking quotients by this ideal.

Definition 3.3 Given a Boolean algebra B we define a sequence B^{[n]} of Boolean algebras and a sequence I_{n} of ideals of B as follows: B^{[0]} = B; B^{[n+1]} = B^{[n]}/I(B^{[n]}). The canonical embeddings are given by π_{m,n} : B^{[m]} → B^{[n]} for m ≤ n. We denote π_{0,n} by π_{n}. The desired sequence of ideals of B is given by I_{0}(B) = {0}, I_{n+1}(B) = π_{n}^{−1}[I(B^{[n]})] so B^{[n]} ≅ B/I_{n}(B).

We can now define the elementary invariants for Boolean algebras as a triple of natural numbers or symbols −1, ∞ encoding the level at which this process stops and the type of the final nonzero algebra produced.

Definition 3.4 The invariant of the Boolean algebra B, inv(B), is a triple of numbers (or symbols −1, ∞):

1. inv(B) = ⟨−1, 0, 0⟩ if B = {0};

2. inv(B) = ⟨∞, 0, 0⟩ if ∀i(B^{[i]} ≠ {0});

3. inv(B) = ⟨k, l, m⟩ if

(a) B^{[k]} ≠ {0}, B^{[k+1]} = {0},

(b) l = min{∞, ∥At(B^{[k]})∥},

(c) m = 0 if B^{[k]} is atomic and m = 1 otherwise.

We denote the entries of this triple by inv_{i}(B) for i = 1, 2, 3.

Tarski showed that these invariants characterize all Boolean algebras up to elementary equivalence Theorem 3.5 (Tarski [1949]) For all Boolean algebras B and A, B ≡ A ⇔ inv(B) = inv(A).

We now wish to argue that we can prove the existence of the map inv as a definable procedure and the fact that it characterizes elementary equivalence in ACA_{0}^{+}. It should be clear that in ACA_{0} we can show for every Boolean algebra B that At_{0}(B), the sets of atomic and atomless elements of B, I(B), B/I(B) and the canonical map π : B → B/I(B) all exist. The sequence of these predicates and maps over all n, however, do not obviously provably exist in ACA_{0}. Indeed, even the existence of all “finite” initial segments of these sequences does not seem to be provable in ACA_{0} although the existence for the sequences of length n are, of course, provable for all n in ACA by induction. This will be an important issue in our consideration of reversals but for now it is sufficient to note that all these (even infinite) sequences of subsets of B provably exist in ACA_{0}^{+}. The point is that they are all uniformly recursive in B^{(ω)}. Thus the map inv is recursive in B^{(ω+1)}. (We need to quantify over the sequences B^{[n]}, I_{n} to check if inv_{1}(B) = ∞. Otherwise, we just need to check the individual B^{[n]} for their cardinality and atomicity and each one is recursive in a finite (in the model) number of jumps, and so in B^{(ω)} (in the model). Thus we can define inv and prove that the definition defines a function in ACA_{0}^{+}.

To finish the proof of Theorem 3.5 in ACA_{0}^{+} we have to define elementary equivalence, ≡, and go through a suitable proof. Again in, say RCA_{0}, the definition of ≡ is delicate and we will deal with it more carefully when we prove the reversals in Definitions 4.5-4.7. For now, it is straightforward to check that any reasonably constructive standard inductive definition of satisfaction for a structure A for a recursive language L can be carried out uniformly recursively in A^{(ω)}, and so we can adopt the standard definition of ≡ as A ≡ B ⇔ ∀ρ ∈ L(A ⊧ ρ ↔ B ⊧ ρ). The proof of Tarski’s theorem itself requires some care. The most commonly found proofs (as in Chang and Keisler [1977, 5.5.10] or Monk [1989, 18] use saturated or special models of some sort that rely on the existence of uncountable cardinals. Tarski’s original proof (according to Doner and Hodges [1988]) was a quantifier elimination proof in an expanded language and presumably the most constructive of them all. For the purposes of our argument in ACA_{0}^{+}, the easiest route to follow is the one done in detail in Goncharov [1977, 2.3], as it can be straightforwardly carried out in ACA_{0}^{+} . It is also the one defining the dense Boolean algebras and explicitly dealing with the isomorphism problem for that class. We now turn to these matters and the proof of Tarksi’s theorem in ACA_{0}^{+}.

4 Dense Boolean algebras

We begin with the analog of our invariants for individual elements and formal definitions in the language of Boolean algebras of the predicates we will use to describe the sequences of algebras and ideals of Definition 3.3. These will be the key ingredients in the proof of existence of isomorphism invariants for the dense Boolean algebras and the associated proof of Tarski’s theorem.

Definition 4.1 The invariant, inv(a) (or inv_{B}(a), if we need to make B explicit), of an element a of the Boolean algebra B is a triple of numbers (or symbols −1, ∞):

1. inv(a) = ⟨−1, 0, 0⟩ if a = 0;

2. inv(a) = ⟨∞, 0, 0⟩ if ∀i(a ∉ I_{n})

3. inv(a) = ⟨k, l, m⟩ if

(a) a ∉ I_{k}, a ∈ I_{k+1},

(b) l = min{∞, ∥{x ∈ At(B^{[k]}) & x ≤ a}∥

(c) m = 0 if in B^{[k]} there are no nonzero atomless elements below a and m = 1 otherwise.

We denote the entries of this triple by inv_{i}(a) for i = 1, 2, 3. Note that inv(B) = inv_{B}(1).

Definition 4.2 We define unary predicates I_{n},A_{n}, B_{n} and C_{n} and the associated formulas in the language of Boolean algebras that characterize them by induction:

I_{0}(x) ⇔ x = 0;

A_{0}(x) ⇔ ¬I_{0}(x) & (∀y ≤ x)(y = 0 ∨ y = x);

B_{0}(x) ⇔ (¬∃y ≤ x)(A_{0}(y));

C_{0}(x) ⇔ (¬∃y ≤ x)(¬I_{0}(y) ∧ B_{0}(y)).

I_{n+1}(x) ⇔ ∃y, z(B_{n}(y) & C_{n}(z) & x = y ∨ z);

A_{n+1}(x) ⇔ ¬I_{n+1}(x) & (∀y ≤ x)(I_{n+1}(y) ∨ I_{n+1}(x − y) );

B_{n+1}(x) ⇔ (¬∃y ≤ x)(A_{n+1}(y));

C_{n+1}(x) ⇔ (¬∃y ≤ x)(¬I_{n+1}(y) ∧ B_{n+1}(y)).

We note that these formulas I_{n}, A_{n}, B_{n} and C_{n} are equivalent (by prenexing rules) to a recursive list of formulas which are Σ_{4n}, Π_{4n+1}, Π_{4n+2} and Π_{4n+3}, respectively. It is proven in Goncharov [1997, 2.2] that they define the notions of being in I_{n}, an atom of B^{[n]}, atomless in B^{[n]} and atomic in B^{[n]}, respectively. There is no problem in carrying out his proofs in ACA_{0}^{+}. Thus in ACA_{0}^{+} we can extend B to a structure with these predicates for all n. In particular, in ACA_{0}^{+} we can prove that if A ≡ B then inv(A) = inv(B).

To prove the converse, that inv does determine elementary type, we continue to follow Goncharov [1997, 2.3] by defining dense Boolean algebras and noting some of their properties.

Definition 4.3 A Boolean algebra B is dense if ∀b ∈ B∀k ∈ ω

1. k < inv_{1}(b) ⇒ ∃a ≤ b(inv(a) = ⟨k, ∞, 0⟩) and

2. inv_{1}(b) = ∞ or inv_{2}(b) = ∞ ⇒ (∃a ≤ b) [inv_{1}(a) = inv_{1}(b) = inv_{1}(b − a) & inv_{2}(a) = inv_{2}(b) = inv_{2}(b − a)].

We denote by DB the class of dense Boolean algebras.

Goncharov [1997, 2.3] proves that every countable Boolean algebra has an elementary extension B^{∗} which is dense and that any two countable dense Boolean algebras with the same invariant are isomorphic. This then shows that any two countable Boolean algebras with the same invariant are elementary equivalent, and so establishes Tarski’s theorem. (For uncountable Boolean algebras it follows from the countable case by the downward Skolem-Löwenheim theorem and the fact mentioned above that the value of inv is determined by the elementary theory of a Boolean algebra.)

Given B, the construction of a dense elementary extension B^{∗} proceeds by building an ascending chain of algebras each satisfying the complete elementary diagram of B (with constants for all its elements) and adding on the witnesses needed in the definition of density as one goes along. The existence of the required extension at each step follows from a compactness argument that depends on the existence of witnesses for any finite subset of conditions in the original algebra based only on the characteristic of the given b. The existence of these witnesses is proven using only arithmetic comprehension once one has the existence of B^{(ω)} (to supply the elementary diagram of B). Of course, the compactness theorem holds in ACA_{0} as well. Thus the existence of the desired chain can always be proven in ACA_{0}^{+}. Each element in this chain is a model of the complete diagram of B, and so an elementary extension of B as is its union B^{∗} (again all this is provable in ACA_{0}^{+} ). As all the required witnesses for density were put in along the way, B^{∗} is dense, and so it is the required extension of B.

The proof that any two countable dense Boolean algebras A and B with the same characteristic are isomorphic proceeds by considering the relation

S = {(a, b) ∈ A × B|inv_{A}(a) = inv_{B}(b) & inv_{A}(¬a) = inv_{B}(¬b)}

and proving that S satisfies the Vaught Criterion [1954] (as described in Goncharov [1997, 1.5]) for carrying out the back and forth argument needed to prove isomorphism of the Boolean algebras. The existence of S follows from the existence of the function inv (as characterized in Definition 4.2) and ACA_{0} and so from ACA_{0}^{+}. That it satisfies the Vaught Criterion follows from density in ACA_{0} (given the existence of the function inv on A and B). The construction of the isomorphism from S is the usual back and forth argument that can be carried out in ACA_{0}. Thus the following results are provable in ACA_{0}^{+}:

Theorem 4.4 (ACA_{0}^{+}) For Boolean algebras A and B, A ≡ B if and only if inv(A) = inv(B). Moreover, if A and B are dense then A ≅ B if and only if inv(A) = inv(B).

For the sake of our eventual reversal results in RCA_{0} we will reconsider these arguments in ACA_{0} for algebras with inv_{1} = k < ∞ under assumptions that allow us to make sense in RCA_{0} or ACA_{0} of the notion of elementary equivalence for the structures we will consider. We begin with our promised treatment of satisfaction and elementary equivalence in RCA_{0} (or at least ACA_{0}). We model our definitions on Simpson’s [1999, II.8.9] notion of a weak model. The notion of a structure for a language (having a domain and functions and relations interpreting the appropriate symbols of the language) is standard. The interpretation of variable free terms in the structure and satisfaction for atomic sentences are defined as usual (using recursion) in RCA_{0}.

Definition 4.5 (RCA_{0}) If A is a structure for a language L (with equality) and S is a set of sentences of L_{A} (L expanded by constants \underline{a} for all elements a of A) containing the atomic sentences of L_{A} which is closed under propositional combinations and substitution instances (by variable free terms of L_{A}) of subformulas then F : S → {0, 1} is a (partial) truth assignment for A (defined on S) if the following hold for any formulas σ, τ in S:

1. If σ is atomic then F [σ] = 1 ⇔ A ⊧ σ.

2. F [¬σ] = 1 − F [σ] for any σ ∈ S.

3. F [σ&τ] = 1 ⇔ F [σ] = 1 and F [τ] = 1.

4. F [∃xσ(x)] = 1 ⇔ (∃a ∈ A)(F [σ(\underline{a})] = 1).

Of course, given two assignments F and F′ for a structure A defined on sets S and S′ respectively, it is easy to prove by induction in RCA_{0} that the two assignments agree on S ∩ S′. Thus we can define the (partial) satisfaction function.

Definition 4.6 For a structure A and sentence σ of its language L we set the ( partial) satisfaction function Sat(A, σ) = i ∈ {0, 1} if there is a truth assignment F for A such that F [σ] = i and let it be undefined otherwise.

Definition 4.7 (RCA_{0}) Two structures A and B for a language L are elementary equivalent, A ≡ B, if, for every sentence σ of L, Sat(A, σ) = Sat(B, σ) in the sense that, if either is defined, they are both defined and equal.

It is now immediate that ≡ an equivalence relation coarser than isomorphism

Proposition 4.8 (RCA_{0}) If A ≅ B then A ≡ B.

In ACA_{0}^{+} there is always a truth assignment on S_{ω}, the set of all sentences, and it and our definition of ≡ agree with the usual notions. Indeed, in ACA we can prove by induction that there is a truth assignment to the sets S_{n} consisting of all sentences of L_{A} of quantifier depth at most n. Thus the notions of satisfaction and elementary equivalence also have their usual properties in this system as well. In ACA_{0} alone however, we cannot prove that Sat is defined on all sentences for all structures. (This requires the existence of A^{(n)} for every n which follows from either ACA_{0}^{+} or ACA.) We can, however, hope to build specific structures A (e.g. decidable ones) for which we can prove that Sat is defined for all σ ∈ L. This is the course we will follow in our reversal argument for Boolean algebras.

The crucial notions are the predicates I_{n}, A_{n}, B_{n} and C_{n} (for n ≤ inv_{1}(B)), as defined above. We want to consider Boolean algebras B for which we can extend the structure to include the predicates I_{n}, A_{n}, B_{n} and C_{n} (for n ≤ inv_{1}(B)) so as to satisfy the formulas of Definition 4.2. Given a Boolean algebra in the extended language which satisfies these axioms, we can prove in ACA_{0} that they correctly represent the associated notions, and so define the invariant of each element of the algebra. In the other direction, given a function h on B we can use these predicates and axioms to characterize the requirements for h be the function inv_{1} (or inv) as in Definition 6.4. Although we will not need it here, it is possible to prove in ACA_{0} that there is a total satisfaction function (even in the extended language) for algebras with such predicates (or functions) defined on them. It is uniquely determined by the 1-quantifier theory in the extended language. (All this would follow from the appropriate quantifier elimination result underlying Tarski [1949] or the one for model completeness in Ershov [1964].) One can also prove that the algebras have dense elementary extensions (which necessarily have the same invariant). Moreover, the proof of Goncharov [1997, 2.3] discussed above, that two dense Boolean algebras of the same characteristic are isomorphic, can be carried out in ACA_{0} given these predicates as they effectively determine inv(a) for every element a of the algebras.

We next (§5) turn to the analysis of the recursion theoretic complexity for ψ(B, ≡) and of ψ(DB, ≅). We will then use those constructions to establish our proof theoretic reversals in §6.

5 Recursion theoretic complexity

Our plan is first to provide a uniformly recursive set of Boolean algebras B_{k,l,m} such that inv(B_{k,l,m}) = ⟨k, l, m⟩. Next, by induction we construct uniformly recursive Boolean algebras, A_{i,j}, which code 0^{(i)} in the following sense:

inv_{1}(A_{i,j}) = i ⇔ j ∈ 0^{(i)}

inv_{1}(A_{i,j}) = i + 1 ⇔ j ∉ 0^{(i)}. If we now apply the assumption of the existence of invariants for countable sequences in the sense of ψ to the sequence C_{q} recursively listing all the B_{k,l,m} and A_{i,j}, we code 0^{(ω)} in the sense that any sequence ⟨n_{q}⟩ witnessing ψ for ⟨C_{q}⟩ computes 0^{(ω)}: To see if i ∈ 0^{(j)}, find a q such that C_{q} = A_{i,j} and then ⟨k, l, m⟩ and p such that B_{k,l,m} = C_{p} and n_{p} = n_{q}. (Such numbers exist since the B_{k,l,m} include all possible invariants and so all possible elementary equivalence types with inv_{1} finite.) Now i ∈ 0^{(j)} if and only if k = i. On the other hand, our analysis in §4 shows that for every sequence ⟨A_{i}⟩ of Boolean algebras the desired witness ⟨n_{i}⟩ for ψ is given by ⟨inv(A_{i})⟩ and this sequence is recursive in ⟨A_{i}⟩^{(ω)}. Thus we characterize the recursion theoretic strength of (∗B, ≡) as that of the ω-jump.

We now need some definitions and construction methods for Boolean algebras. Our primary building blocks will be algebras generated from linear orderings. We refer the reader to Monk [1989, I.6.15] and Goncharov [1997, 1.6 and 3.2] for general information about these interval algebras. We begin with some simple linear orderings and operations on linear orderings that we will use to construct the orderings whose interval algebras will be our desired B_{k,l,m} and A_{i,j}.

Definition 5.1 We let m denote the order type of an m-element linear ordering; ω that of the first infinite ordinal and η the order type of the rationals.

Definition 5.2 We define operations +, ∑_{i∈M} , ·, ^{n} and ∗ on linear orderings L_{i} and M by describing the resulting order types. We leave the formalities of defining particular representations of the order types to the reader.

1. L_{1} + L_{2}, the sum of the two orderings, has the order type of L_{1} followed by L_{2}.

2. ∑_{i∈M} L_{i} has the order type produced by replacing the element i of M (assumed to have underlying set ℕ) by the ordering L_{i}.

3. L_{1} · L_{2} the product of the two orderings, has the order type gotten by replacing each element of L_{2} by a copy of L_{1} (and so it is the ordering on pairs ⟨x_{1}, y_{1}⟩ ∈ L_{1} × L_{2} given by ⟨x_{1}, y_{1}⟩ < ⟨x_{2}, y_{2}⟩ ⇔ y_{1} < y_{2} or (y_{1} = y_{2} and x_{1} < x_{2})).

4. L_{1}^{n}, the n^{th} power of L_{1}, is defined as usual given by repeated multiplication: L_{1}^{1} = L_{1}; L^{n+1} = L_{1}^{n} · L_{1}.

Definition 5.3 If L is a linear ordering with a first element, then Intalg(L) is the Boolean algebra of finite unions of half open intervals [a, b) of L where b can be ∞. (The understanding here is that [a, ∞) = {x|x ≥ a}.) We often abuse notation by using L in place of Intalg(L). For example, we write inv(L) for inv(Intalg(L)). We also carry over notions and notation. For example, an ordering L or interval [a, b) is atomic if every subinterval contains an atom, i.e. a subinterval [x, y) such that [x, y) = {x}. Similarly, L or [a, b) is atomless iff it is dense with a first element (i.e. of the form 1 + η).

Note that, when we deal with interval algebras, the orderings generating them all have a first elements. We think of ∞ as a symbol used to define half open intervals but not as an element of the ordering. It is not hard to see that every countable Boolean algebra is isomorphic to the interval algebra of a countable linear order (Monk [1989, I.6.15.10]). We will generally work directly with the linear orders. To that end, we want to point out a few facts about the correspondences between L and Intalg(L) that are relevant to the analysis described by the Tarski invariants. They can be found in Monk [1989, I.6.15] or Goncharov [1997, 1.6 and 3.2].

Definition 5.4 A subset S of L is convex if x, y ∈ S and x < z < y implies that z ∈ S. An equivalence relation ∽ on L is convex if every one of its equivalence classes is convex.

Proposition 5.5 There is a one-one correspondence between ideals I of Intalg(L) and convex equivalence relations ∽ on L such that Intalg(L)/I ≅ Intalg(L/ ∽). Here L/ ∽ is the linear ordering of equivalence classes [x], [y] of ∽ given by [x] < [y] ⇔ ∀w ∽ x∀z ∽ y(w < z). The convention here is that if a final segment of L is collapsed to a single equivalence class then it is removed from L/ ∽ and its role is taken by ∞. (That is, we identify the final segment with the “external” point ∞.) For a given ideal I and canonical projection π, the corresponding equivalence class ∽ is given by x ∽ y ⇔ π(x) = π(y).

Definition 5.6 In accordance with this Proposition, we define the equivalence relation ∽_{T} corresponding to the Tarski ideal I(Intalg(L)) by x ∽_{T} y ⇔ [x, y) is a finite sum of atomic and atomless suborderings. We denote L/ ∽_{T} by L′ and so Intalg(L′) ≅ Intalg(L)/I(Intalg(L)) = (Intalg(L))′. As with the corresponding algebras we let L^{[0]} = L and L^{[n+1]} = (L^{[n]})′.

Now for the canonical algebras B_{k,l,m} with invariant ⟨k, l, m⟩ we take those of Morozov [1982] which are not only uniformly recursive (indeed, uniformly decidable) but dense as well.

Proposition 5.7 (Morozov [1982]) Let P = (1 + η + 1 + ω · η) · ω. The following table lists linear orders whose interval algebras are uniformly decidable, dense and have the indicated invariants.

\begin{matrix}L_{n,0,1} & P^{n} · (1 + η) & ⟨n, m, 1⟩ \\ L_{n,m,0} & P^{n} · m & ⟨n, m, 0⟩ \\ L_{n,m,1} & P^{n} · (1 + η + m) & ⟨n, 0, 1⟩ \\ L_{n,∞,0} & P^{n} · (1 + ω · η) & ⟨n, ∞, 0⟩ \\ L_{n,∞,1} & P^{n} · (1 + η + 1 + ω · η) & ⟨n, ∞, 1⟩ \end{matrix}

Thus we may take B_{k,l,m} to be Intalg(L_{k,l,m}).

Next, we must describe the algebras A_{i,j} that code 0^{(i)}. Our plan is to uniformly construct recursive linear orderings L_{n,j}^{Π} and L_{n,j}^{Σ} such that • inv_{1}(L_{n,j}^{Σ}) = n + 1 ⇔ j ∈ 0^{(n)} (Σ_{n} case)

• inv_{1}(L_{n,j}^{Σ}) = n ⇔ j ∉ 0^{(n)} (Π_{n} case)

• inv_{1}(L_{n,j}^{Π}) = n ⇔ j ∈ 0^{(n)} (Σ_{n} case)

• inv_{1}(L_{n,j}^{Π}) = n + 1 ⇔ j ∉ 0^{(n)} (Π_{n} case)

We begin with n = 1 :

• L_{1,j}^{Σ} = P^{2} ⇔ j ∈ 0′ (Σ_{1} case)

• L_{1,j}^{Σ} = P ⇔ j ∉ 0′ (Π_{1} case)

• L_{1,j}^{Π} = P ⇔ j ∈ 0′ (Σ_{1} case)

• L_{1,j}^{Π} = P^{2} ⇔ j ∉ 0′ (Π_{1} case)

Note that the desired properties for n = 1 hold (in ACA_{0}) as inv_{1}(P) = 1 and inv_{1}(P^{2}) = 2. In fact, if B = Intalg(P) then B/I(B) = {0, 1} and so inv(B) = ⟨1, 1, 0⟩ while P^{2}/I(P^{2}) = P and so inv(P^{2}) = ⟨2, 1, 0⟩.

Now each Σ_{n+1}(Π_{n+1}) fact such as j ∈ 0^{(n+1)}(j ∉ 0^{(n+1)}) is uniformly of the form ∃x(f(n, j, x) ∉ 0^{(n)}) (∀x(f(n, j, x) ∈ 0^{(n)})) for some fixed recursive f. Moreover, we may choose f such that f(n, j, x) ∉ 0^{(n)}& y > x → f(n, j, y) ∉ 0^{(n)}. (This is just quantifier manipulation to replace ∃z … with ∃x∃z < x … etc.) We now define the rest of our orderings as follows:

• L_{n+1,,j}^{Σ} = P^{n+1} + P^{n+1} + ∑_{k∈P} L_{n,f(n,j,k)}^{Π}

• L_{n+1,j}^{Π} = P^{n+1} + P^{n+1} + ∑_{k∈P} L_{n,f(n,j,k)}^{Σ}.

We let L_{n} = {L_{n,j}^{Π}|j ∈ ω} ∪ {L_{n,j}^{Σ}|j ∈ ω}. To verify that the invariants of these orderings are as required we proceed by induction on n to prove various facts about the orderings including that the coding works. We begin with a general lemma.

Lemma 5.8 If, for every i ∈ ω, inv_{1}(L_{i}) ≥ 1 for every L_{i} and L = ∑_{i∈M} L_{i} then L′ = ∑_{i∈M} L′_{i}.

Proof. Consider the equivalence relation x ∽_{T} y on L. If x and y belong to the same copy of L_{k} in M then they are clearly T-equivalent in M if and only if they are in L_{k} as this depends only on the order type of [x, y). If x and y are not in L_{i} and L_{j} for successive i, j ∈ M then x ≁_{T} y as the interval between them contains some L_{k} which by assumption is not a finite sum of atomic and atomless orderings. If x and y are in adjacent L_{i}, L_{j} then they can be identified only if x is identified with all the points to its right in L_{i}, i.e. the final segment of L_{i} beginning with x is a finite sum of atomic and atomless orderings (and so disappears in L′_{i}) and y is identified with the first element of L_{j} in L′_{j}. □

Theorem 5.9 If L ∈ L_{n} then inv_{1}(L) is n or n + 1. Moreover,

1. L = L_{n,j}^{Σ} & j ∈ 0^{(n)} ⇒ inv_{1}(K) = n + 1 and K^{[n+1]} = 1 for every final segment K of L;

2. L = L_{n,j}^{Σ} & j ∉ 0^{(n)} ⇒ inv_{1}(L) = n & L^{[n]} = 1 if n = 1 and L^{[n]} = m for some m > 1 if n > 1;

3. L = L_{n,j}^{Π} & j ∉ 0^{(n)} ⇒ inv_{1}(K) = n + 1 and K^{[n+1]} = 1 for every final segment K of L;

4. L = L_{n,j}^{Π} & j ∈ 0^{(n)} ⇒ inv_{1}(L) = n & L^{[n]} = 1 if n = 1 and L^{[n]} = m for some m > 1 if n > 1.

Proof. We proceed by induction on n. We have already noted that for n = 1 the desired facts about invariants and Tarski derivatives of L are true. For the final segments just note that in cases 1 and 3 they all contain (and are contained in) final segments isomorphic to the whole ordering.

For the inductive step at n + 1 we consider the cases in order. For notational convenience, we choose L_{k} in each case so that L = P^{n+1} + P^{n+1} + ∑_{k∈P} L_{k}.

1. Here inv_{1}(L_{k}) is n for finitely many k and n + 1 for the rest by induction. Recursively applying Lemma 5.8 we see that L^{[n]} = P + P + ∑_{k∈P} L_{k}^{[n]}. For the cofinitely many k for which inv_{1}(L_{k}) = n + 1 the entry in the k^{th} spot in the sum corresponding to L^{[n+1]} is L_{k}^{[n+1]} which is a single point (by induction). For the finitely many k for which inv_{1}(L_{k}) = n, L_{k}^{[n]} is m_{k} for some m_{k} ∈ ℕ (by induction). Thus in L^{[n+1]} it is identified with the least element in L^{[n]} to the right of all the points in L_{k}^{[n]} or the greatest one to its left if there is one (if both exist they are also identified) and otherwise becomes 1, i.e. a single point. Thus L^{[n+1]} is 1 + 1 + P (finitely many points have been removed from P but the result is still isomorphic to P) and so L^{[n+2]} = 1 as required. Of course, the same argument works for the sum over the L_{k} for k in any final segment of P.

2. Here inv_{1}(L_{k}) = n for every k by induction. If n = 1, L′_{k} = 1 for every k and so L′ = P + P + P and L^{[2]} = 3 as required. If n > 1, L^{[n]} = P + P + V where V is atomic, and so L^{[n+1]} = 2 again as required.

3. Here inv_{1}(L_{k}) = n + 1 and L_{k}^{[n+1]} = 1 for every k by induction. Thus L^{[n+1]} = 1 + 1 + P, and so L^{[n+2]} = 1 as required. Of course, the same is true for the sum over the L_{k} for k in any final segment of P.

4. If n = 1 then L is P^{2} + P^{2} followed by a sum over P in which finitely many points have been replaced by P^{2} and the rest by P. It is clear that, in this case, L^{[2]} is m where m is three more than the number of points that have been replaced by P^{2}. (The final segment of L is essentially P^{2} and so contributes one point to L^{[2]}. The initial segment is P^{2} + P^{2} and contributes two points as does every other copy of P^{2} in L. The points of P replaced by a copy of P which are to the left of a location where a copy of P^{2} is inserted are again single points in L′, and so these intervals in L′ are isomorphic to proper segments [x, y) of P which are then identified with the least point of the next copy of P^{2} in L^{[2]}.)

Finally, if n > 1 then for finitely many k, inv_{1}(L_{k}) = n + 1 and L_{k}^{[n+1]} = 1 while for all the rest inv_{1}(L_{k}) = n and L_{k}^{[n]} = m_{k} for some m_{k} > 1. In this case, L^{[n]} is P + P + V where V is a sum over P in which finitely many of the points are replaced by copies of P and the rest are replaced by the m_{k} which are atomic. Thus L^{[n+1]} is again two more points than the number of copies of P in V. (Each copy of P contributes one point. The atomic portions caught between two copies of P are identified with the first point of the copy of P immediately to their right. The final atomic segment is identified with ∞ and so is removed.) □

We can now prove that the recursion theoretic complexity of the existence of elementary equivalence invariants for recursive sequences of Boolean algebras is that of 0^{(ω)}.

Theorem 5.10 There is a uniformly recursive sequence ⟨A_{i}⟩ of Boolean algebras such that 0^{(ω)} is recursive in any witness ⟨n_{i}⟩ to the instance of ψ(B, ≡) corresponding to ⟨A_{i}⟩.

Proof. Let the members of the sequence ⟨A_{i}⟩ be the B_{k,l,m} and the interval algebras of the orders L in ∪{L_{n}|n ∈ ω} as defined above in some recursive order of type ω. To decide if j ∈ 0^{(n)} (recursively in ⟨n_{i}⟩) find numbers k, l, m, p and q such that A_{p} = B_{k,l,m}, A_{q} = L_{n,j}^{Σ} and n_{p} = n_{q}. (Such numbers exist since the B_{k,l,m} include all possible invariants and so all possible elementary equivalence types with inv_{1} finite.) By Theorem 5.9, inv_{1}(A_{q}) is n + 1 or n depending on whether j ∈ 0^{(n)} or not. As we also know that inv_{1}(A_{q}) = k since A_{q} ≡ B_{k,l,m}, we know that j ∈ 0 if and only if k = n + 1. □

We now work towards a proof that the Boolean algebras appearing in the above proof are all dense.

Lemma 5.11 (Goncharov [1997] 2.24) If a, b ∈ A a Boolean algebra and a ∧ b = 0 then

1. inv_{1}(a ∨ b) = max{inv_{1}(a), inv_{1}(b)};

2. inv_{1}(a) = inv_{1}(b) ⇒ inv_{2}(a ∨ b) = inv_{2}(a) + inv_{2}(b);

3. inv_{1}(a) < inv_{1}(b) ⇒ inv(a ∨ b) = inv(b).

Corollary 5.12 If a ∈ Intalg(L) and (as must necessarily be true for some choice of x_{i}, y_{i} and n) a = ∪{[x_{i}, y_{i})|i < n} then there is an i < n such that inv_{1}(a) = inv_{1}([x_{i}, y_{i})) and if inv_{2}(a) = ∞ then there is an i < n such that inv_{1}(a) = inv_{1}([x_{i}, y_{i})) and inv_{2}([x_{i}, y_{i})) = ∞.

Lemma 5.13 If K, L and M are linear orderings with first elements and x, y ∈ L (with y possibly being the ∞ of L which we identify with the first element of M) then inv^{L}([x, y)) = inv^{K+L+M}([x, y)) where we use the superscript to indicate that the evaluation of the invariant is taking place in the specified Boolean algebra (i.e. the interval algebra of the specified ordering).

Proof. This is immediate from the fact that points x and y are identified under the Tarski equivalence relation if and only if [x, y) can be divided up into a finite sum of sub intervals each of which is atomic or atomless and this depends only on the order type of [x, y) and not on the ambient order containing it. □

Definition 5.14 We say that a linear ordering L is B-dense if Intalg(L) is a dense Boolean algebra.

Remark 5.15 By Corollary 5.12 if we want to prove that a linear ordering L is B-dense we need only verify the requirements of B-density for elements of the form [x, y). As all the orderings we consider have finite first invariant, proving the B-density of L amounts to verifying two conditions for every b = [x, y) and every m ∈ ℕ:

1. m < inv_{1}(b) ⇒ ∃a ≤ b(inv(a) = ⟨m, ∞, 0⟩) and

2. inv_{2}(b) = ∞ ⇒ ∃a ≤ b(inv_{1}(a) = inv_{1}(b) = inv_{1}(b−a) & inv_{2}(a) = ∞ = inv_{2}(b−a)

Lemma 5.16 If K and L are linear orderings with first elements then K + L is B-dense if and only if both K and L are B-dense.

Proof. Assume K and L are B-dense. We verify the requirements for the B-density of K + L for an arbitrary [x, y). If x and y are in the same component of K + L (including y = 0_{L} which plays the role of ∞ in K) then the requirements follow from the B-density of the component and Lemma 5.13. So suppose that x ∈ K and y ∈ L − {0_{L}} so that [x, y) = [x, 0_{L})∪[0_{L}, y). Now the result follows from our assumptions and Corollary 5.12.

For the other direction, assume that K + L is B-dense. Consider any b = [x, y) with x and y in the same component (we identify ∞_{K} and 1_{L}). If b satisfies the hypotheses of one of the conditions defining B-density in its own component, then it does so in K + L as well by 5.13. The witness a, assured by the B-density of K + L, is smaller than b and so contained in the same component. Again, its invariants in that component are the same as in K + L, and so it witnesses satisfaction of the requirement for the B-density of the component. □

Theorem 5.17 Every L ∈ L_{n} is B-dense for every n.

Proof. We begin with P itself and consider an arbitrary b = [x, y). The only ones such that inv_{1}(b) = 1 are those with y = ∞. For these inv(b) = ⟨1, 1, 0⟩; all the others have inv_{1}(b) = 0. So, if inv_{1}(b) = 1 we must verify Condition (1) with k = 0. Any element a corresponding to the suborder 1+ω·η of any component of P = ∑_{k∈ω}(1+η+1+ω·η) in the final segment b has inv(a) = ⟨0, ∞, 0⟩ as required. If inv_{1}(b) = 0, then we only have to verify Condition (2). If inv_{2}(b) = ∞, i.e. b contains infinitely many pairs of points that are immediate successors, then it must contain some suborder of type ω · η. It can then be split into two such suborderings as required.

We should next consider P^{2} and indeed all the P^{n} but their B-density follows from the general argument for Case 3 so we proceed by induction on n beginning with Case 3. We phrase the proof to cover the P^{n} as well. It also then covers Case 2 with n = 1.

Note that, in every case, by Lemma 5.16, we need only prove the B-density of orderings of the form L = ∑_{k∈P} L_{k} for L_{k} ∈ L_{n}. Note that by Lemma 5.13 and the inductively assumed B-density of the L_{k}, we only need to verify the conditions for B-density for b = [x, y) with y = ∞ and with x ∈ L_{i} and y ∈ L_{j} for i <_{P} j. Also note that if j is the immediate successor of i in P, then b = [x, 1_{L_{j}}) ∪ [1_{L_{j}}, y). Now Corollary 5.12, together with the assumptions that L_{i} and L_{j} are B-dense, shows that b satisfies the requirements for B-density. Thus we may assume that there is a k such that i <_{P} k <_{P} j.

3. We want to show that if L = ∑_{k∈P} L_{k} and, for every k, L_{k} is B-dense, inv_{1}(K) = n + 1 and K^{(n+1)} = 1 for every final segment K of L_{k}, then L is B-dense. We already know that inv_{1}(b) = n + 2 only if b = [x, ∞) and that in this case inv_{2}(b) = 1. Thus, for these b, we need only verify Condition (1). By induction and Lemma 5.13, we only have to verify the case that m = n + 1. Here we know that L^{[n+1]} = P. Thus any element a whose image in L^{[n+1]} corresponds to the suborder 1 + ω · η of any component of P in the image of b has inv(a) = ⟨n + 1, ∞, 0⟩ as required. We are now left with the case that x ∈ L_{i} and y ∈ L_{j} with i <_{P} j. In this case inv_{1}(b) = n + 1 = inv_{1}^{L_{i}}(x, ∞) so there is an a = [w, z) ∈ L_{i} as required by Condition (1) for the B-density of L_{i}. This element satisfies the same condition for b in L by Lemma 5.13. Finally we must verify Condition (2) for such b with inv_{2}(b) = ∞. Since L^{[n+1]} = P, the argument for P can be applied to the image of b in L^{[n+1]} and the inverse image of the element so produced provides the desired witness.

2. (n > 1) Here L^{[n]} is atomic and so inv_{1}(L) = n. Thus inv_{1}(b) ≤ n. As noted above we may assume that b contains all of L_{k} for some k. Thus inv_{1}(b) = n and there are w, z strictly between x and y such that [w, z) ≅ P^{n}, so there are smaller elements satisfying Condition (1). The only way to have inv_{2}(b) = ∞ is for the image of [x, y) in P (in the sum ∑_{i∈P} m_{k} = L^{[n]}) to contain a subinterval of type η or ω · η. In either case, it is easy to split this image into two parts both of which contain infinitely many points. Each of these points of P corresponds to a component of L^{[n]} with at least one atom, and so its inverse image in L satisfies Condition (2).

1. In this case, there is a final segment of L which has the same properties as all of L did in Case 3, and so we have covered the situation in which y = ∞. Now inv_{1}(b) = n+1 if and only if b contains a finite segment of one of the L_{k} with inv_{1}(L_{k}) = n + 1. Any witness for Condition (1) for this final segment in L_{k} works for b in L. As L^{[n+1]} = P (with perhaps finitely many points removed) the analysis for P shows that Condition (2) is also satisfied for b if inv_{1}(b) = n + 1. Finally, if inv_{1}(b) ≤ n then inv_{1}(b) = n, since b contains some L_{k} with inv_{1}(L_{k}) = n. Condition (1) is satisfied by the density of the L_{k} contained in b. As for Condition (2), note that the only way that b does not contain some L_{k} with inv_{1}(L_{k}) = n + 1 is if it is contained in a finite sum of successive L_{i} with inv_{1}(L_{i}) = n plus perhaps a proper initial segment of one L_{j} with inv_{1}(L_{j}) = n + 1.

As for each such i other than j, L_{i}^{[n]} is atomic, Condition (2) can come into play only because of [0_{L_{j}}, y). As L_{j}^{[n]} has P as an initial segment, inv_{2}([0_{L_{j}}, y) = ∞ implies that in L_{j}^{[n]} the image of y is beyond the initial segment of P of type 1 + η. Thus, it contains an initial segment of the first copy of ω · η in P which can then easily be split as required for Condition (2).

4. If n = 1, L is a sum over P of finitely many copies of P^{2} and the rest copies of P. Now B-density follows easily from our previous arguments.

If n > 1, a final segment of L is of the form considered in Case (2). Thus we need only consider an initial segment of L of the form ∑_{i∈Q} L_{k} where Q = (1 + η + 1 + ω · η)m for some m ∈ ω in which, for finitely many k, inv_{1}(L_{k}) = n + 1 and, for the rest, inv_{1}(L_{k}) = n. In fact, by Lemma 5.16, it suffices to take m = 1. Now inv_{1}(b) = n + 1 if and only if b contains a final segment of one of the copies of an L_{k} with inv_{1}(L_{k}) = n + 1. In this case, Condition (1) is immediate from the B-density of L_{k}. As L^{[n+1]} is finite, Condition (2) is vacuous for such b. The only remaining case is that b contains only L_{k} with inv_{1}(L_{k}) = n and at least one such L_{k} so that inv_{1}(b) = n. In particular, the image of b in L^{[n]} is ∑_{i∈Q} m_{k} for some subinterval Q of P. In this case Condition (1) follows from the B-density of L_{k} (by induction) and Condition (2) can apply only if Q contains a interval of the form η or ω · η and so is easily satisfied. □

Remark 5.18 All the orderings of Proposition 5.7 (Morozov [1982]) can now been seen to be dense. We have directly proved it for all the powers P^{n}. The others all follow from Lemma 5.16 as all of the orderings with first invariant n are either sums of P^{n} or components of P^{n+1} or sums of each of these. (For example, P^{n+1} = P^{n}(1 + η) + P^{n}(1 + ω · η), and so both P^{n}(1 + η) and P^{n}(1 + ω · η) are dense.)

We have now proven that the recursion theoretic complexity of the existence of isomorphism invariants for recursive sequences of dense Boolean algebras is also 0^{(ω)}.

Theorem 5.19 There is a uniformly recursive sequence ⟨A_{i}⟩ of dense Boolean algebras such that 0^{(ω)} is recursive in any witness ⟨n_{i}⟩ to the instance of ψ(DB, ≅) corresponding to ⟨A_{i}⟩.

Proof. Theorem 5.17 and Remark 5.18 show that all the Boolean algebras appearing in the proof of Theorem 5.10 are dense. Goncharov [1997, 2.3] (as described in Theorem 4.4) shows that for dense Boolean algebras elementary equivalence is the same as isomorphism. □

From a recursion theoretic point of view these results can be viewed as types of hardness results for index sets. In the terminology defined in Soare [1987, IV.3.1] we have shown, for example, that (Σ_{n}, Π_{n}) ≤_{m} (B_{n}, B_{n+1}) where B_{n} = {B ∈ B|inv_{1}(B) = n}. The first natural question is whether this is the best one can do. As mentioned above a simple quantifier count shows only that B_{n} is in Σ_{4n}. One could therefore hope or even expect that it is Σ_{4n} complete. At one point, we thought that such a result would be useful for the reverse mathematical arguments we now wish to pursue. That does not seem to be the case, and so this seems to be an instance where the recursion theoretic questions are finer than those of reverse mathematics. Similar questions arise about the index sets for all the values of inv. We hope to deal with these purely recursion theoretic issues along with determining the index set for the Boolean algebras with finite first invariant in a future paper (Csima, Montalban and Shore [2005]). For now we turn to the issue of the complexity of the existence of these invariants in the sense of reverse mathematics.

6 Reversals

Our primary goal is to show that the strength, in the sense of reverse mathematics, of the existence of elementary equivalence invariants for Boolean algebras is that of ACA_{0}^{+}. As we argued in §1, it is sufficient to prove that RCA_{0} ⊢ ψ(B, ≡) → ACA_{0}^{+}. As usual, establishing ACA_{0}^{+} amounts to proving the existence of 0^{(ω)} (by a relativizable proof). Our recursion theoretic results seem to have provided us with such a proof already. In particular, Theorem 5.10 provides us with a uniformly recursive sequence ⟨A_{i}⟩ of Boolean algebras such that any witness ⟨n_{i}⟩ for the instance of ψ(B, ≡) corresponding to ⟨A_{i}⟩ computes 0^{(ω)}. The issue is, of course, whether our proof of Theorem 5.10 takes place in, or can be revised to work in, RCA_{0}.

The first problem is that even some of the simple algebraic arguments naturally take place in ACA_{0}. This problem is easy to handle in the style of the results of the previous section. The only issue is that dealing with elementary equivalence in RCA_{0} requires some care since one cannot assume that a given structure has a full satisfaction function (that would itself give ACA_{0}^{+}) nor even one for the set of Σ_{1} sentences (as that in general would give ACA_{0}). Thus we must use structures for which we can prove the existence of a partial satisfaction covering the sentences we need.

Proposition 6.1 RCA_{0} ⊢ ψ(B, ≡) → ACA_{0}. Indeed, RCA_{0} ⊢ ψ(DB, ≅) → ACA_{0}.

Proof. We begin with two nonisomorphic recursive dense Boolean algebras C_{0} = Intalg(1 + η) and C_{1} = Intalg(1 + η + 1). For any natural choice of recursive presentations of C_{0} and C_{1} it is easy to recursively define inv on these algebras and prove in RCA_{0} that they are dense. We can easily produce a uniformly recursive sequence ⟨C_{i}⟩ of Boolean algebras such that ∀i(C_{i} ≅ C_{0} or C_{i} ≅ C_{1}) and (∀i > 1)(i ∈ 0′ ⇔ C_{i} ≅ C_{0}) where each of the isomorphisms is recursive. Let ⟨n_{i}⟩ be a witness for the instance of ψ(B, ≡) or ψ(DB, ≅) corresponding to ⟨C_{i}⟩. If ⟨n_{i}⟩ is a witness for ψ(DB, ≅) it clearly computes 0′. Suppose it witnesses ψ(B, ≡). As isomorphism implies elementary equivalence (Proposition 4.8), i ∈ 0′ ⇒ n_{i} = n_{0} and i ∉ 0′ ⇒ n_{i} = n_{1}. Thus we only need to prove that n_{0} ≠ n_{1}, i.e. C_{0} ≢ C_{1}. Consider the sentence σ = ∀x∃y(x = 0 ∨ 0 < y < x). It is true in C_{0} and false in C_{1}. Moreover, it is easy to define partial satisfaction functions for both structures on the atomic sentences (with constants for the elements of C_{0}, C_{1}) and the (propositional combinations of) substitution instances of subformulas of σ. (The only basic ones not covered by the atomic cases are of the form ∃y(b = 0 ∨ 0 < y < b). These are true of 0 (in both algebras) but false for every nonzero b ∈ C_{0} and of every nonzero b ∈ C_{1} except for the final segment of C_{1} consisting of a single atom.) □

In view of this proposition, we may work over ACA_{0} from now on. We begin by discussing the properties of Boolean algebras developed in §3-4. There is no problem with the definition of the basic notions dealing with atomicity or atomlessness and of the Tarski ideal and derivative. All make sense and can be proven to exist for every Boolean algebra B in ACA_{0}. Our first problem arises when we try to iterate the Tarski derivative to define B^{[n]} and the function inv on B. These are not provably total operations in ACA_{0}. Of course, it only takes induction to define them and an induction argument to prove that they exist. Thus, in ACA, we can prove that B^{[n]} exists for every n. Even in ACA, however, we cannot prove the existence of either the sequence ⟨B^{[n]}⟩ or the function inv on B unless B^{[n]} = 0 for some n. Note that we need much less than full induction to get these results. For example, let ACA_{0}^{∗} be ACA_{0} + ∀X∀n(X^{(n)} exists) (by this we mean that ∀X∀n∃⟨Y_{0}, …, Y_{n}⟩(Y_{0} = X & (∀i < n)(Y_{i+1} = Y′_{i}))). Clearly ACA ⊢ ACA_{0}^{∗} and ACA_{0}^{∗} suffices to prove that, for every Boolean algebra B and every natural number n, B^{[n]} exists and if for some n, B^{[n]} = 0 then there is a function inv on B from which we can define the predicates of Definition 4.2 so that they satisfy the axioms listed there. We can also say that inv(B) = ⟨∞, 0, 0⟩ with the intended interpretation by saying that ∀n¬(inv_{1}(B) = n) (i.e. that the sequence of derivatives of length n + 1 exists and that B does not become 0 in any of them).

Note that the algebras we needed in the last section all had finite first invariant. Of course, for specifically constructed Boolean algebras, we may be able to prove even in ACA_{0} that a function inv exists with the required properties.

One route to our main theorem might now be to prove an effective quantifier elimination result for Boolean algebra with these extra predicates (as Tarski apparently did). This would show that two Boolean algebras are elementary equivalent if and only if they have the same invariant. (One point being that the quantifier elimination result would show that they have total satisfaction functions.) Although something along these lines is possible, there is no direct classical style proof of quantifier elimination in the published literature. The closest is the proof of model completeness in Ershov [1964] which would also suffice to prove the existence of total satisfaction functions for each of our algebras in ACA_{0}. His decision procedure for the one quantifier sentences would then give the decidability of the theories and show that they are elementary equivalent if and only if they have the same invariant. That would still leave us with the (inductive) task of establishing that our algebras have the desired invariants. We have chosen, instead, to follow a path of analysis that exploits the density of our algebras, and so establishes isomorphism results rather than elementary equivalence ones. Nonetheless, we will have to deal with many of the same issue of the apparent calls on induction needed to define the invariant functions for our algebras.

Turning then to the development of the theory of dense Boolean algebras we immediately hit the issue of the definition of density of B which, prima facie, assumes the existence of the function inv on B. Again, as we will only need ones with inv_{1} < ∞, we could assume ACA_{0}^{∗} and keep the original definition. As we will in the end want to work only in ACA_{0}, it is better to follow a route like that taken for elementary equivalence.

Definition 6.2 (ACA_{0}) A boolean algebra B is dense if, for every function inv and associated predicates I_{n}, A_{n}, B_{n} and C_{n} on B as given in Definition 4.2 that satisfy the axioms listed there and the defining equations for inv of Definition 4.1, the conditions defining density (Definition 4.3) hold.

Note that, given a function h on B purporting to be a candidate for inv which gives inv_{1}(B) = n for some n, the properties that need to be verified to show that it is really the function inv are all arithmetical, indeed, of fixed quantifier level (in h and B). (First define the extra predicates directly from inv and then just look at the axioms in Definition 4.2.) Thus it makes sense to hope that we can verify that h is the desired inv function in ACA_{0} and that it witnesses the density of B even if an induction on inv_{1}, or equivalently, on the levels of the predicates, is needed.

Next, it is easy to check that our basic definitions and lemmas about dense Boolean algebras, interval algebras and the connections between them make sense and can be carried out in ACA_{0}. In particular, there are no problems with 5.1-5.5 and 5.8. (In Lemma 5.7 we understand the assertion that inv_{1}(L_{k}) ≥ 1 to mean just that L_{k} is not a finite sum of atomic and dense suborderings.) So too there are no problems in proving 5.11-5.16 in ACA_{0} whenever the invariant functions assumed in the statements exist. We also note again that Goncharov’s [1997, 2.3.2] proof that any two dense Boolean algebras with the same invariant are isomorphic works in ACA_{0} as long as the function inv exists for both algebras.

Finally, we are left to consider the proofs of Theorems 5.9 where the Boolean algebras coding 0^{(ω)} are constructed and analyzed and Theorem 5.17 where they are all proven to be dense. There is no problem with the definition of the orderings (and so algebras) L_{k,l,m} and those in the L_{n} hierarchy as they are given uniformly recursively. As presented in the last section, the proofs of both of these theorems are straightforward ones by induction. They can be routinely carried out in ACA. Thus we have proven our reversals over ACA; actually, by Proposition 6.1, over RCA .

Theorem 6.3 RCA ⊢ ψ(B, ≡) → ACA^{+} and RCA ⊢ ψ(DB, ≅) → ACA^{+}.

One could also prove these results now in ACA_{0}^{∗} by showing that all is well for each n. Here one can prove the existence of the functions inv for the orderings at each level L_{n} directly from the definitions of the predicates up to level n + 1 which exist for an arbitrary Boolean algebra B since their definition only requires the existence of B^{(4n+4)}. However, we want to work over ACA_{0} alone. The first step is to give the “right” proof in ACA_{0}^{∗} that only needs the existence of 0^{(n)} to prove the existence of the function inv on the orderings in L_{n}. We then plan on doing an induction argument that simultaneously proves the existence of 0^{(n)} and that the orderings in L_{n} have the properties established in §5. (A subtle point here is that we can not do an induction that establishes the existence of 0^{(n)} and then simply asserts that therefore there are inv functions for orderings in L_{n} as, in the abstract, this requires 0^{(4n+4)} whose existence we cannot prove in ACA_{0} from the existence of 0^{(n)}.)

We begin with a formal description of what it means to be the function inv_{1} on a Boolean algebra. Of course, the full invariant function inv is arithmetically definable from inv_{1} and so if the latter has been shown to exist in ACA_{0} then so does the former.

Definition 6.4 (ACA_{0}) If B is a Boolean algebra, we say that a function h : B → ℕ satisfies the conditions to be inv_{1} on B if ∀n(I_{n+1} = {x ∈ B| the image of x in B/I_{n} is a finite sum of atomic and atomless elements of B/I_{n}) where I_{k} = {x ∈ B|h(x) ≤ k}.

Proposition 6.5 (ACA_{0}) Fix a natural number m and assume that 0^{(m)} exists, i.e. there is a sequence of sets ⟨Y_{i}|i ≤ m⟩ such that Y_{0} = ∅ and (∀i < n)(Y_{i+1} = Y′_{i}). Then there is a family of functions h_{n,j}^{Γ} for n < m and j ∈ ℕ uniformly recursively in 0^{(m)} such that they satisfy the conditions to be inv_{1} on Intalg(L_{n,j}^{Γ}) for n < m, j ∈ ℕ and Γ = Σ or Π. Moreover, the properties established in Theorems 5.9 and 5.17 all hold.

Proof. We begin by defining the functions h_{n,j}^{Γ} by induction on n < m uniformly recursively in 0^{(m)}. In every case, we define the functions directly on subintervals [x, y) and extend to the whole algebra (i.e. to finite sums) by taking the max. When defining h on a sum over P of orderings L_{k} for which we already have defined functions h_{k}, we set h([x, y)) = h_{k}([x, y)) if x and y are in the same component L_{k} (with the usual understanding that we identify the first element of L_{j} with ∞_{L_{k}} if j is the immediate successor of k in P). Similarly, if x ∈ L_{i}, y ∈ L_{j} and j is the immediate successor of i in P then we let h([x, y)) = max{h_{L_{i}}([x, ∞)), h_{L_{j}}([1, y))}. Thus we only need to specify the value of h on intervals of the form [x, ∞) and [x, y) with x ∈ L_{i}, y ∈ L_{j} when there is some k such that i <_{P} k <_{P} j.

For n = 1, L_{n,j}^{Γ} is either P or P^{2} and 0′ can tell which one effectively. The corresponding functions h_{n,j}^{Γ} are then just set to be what we know are the corresponding functions inv_{1} on P or P^{2}. For P, h([x, y)) is 1 if y = ∞ and 0 otherwise. For P^{2} = ∑_{i∈P} P, we let h([x, y)) = 2 if y = ∞ and otherwise 1, for x and y in different components.

For 1 < n + 1 < m, we divide into cases as in Theorem 5.9. Note that it suffices to define h on ∑_{i∈P} L_{i} as we can then extend it to P^{n+1} + P^{n+1} + ∑_{i∈P} L_{i} by our algebraic rules as long as we have a definition for P^{n+1}. This definition is given by the procedures in Case 3 for ∑_{i∈P} L_{i} when each L_{i} = P^{n}. It also covers Case 2 for n = 1.

3. h([x, y)) = n + 2 if y = ∞ and otherwise n + 1 for x and y in different components.

1. As j ∈ 0^{(n+1)}, there are only finitely many k such that f(n, j, k) ∈ 0^{(n)} and recursively in 0^{(n+1)} we can find (the canonical index of) the set F consisting of these k.

Of course, we set h([x, ∞)) = n + 2 for every x. If x ∈ L_{i} and y ∈ L_{j} for i <_{P} j, we set h([x, y)) = n + 1 if there is a k ∉ F such that i ≤_{P} k < j; otherwise, h([x, y)) = n.

2. (n > 1) We set h([x, ∞)) = n + 1 for every x. For the other case that needs a definition, we set h([x, y)) = n.

4. As j ∈ 0^{(n+1)}, there are only finitely many k such that f(n, j, k) ∈ 0^{(n)} and, recursively in 0^{(n+1)}, we can find (the canonical index of) the set F consisting of these k. We set h([x, ∞)) = n+1 for every x. For the other case required, we set h([x, y)) = n+1 if there is a k ∈ F such that i ≤_{P} k <_{P} j; otherwise, h([x, y)) = n.

It is now routine to prove by induction on n < m that these functions satisfy the conditions to be inv_{1} on the corresponding algebras and (following the previous proofs) that they have the properties established in Theorems 5.9 and 5.17. □

We can now prove the reversal part of our main theorem.

Theorem 6.6 RCA_{0} ⊢ ψ(B, ≡) → ACA_{0}^{+}.

Proof. Let ⟨n_{1}⟩ be the witness to ψ(B, ≡) for ⟨A_{i}⟩. Define ⟨Y_{i}⟩ recursively in the jump of ⟨n_{i}⟩ by j ∈ Y_{i} ⇔ ∃k, l, m, p, q(A_{p} = B_{k,l,m} & A_{q} = L_{i,j}^{Σ} & n_{p} = n_{q}). We claim that Y_{i+1} = Y′_{i} for every i. If not, let m be least counterexample. Thus, 0^{(m)} exists and, since RCA_{0} ⊢ ψ(B, ≡) → ACA_{0} (Proposition 6.1), so does 0^{(m+2)}. Proposition 6.5 now guarantees that all the orderings up to level m + 1 have all the desired properties, and so the proofs of Theorems 5.10 and 5.19 work up to level m + 1 to show that Y_{m+1} = Y′_{m}, for the required contradiction. □

Finally, we want to get the same result for ψ(DB, ≅). The problem is that we cannot prove in advance of applying ψ(DB, ≅) that that all the orderings in the L_{n} are B-dense. We need one more twist to strengthen our inductive hand. We also show that for any L ∈ L_{n+1} with a function satisfying the conditions to be inv_{1} (or equivalently that the function inv with the required properties on L exists), then 0^{(n)} exists.

Definition 6.7 We define the members of L̂_{n} by induction. L̂_{1} = L_{1}. For L_{n+1,j}^{Γ} ∈ L_{n+1} we let L̂_{n+1,j}^{Γ} ∈ L̂_{n+1} be ∑_{m≤n} ∑_{i∈ω·η} L_{m.i}^{Σ} + ∑_{m≤n} ∑_{i∈ω·η} L_{m.i}^{Π} + L_{n+1,j}^{Γ}.

Proposition 6.8 (ACA_{0}) If a function h : L̂ → ℕ satisfies the conditions to be inv_{1} on L̂ ∈ L̂_{n}, then 0^{(n)} exists.

Proof. Let h be the assumed function on L̂. Each L_{i,j}^{Σ} is an interval [x_{i,j}, y_{i,j}) in L̂ that can be found recursively. Define Y_{i} for i ≤ n by j ∈ Y_{i} ⇔ h[x_{i,j}, y_{i,j}) = i + 1. Again, it is at this point straightforward to prove by induction that the L_{m,k}^{Γ} for m ≤ n all have the properties previously established, and so Y_{i+1} = Y′_{i} for i ≤ n. □

Theorem 6.9 RCA_{0} ⊢ ψ(DB, ≅) → ACA_{0}^{+}.

Proof. The L̂_{n,j} are all dense, and so we can argue as in Theorem 6.10 that applying ψ(DB, ≅) to the same sequence as there, except that we substitute L̂_{n,j} for L_{n,j}, we obtain the same results. □

We have thus completed the proofs of our main theorems of reverse mathematics.

Theorem 6.10 The existence of number invariants for elementary equivalence of countable Boolean algebras or for isomorphism of dense countable Boolean algebras has the same complexity in the sense of reverse mathematics as ACA_{0}^{+}.

7 Bibliography

Blass, A. R., Hirst, J. L. and Simpson, S. G. [1987], Logical analysis of some theorems of combinatorics and topological dynamics, in Logic and Combinatorics, S. G. Simpson ed., Contemporary Mathematics, American Mathematical Society, Providence, 125-156.

Csima, B., Montalban, A. and Shore, R.A. [2005], Boolean algebras, Tarski invariants and index sets, in preparation.

Chang, C. C. and Keisler, H. J. [1977], Model Theory 2^{nd} ed., North Holland, Amsterdam.

Ershov, Yu. L. [1964], Decidability of the elementary theory of distributive lattices with relative complements and the theory of filters, Algebra i Logika 3, 17-38.

Ershov, Yu. L., Goncharov, S. S., Nerode, A. and Remmel, J. B. eds. [1998], Handbook of Recursive Mathematics, Studies in Logic and the Foundations of Mathematics, vols. 138-139, Elsevier, Amsterdam, vols. 1-2.

Friedman, H., Simpson, S. G. and Smith, R. [1983], Countable algebra and set existence axioms, Annals of Pure and Applied Logic 25, 141-181.

Goncharov, S. S. [1997], Countable Boolean Algebras and Decidability, Consultants Bureau, New York.

Doner, J. and Hodges, W., Alfred Tarski and decidable theories, The Journal of Symbolic Logic 53, 20-35.

Jensen, R. B. [1972], The fine structure of the constructible hierarchy, Annals of Mathematical Logic 4, 229-308.

Monk, J. D. ed. [1989], Handbook of Boolean Algebras, North Holland, Amsterdam, vols. 1-3.

Morozov, A. S. [1982], Strong constructivizability of countable saturated Boolean algebras, Algebra i Logika 21, 193-203; English version in Algebra and Logic 21, 130-137.

Simpson, S. G. [1999], Subsystems of Second Order Arithmetic, Springer, Berlin. Soare, R. I. [1987], Recursively Enumerable Sets and Degrees, Perspectives in Math-

ematical Logic, Springer-Verlag, Berlin.

Tarski, A. [1949], Arithmetical classes and types of Boolean algebras, Bulletin of the American Mathematical Society 55, 63.

Vaught, R. L. [1954], Topics in the Theory of Arithmetical Classes and Boolean Algebras, Ph.D. Thesis, University of California, Berkeley.

White, W. M. [2000], Characterizations for Computable Structures, Ph.D. Thesis, Cornell University.