# An equivalent formulation of the GCH

The continuum hypothesis CH is the assertion that the size of the power set of a countably infinite set $\aleph_0$ is the next larger cardinal $\aleph_1$, or in other words, that $2^{\aleph_0}=\aleph_1$. The generalized continuum hypothesis GCH makes this same assertion about all infinite cardinals, namely, that the power set of any infinite cardinal $\kappa$ is the successor cardinal $\kappa^+$, or in other words, $2^\kappa=\kappa^+$.

Yesterday I received an email from Geoffrey Caveney, who proposed to me the following axiom, which I have given a name.

The Alternative GCH is the assertion that for every cardinal number $\kappa$, there is a set $F$ of cardinals such that $P_F(\kappa)=\{X\subseteq\kappa\mid |X|\in F\}$ has size $\kappa^+$.

The set $P_F(\kappa)$ restricts the power set operation to consist only of subsets whose size is allowed by the family $F$. We may assume without loss that $F$ consists of cardinals of size $\kappa$ or less.

Caveney was excited about his axiom for three reasons. First, a big part of his motivation for considering the axiom was the observation that the equation $2^\kappa=\kappa^+$ is simply not correct for finite cardinals $\kappa$ (other than $0$ and $1$) — and this is why the GCH makes the assertion only for infinite cardinals $\kappa$ — whereas the alternative GCH axiom makes a uniform statement for all cardinals, and gets the right answer for the finite cardinals. Specifically, for any natural number $n$, we can let $F=\{0,1\}$, and then note that $n$ has exactly $n+1$ many subsets of size in $F$. Second, Caveney had also observed that the GCH implies his axiom, since as we just mentioned, it is true for the finite cardinals and for infinite $\kappa$ we can take $F=\{\kappa\}$, using the fact that every infinite cardinal $\kappa$ has $2^\kappa$ many subsets of size $\kappa$ (we are working in ZFC). Third, Caveney had noticed that his axiom implies the continuum hypothesis, since in the case that $\kappa=\aleph_0$, there would be a family $F$ for which $P_F(\aleph_0)$ has size $\aleph_1$. But since there are only countably many finite subsets of $\aleph_0$, it follows that $F$ must include $\aleph_0$ itself, and so this would mean that $\aleph_0$ has only $\aleph_1$ many infinite subsets, and this implies CH.

To my way of thinking, the natural question to consider was whether Caveney’s axiom was actually weaker than GCH or not. At first I noticed that the axiom implies $2^{\aleph_1}=\aleph_2$ and similarly $2^{\aleph_n}=\aleph_{n+1}$, getting us up to $\aleph_\omega$. Then, after a bit I noticed that we can push the argument through all the way.

Theorem. The alternative GCH is equivalent to the GCH.

Proof. We’ve already argued for the converse implication, so it remains only to show that the alternative GCH implies the GCH. Assume that the alternative GCH holds.

We prove the GCH by transfinite induction. For the anchor case, we’ve shown already above that the GCH holds at $\aleph_0$, that is, that CH holds. For the successor case, assume that the GCH holds at some $\delta$, so that $2^\delta=\delta^+$, and consider the case $\kappa=\delta^+$. By the alternative GCH, there is a family $F$ of cardinals such that $P_F(\kappa)=\kappa^+$. If every cardinal in $F$ is less than $\kappa$, then $P_F(\kappa)$ has size at most $\kappa^{<\kappa}=(\delta^+)^\delta=2^\delta=\delta^+=\kappa$, which is too small. So $\kappa$ itself must be in $F$, and from this it follows that $\kappa$ has at most $\kappa^+$ many subsets of size $\kappa$, which implies $2^\kappa=\kappa^+$. So the GCH holds at $\kappa$, and we’ve handled the successor case. For the limit case, suppose that $\kappa$ is a limit cardinal and the GCH holds below $\kappa$. So $\kappa$ is a strong limit cardinal. By the alternative GCH, there is a family $F$ of cardinals for which $P_F(\kappa)=\kappa^+$. It cannot be that all cardinals in $F$ are less than the cofinality of $\kappa$, since in this case all the subsets of $\kappa$ in $P_F(\kappa)$ would be bounded in $\kappa$, and so it would have size at most $\kappa$, since $\kappa$ is a strong limit. So there must be a cardinal $\mu$ in $F$ with $\newcommand\cof{\text{cof}}\cof(\kappa)\leq\mu\leq\kappa$. But in this case, it follows that $\kappa^\mu=\kappa^+$, and this implies $\kappa^{\cof(\kappa)}=\kappa^+$, since by König’s theorem it is always at least $\kappa^+$, and it cannot be bigger if $\kappa^\mu=\kappa^+$. Finally, since $\kappa$ is a strong limit cardinal, it follows easily that $2^\kappa=\kappa^{\cof(\kappa)}$, since every subset of $\kappa$ is determined by it’s initial segments, and hence by a $\cof(\kappa)$-sequence of bounded subsets of $\kappa$, of which there are only $\kappa$ many. So we have established that $2^\kappa=\kappa^+$ in the limit case, completing the induction. So we get all instances of the GCH.
QED

# Same structure, different truths, Stanford University CSLI, May 2016

This will be a talk for the Workshop on Logic, Rationality, and Intelligent Interaction at the CSLI, Stanford University, May 27-28, 2016.

Abstract. To what extent does a structure determine its theory of truth? I shall discuss several surprising mathematical results illustrating senses in which it does not, for the satisfaction relation of first-order logic is less absolute than one might have expected. Two models of set theory, for example, can have exactly the same natural numbers and the same arithmetic structure $\langle\mathbb{N},+,\cdot,0,1,<\rangle$, yet disagree on what is true in this structure; they have the same arithmetic, but different theories of arithmetic truth; two models of set theory can have the same natural numbers and a computable linear order in common, yet disagree on whether it is a well-order; two models of set theory can have the same natural numbers and the same reals, yet disagree on projective truth; two models of set theory can have a rank initial segment of the universe $\langle V_\delta,{\in}\rangle$ in common, yet disagree about whether it is a model of ZFC. These theorems and others can be proved with elementary classical model-theoretic methods, which I shall explain. On the basis of these observations, Ruizhi Yang (Fudan University, Shanghai) and I argue that the definiteness of the theory of truth for a structure, even in the case of arithmetic, cannot be seen as arising solely from the definiteness of the structure itself in which that truth resides, but rather is a higher-order ontological commitment.

Main article: Satisfaction is not absolute

# On the strength of second-order set theories beyond ZFC, PSC-CUNY Research Award grant, 2016

J. D. Hamkins, On the strength of second-order set theories beyond ZFC, PSC-CUNY Research Award grant #69573-00 47, funded for 2016-2017.

Abstract. Professor Hamkins proposes to undertake research in the area of logic and foundations known as set theory, focused on the comparative strengths of several of the second-order set theories upon which several prominent recent research efforts have been based. These theories span the range from ZFC through GBC, plus various comprehension, transfinite recursion or class determinacy principles, up to KM and through the hierarchy to KM+ and beyond. Hamkins’s recent result with Gitman characterizing the precise strength of clopen determinacy for proper class games is a good start for the project, but many open questions remain, and Hamkins outlines various strategies that might solve them.

# The finite axiom of symmetry

At the conclusion of my talk today for the CUNY Math Graduate Student Colloquium, Freiling’s axiom of symmetry Or, throwing darts at the real line, I had assigned an exercise for the audience, and so I’d like to discuss the solution here.

The axiom of symmetry asserts that if you assign to each real number $x$ a countable set $A_x\subset\mathbb{R}$, then there should be two reals $x,y$ for which $x\notin A_y$ and $y\notin A_x$.

Informally, if you have attached to each element $x$ of a large set $\mathbb{R}$ a certain comparatively small subset $A_x$, then there should be two independent points $x,y$, meaning that neither is in the set attached to the other.

The challenge exercise I had made is to prove a finite version of this:

The finite axiom of symmetry. For each finite number $k$ there is a sufficiently large finite number $n$ such that for any set $X$ of size $n$ and any assignment $x\mapsto A_x$ of elements $x\in X$ to subsets $A_x\subset X$ of size $k$, there are elements $x,y\in X$ such that $x\notin A_y$ and $y\notin A_x$.

Proof. Suppose we are given a finite number $k$. Let $n$ be any number larger than $k^2+k$. Consider any set $X$ of size $n$ and any assignment $x\mapsto A_x$ of elements $x\in X$ to subsets $A_x\subset X$ of size at most $k$. Let $x_0,x_1,x_2,\dots,x_k$ be any $k+1$ many elements of $X$. The union $\bigcup_{i\leq k} A_{x_i}$ has size at most $(k+1)k=k^2+k$, and so by the choice of $n$ there is some element $y\in X$ not in any $A_{x_i}$. Since $A_y$ has size at most $k$, there must be some $x_i$ not in $A_y$. So $x_i\notin A_y$ and $y\notin A_{x_i}$, and we have fulfilled the desired conclusion. QED

Question. What is the optimal size of $n$ as a function of $k$?

It seems unlikely to me that my argument gives the optimal bound, since we can find at least one of the pair elements inside any $k+1$ size subset of $X$, which is a stronger property than requested. So it seems likely to me that the optimal bound will be smaller.

# Every function can be computable!

I’d like to share a simple proof I’ve discovered recently of a surprising fact:  there is a universal algorithm, capable of computing any given function!

Wait, what? What on earth do I mean? Can’t we prove that some functions are not computable?  Yes, of course.

What I mean is that there is a universal algorithm, a Turing machine program capable of computing any desired function, if only one should run the program in the right universe. There is a Turing machine program $p$ with the property that for any function $f:\newcommand\N{\mathbb{N}}\N\to\N$ on the natural numbers, including non-computable functions, there is a model of arithmetic or set theory inside of which the function computed by $p$ agrees exactly with $f$ on all standard finite input. You have to run the program in a different universe in order that it will compute your desired function $f$.
Theorem There is a Turing machine program $p$, carrying out the specific algorithm described in the proof, such that for any function $f:\N\to\N$, there is a model of arithmetic $M\models\PA$, or indeed a model of set theory $M\models\ZFC$ or more (if consistent), such that the function computed by program $p$ inside $M$ agrees exactly with $f$ on all standard finite input.

The proof is elementary, relying essentially only on the ideas of the classical proof of the Gödel-Rosser theorem. To briefly review, for any computably axiomatized theory $T$ extending $\PA$, there is a corresponding sentence $\rho$, called the Rosser sentence, which asserts, “for any proof of $\rho$ in $T$, there is a smaller proof of $\neg\rho$.” That is, by smaller, I mean that the Gödel-code of the proof is smaller. One constructs the sentence $\rho$ by a simple application of the Gödel fixed-point lemma, just as one constructs the usual Gödel sentence that asserts its own non-provability. The basic classical facts concerning the Rosser sentence include the following:

• If $T$ is consistent, then so are both $T+\rho$ and $T+\neg\rho$
• $\PA+\Con(T)$ proves $\rho$.
• The theories $T$, $T+\rho$ and $T+\neg\rho$ are equiconsistent.
• If $T$ is consistent, then $T+\rho$ does not prove $\Con(T)$.

The first statement is the essential assertion of the Gödel-Rosser theorem, and it is easy to prove: if $T$ is consistent and $T\proves\rho$, then the proof would be finite in the meta-theory, and so since $T$ would have to prove that there is a smaller proof of $\neg\rho$, that proof would also be finite in the meta-theory and hence an actual proof, contradicting the consistency of $T$. Similarly, if $T\proves\neg\rho$, then the proof would be finite in the meta-theory, and so $T$ would be able to verify that $\rho$ is true, and so $T\proves\rho$, again contradicting consistency. By internalizing the previous arguments to PA, we see that $\PA+\Con(T)$ will prove that neither $\rho$ nor $\neg\rho$ are provable in $T$, making $\rho$ vacuously true in this case and also establishing $\Con(T+\rho)$ and $\Con(T+\neg\rho)$, for the second and third statements. In particular, $T+\Con(T)\proves\Con(T+\rho)$, which implies that $T+\rho$ does not prove $\Con(T)$ by the incompleteness theorem applied to the theory $T+\rho$, for the fourth statement.

Let’s now proceed to the proof of the theorem. To begin, we construct what I call the Rosser tree over a c.e. theory $T$. Namely, we recursively define theories $R_s$ for each finite binary string $s\in 2^{{<}\omega}$, placing the initial theory $R_{\emptyset}=T$ at the root, and then recursively adding either the Rosser sentence $\rho_s$ for the theory $R_s$ or its negation $\neg\rho_s$ at each stage to form the theories at the next level of the tree.
$$R_{s\concat 1}=R_s+\rho_s$$
$$R_{s\concat 0}=R_s+\neg\rho_s$$
Each theory $R_s$ is therefore a finite extension of $T$ by successively adding the appropriate Rosser sentences or their negations in the pattern described by $s$. If the initial theory $T$ is consistent, then it follows by induction using the Gödel-Rosser theorem that all the theories $R_s$ in the Rosser tree are consistent. Extending our notation to the branches through the tree, if $f\in{}^\omega 2$ is an infinite binary sequence, we let $R_f=\bigcup_n R_{f\upharpoonright n}$ be the union of the theories arising along that branch of the Rosser tree. In this way, we have constructed a perfect set of continuum many distinct consistent theories.

I shall now describe a universal algorithm for the case of computing binary functions. Consider the Rosser tree over the theory $T=\PA+\neg\Con(\PA)$. This is a consistent theory that happens to prove its own inconsistency. By considering the Gödel-codes in order, the algorithm should begin by searching for a proof of the Rosser sentence $\rho_{\emptyset}$ or its negation in the initial theory $R_{\emptyset}$. If such a proof is ever found, then the algorithm outputs $0$ or $1$ on input $0$, respectively, depending on whether it was the Rosser sentence or its negation that was found first, and moves to the next theory in the Rosser tree by adding the opposite statement to the current theory. Then, it starts searching for a proof of the Rosser sentence of that theory or its negation. At each stage in the algorithm, there is a current theory $R_s$, depending on which prior proofs have been found, and the algorithm searches for a proof of $\rho_s$ or $\neg\rho_s$. If found, it outputs $0$ or $1$ accordingly (on input $n=|s|$), and moves to the next theory in the Rosser tree by adding the opposite statement to the current theory.

If $f:\N\to 2=\{0,1\}$ is any binary function on the natural numbers, then let $R_f$ be the theory arising from the corresponding path through the Rosser tree, and let $M\models R_f$ be a model of this theory. I claim that the universal algorithm I just described will compute exactly $f(n)$ on input $n$ inside this model. The thing to notice is that because $\neg\Con(\PA)$ was part of the initial theory, the model $M$ will think that all the theories in the Rosser tree are inconsistent. So the model will have plenty of proofs of every statement and its negation for any theory in the Rosser tree, and so in particular, the function computed by $p$ in $M$ will be a total function. The question is which proofs will come first at each stage, affecting the values of the function. Let $s=f\restrict n$ and notice that $R_s$ is true in $M$. Suppose inductively that the function computed by $p$ has worked correctly below $n$ in $M$, and consider stage $n$ of the procedure. By induction, the current theory will be exactly $R_s$, and the algorithm will be searching for a proof of $\rho_s$ or its negation in $R_s$. Notice that $f(n)=1$ just in case $\rho_s$ is true in $M$, and because of what $\rho_s$ asserts and the fact that $M$ thinks it is provable in $R_s$, it must be that there is a smaller proof of $\neg\rho_s$. So in this case, the algorithm will find the proof of $\neg\rho_s$ first, and therefore, according to the precise instructions of the algorithm, it will output $1$ on input $n$ and add $\rho_s$ (the opposite statement) to the current theory, moving to the theory $R_{s\concat 1}$ in the Rosser tree. Similarly, if $f(n)=0$, then $\neg\rho_s$ will be true in $M$, and the algorithm will therefore first find a proof of $\rho_s$, give output $0$ and add $\neg\rho_s$ to the current theory, moving to $R_{s\concat 0}$. In this way, the algorithm finds the proofs in exactly the right way so as to have $R_{f\restrict n}$ as the current theory at stage $n$ and thereby compute exactly the function $f$, as desired.

Basically, the theory $R_f$ asserts exactly that the proofs will be found in the right order in such a way that program $p$ will exactly compute $f$ on all standard finite input. So every binary function $f$ is computed by the algorithm in any model of the theory $R_f$.

Let me now explain how to extend the result to handle all functions $g:\N\to\N$, rather than only the binary functions as above. The idea is simply to modify the binary universal algorithm in a simple way. Any function $g:\N\to \N$ can be coded with a binary function $f:\N\to 2$ in a canonical way, for example, by having successive blocks of $1$s in $f$, separated by $0$s, with the $n^{\rm th}$ block of size $g(n)$. Let $q$ be the algorithm that runs the binary universal algorithm described above, thereby computing a binary sequence, and then extract from that binary sequence a corresponding function from $\N$ to $\N$ (this may fail, if for example, the binary sequence is finite or if it has only finitely many $0$s). Nevertheless, for any function $g:\N\to \N$ there is a binary function $f:\N\to 2$ coding it in the way we have described, and in any model $M\models R_f$, the binary universal algorithm will compute $f$, causing this adapted algorithm to compute exactly $g$ on all standard finite input, as desired.

Finally, let me describe how to extend the result to work with models of set theory, rather than models of arithmetic. Suppose that $\ZFC^+$ is a consistent c.e. extension of ZFC; perhaps it is ZFC itself, or ZFC plus some large cardinal axioms. Let $T=\ZFC^++\neg\Con(\ZFC^+)$ be a slightly stronger theory, which is also consistent, by the incompleteness theorem. Since $T$ interprets arithmetic, the theory of Rosser sentences applies, and so we may build the corresponding Rosser tree over $T$, and also we may undertake the binary universal algorithm using $T$ as the initial theory. If $f:\N\to 2$ is any binary function, then let $R_f$ be the theory arising on the corresponding branch through the Rosser tree, and suppose $M\models R_f$. This is a model of $\ZFC^+$, which also thinks that $\ZFC^+$ is inconsistent. So again, the universal algorithm will find plenty of proofs in this model, and as before, it will find the proofs in just the right order that the binary universal algorithm will compute exactly the function $f$. From this binary universal algorithm, one may again design an algorithm universal for all functions $g:\N\to\N$, as desired.

One can also get another kind of universality. Namely, there is a program $r$, such that for any finite $s\subset\N$, there is a model $M$ of $\PA$ (or $\ZFC$, etc.) such that inside the model $M$, the program $r$ will enumerate the set $s$ and nothing more. One can obtain such a program $r$ from the program $p$ of the theorem: just let $r$ run the universal binary program $p$ until a double $0$ is produced, and then interprets the finite binary string up to that point as the set $s$ to output.

Let me now also discuss another form of universality.

Corollary
There is a program $p$, such that for any model $M\models\PA+\Con(\PA)$ and any function $f:M\to M$ that is definable in $M$, there is an end-extension of $M$ to a taller model $N\models\PA$ such that in $N$, the function computed by program $p$ agrees exactly with $f$ on input in $M$.

Proof
We simply apply the main theorem inside $M$. The point is that if $M$ thinks $\Con(\PA)$, then it can build what it thinks is the tree of Rosser extensions, and it will think that each step maintains consistency. So the theory $T_f$ that it constructs will be consistent in $M$ and therefore have a model (the Henkin model) definable in $M$, which will therefore be an end-extension of $M$.
QED

This last application has a clear affinity with a theorem of Woodin’s, recently extended by Rasmus Blanck and Ali Enayat. See Victoria Gitman’s posts about her seminar talk on those theorems: Computable processes can produce arbitrary outputs in nonstandard models, continuation.

# Burak Kaya, Ph.D. March 2016

Burak Kaya successfully defended his dissertation, “Cantor minimal systems from a descriptive perspective,” on March 24, 2016, earning his Ph.D. degree at Rutgers University under the supervision of Simon Thomas. The dissertation committee consisted of Simon Thomas, Gregory Cherlin, Grigor Sargsyan and myself, as the outside member.

The defense was very nice, with an extremely clear account of the main results, and the question session included a philosophical discussion on various matters connected with the dissertation, including the principle attributed to Gao that any collection of mathematical structures that has a natural Borel representation has a unique such representation up to Borel isomorphism, a principle that was presented as a Borel-equivalence-relation-theory analogue of the Church-Turing thesis.

Abstract.  In recent years, the study of the Borel complexity of naturally occurring classification problems has been a major focus in descriptive set theory. This thesis is a contribution to the project of analyzing the Borel complexity of the topological conjugacy relation on various Cantor minimal systems.

We prove that the topological conjugacy relation on pointed Cantor minimal systems is Borel bireducible with the Borel equivalence relation $\newcommand\d{\Delta^+_{\mathbb{R}}}\d$. As a byproduct of our analysis, we also show that $\d$ is a lower bound for the topological conjugacy relation on Cantor minimal systems.

The other main result of this thesis concerns the topological conjugacy relation on Toeplitz subshifts. We prove that the topological conjugacy relation on Toeplitz subshifts with separated holes is a hyperfinite Borel equivalence relation. This result provides a partial affirmative answer to a question asked by Sabok and Tsankov.

As pointed Cantor minimal systems are represented by properly ordered Bratteli diagrams, we also establish that the Borel complexity of equivalence of properly ordered Bratteli diagrams is $\d$.

# Famous quotations in their original first-order language

Historians everywhere are shocked by the recent discovery that many of our greatest thinkers and poets had first expressed their thoughts and ideas in the language of first-order predicate logic, and sometimes modal logic, rather than in natural language. Some early indications of this were revealed in the pioneering historical research of Henle, Garfield and Tymoczko, in their work Sweet Reason:

We now know that the phenomenon is widespread!  As shown below, virtually all of our cultural leaders have first expressed themselves in the language of first-order predicate logic, before having been compromised by translations into the vernacular.

$\neg\lozenge\neg\exists s\ G(i,s)$

$(\exists x\ x=i)\vee\neg(\exists x\ x=i)$

$\left(\strut\neg\exists t\ \exists d\ \strut D(d)\wedge F(d)\wedge S_t(i,d)\right)\wedge\left(\strut\neg\exists t\ w\in_t \text{Ro}\right)\wedge\left(\strut \text{Ru}(i,y)\to \lozenge\text{C}(y,i,qb)\wedge \text{Ru}(i)\wedge\text{Ru}(i)\wedge\text{Ru}(i)\wedge\text{Ru}(i)\right)$

$\neg B_i \exists g\ G(g)$

$\forall b\ \left(\strut G(b)\wedge B(b)\to \exists x\ (D(b,x)\wedge F(x))\right)$

$(\exists!w\ W_1(w)\wedge W_2(w)), \ \ \exists w\ W_1(w)\wedge W_2(w)\wedge S(y,w)$?

$\exists s\ Y(s)\wedge S(s)\wedge \forall x\ L(x,s)$

$\exists p\ \left[\forall c\ (c\neq p\to G(c))\right]\wedge\neg G(p)$

$\exists l\ \left[L(l)\wedge \boxdot_l\left({}^\ulcorner\,\forall g\ \text{Gl}(g)\to \text{Gd}(g){}^\urcorner\right)\wedge\exists s\ \left(SH(s)\wedge B(l,s)\right)\right]$

$(\forall p\in P\ \exists c\in\text{Ch}\ c\in p)\wedge(\forall g\in G\ \exists c\in\text{Cr}\ c\in g)$

$\forall x (F(w,x)\to x=F)$

$B\wedge \forall x\ \left[S(x)\wedge T(x)\to \exists!w\ W(w)\wedge\text{Gy}(x,w)\wedge\text{Gi}(x,w)\right]$

$\exists!x\ D(x)\wedge D(\ {}^\ulcorner G(i){}^\urcorner\ )$

$\forall f\ \forall g\ \left(\strut H(f)\wedge H(g)\to f\sim g\right)\wedge\forall f\ \forall g\ \left(\strut\neg H(f)\wedge \neg H(g)\to \neg\ f\sim g\right)$

$\exists w\ \left(\strut O(w)\wedge W(w)\wedge\exists s\ (S(s)\wedge L(w,s))\right)$

$C(i)\to \exists x\ x=i$

$\neg\neg\left(\strut H(y)\wedge D(y)\right)$

$\neg (d\in K)\wedge\neg (t\in K)$

$W(i,y)\wedge N(i,y)\wedge\neg\neg\lozenge L(i,y)\wedge \left(\strut \neg\ \frac23<0\to\neg S(y)\right)$

$\lozenge \text{CL}(i)\wedge\lozenge C(i)\wedge \lozenge (\exists x\ x=i)\wedge B(i)$

$\forall x\ K_x({}^\ulcorner \forall m\ \left[M(m)\wedge S(m)\wedge F(m)\to\boxdot\ \exists w\ M(m,w)\right]{}^\urcorner)$

$\forall e\forall h\ \left(\strut G(e)\wedge E(e)\wedge H(h)\to \neg L(i,e,h)\right)$

$\forall p\ \boxdot\text{St}(p)$

$\lozenge^w_i\ \forall g\in G\ \lozenge (g\in C)$

$\forall m\ (a\leq_C m)$

$\forall t\ (p\geq t)\wedge \forall t\ (p\leq t)$

$\forall x\ (F(x)\iff x=h)$

$(\forall x\ \forall y\ x=y)\wedge(\exists x\ \exists y (x=x>y=y))$

$\forall p\ \left(\strut\neg W(p)\to \neg S(p)\right)$

$\forall p \left(\strut E(p)\to \forall h\in H\ A(p,h)\right)$

Dear readers, in order to assist with this important historical work, please provide translations into ordinary English in the comment section below of any or all of the assertions listed above. We are interested to make sure that all our assertions and translations are accurate.

In addition, any readers who have any knowledge of additional instances of famous quotations that were actually first made in the language of first-order predicate logic (or similar) are encouraged to post comments below detailing their knowledge. I will endeavor to add such additional examples to the list.

Thanks to Philip Welch, to my brother Jonathan, and to Ali Sadegh Daghighi (in the comments) for providing some of the examples, and to Timothy Gowers for some improvements.

# Giorgio Audrito, PhD 2016, University of Torino

Dr. Giorgio Audrito has successfully defended his dissertation, “Generic large cardinals and absoluteness,” at the University of Torino under the supervision of Matteo Viale.

The dissertation Examing Board consisted of myself (serving as Presidente), Alessandro Andretta and Sean Cox.  The defense took place March 2, 2016.

The dissertation was impressive, introducing (in joint work with Matteo Viale) the iterated resurrection axioms $\text{RA}_\alpha(\Gamma)$ for a forcing class $\Gamma$, which extend the idea of the resurrection axioms from my work with Thomas Johnstone, The resurrection axioms and uplifting cardinals, by making successive extensions of the same type, forming the resurrection game, and insisting that that the resurrection player have a winning strategy with game value $\alpha$. A similar iterative game idea underlies the $(\alpha)$-uplifting cardinals, from which the consistency of the iterated resurrection axioms can be proved. A final chapter of the dissertation (joint with Silvia Steila), develops the notion of $C$-systems of filters, generalizing the more familiar concepts of extenders and towers.

# Open determinacy for games on the ordinals, Torino, March 2016

This will be a seminar talk I shall give on March 3, 2016 at the University of Torino, Italy, in the same department where Giuseppe Peano had his position.  I shall be in Italy for the dissertation defense of Giorgio Audrito, on whose dissertation committee I am serving as president.

Abstract. The principle of open determinacy for class games — two-player games of perfect information with plays of length $\omega$, where the moves are chosen from a possibly proper class, such as games on the ordinals — is not provable in Zermelo-Fraenkel set theory ZFC or Gödel-Bernays set theory GBC, if these theories are consistent, because provably in ZFC there is a definable open proper class game with no definable winning strategy. In fact, the principle of open determinacy and even merely clopen determinacy for class games implies Con(ZFC) and iterated instances Con(Con(ZFC)) and more, because it implies that there is a satisfaction class for first-order truth, and indeed a transfinite tower of truth predicates $\text{Tr}_\alpha$ for iterated truth-about-truth, relative to any class parameter. This is perhaps explained, in light of the Tarskian recursive definition of truth, by the more general fact that the principle of clopen determinacy is exactly equivalent over GBC to the principle of elementary transfinite recursion ETR over well-founded class relations. Meanwhile, the principle of open determinacy for class games is provable in the stronger theory GBC+$\Pi^1_1$-comprehension, a proper fragment of Kelley-Morse set theory KM.

This is joint work with Victoria Gitman. See our article, Open determinacy for class games, which is currently under review.

# Math for nine-year-olds: fold, punch and cut for symmetry!

Today I had the pleasure to visit my daughter’s fourth-grade classroom for some fun mathematical activities. The topic was Symmetry!   I planned some paper-folding activities, involving hole-punching and cutting, aiming to display the dynamism that is present in the concept of symmetry. Symmetry occurs when a figure can leap up, transforming itself through space, and land again exactly upon itself in different ways.  I sought to have the students experience this dynamic action not only in their minds, as they imagined various symmetries for the figures we considered, but also physically, as they folded a paper along a line of symmetry, checking that this fold brought the figure exactly to itself.

The exercises were good plain fun, and some of the kids wanted to do them again and again, the very same ones.  Here is the pdf file for the entire project.

To get started, we began with a very simple case, a square with two dots on it, which the girls folded and then punched through with a hole punch, so that one punch would punch through both holes at once.

Next, we handled a few patterns that required two folds. I told the kids to look for the lines of symmetry and fold on them.  Fold the paper in such a way that with ONE punch, you can make exactly the whole pattern.

Don’t worry if the holes you punch do not line up exactly perfectly with the dots — if the holes are all touching their intended target and there are the right number of holes, then I told the kids it is great!

The three-fold patterns are a bit more challenging, but almost all of the kids were able to do it.  They did need some help punching through, however, since it sometimes requires some strength to punch through many layers.

With these further patterns, some of the folds don’t completely cover the paper. So double-check and make sure that you won’t end up with unwanted extra holes!

The second half of the project involved several cutting challenges.  To begin, let’s suppose that you wanted to cut a square out of the middle of a piece of paper. How would you do it?  Perhaps you might want to poke your scissors through and then cut around the square in four cuts.  But can you do it in just ONE cut?  Yes!  If you fold the paper on the diagonals of the square, then you can make one quick snip to cut out exactly the square, leaving the frame completely intact.

Similarly, one can cut out many other shapes in just one cut.  The rectangle and triangle are a little trickier than you might think at first, since at a middle stage of folding, you’ll find that you end up folding a shorter line onto a longer one, but the point is that this is completely fine, since one cut will go through both.  Give it a try!

Here are a few harder shapes, requiring more folds.

It is an amazing mathematical fact, the fold-and-cut theorem, that ANY shape consisting of finitely many straight line segments can be made with just one cut after folding.  Here are a few challenges, which many of the fourth-graders were able to do during my visit.

What a lot of fun the visit was!  I shall look forward to returning to the school next time.

In case anyone is interested, I have made available a pdf file of this project.  I would like to thank Mike Lawler, whose tweet put me onto the topic.  And see also the awesome Numberphile video on the fold-and-cut theorem, featuring mathematician Katie Steckles.

See more of my Math for Kids!

# Set-theoretic mereology

• J. D. Hamkins and M. Kikuchi, “Set-theoretic mereology.” (manuscript under review)
@ARTICLE{HamkinsKikuchi:Set-theoreticMereology,
author = {Joel David Hamkins and Makoto Kikuchi},
title = {Set-theoretic mereology},
journal = {},
year = {},
volume = {},
number = {},
pages = {},
month = {},
note = {manuscript under review},
eprint = {1601.06593},
url = {http://jdh.hamkins.org/set-theoretic-mereology},
abstract = {},
keywords = {},
source = {},
}

Abstract. We consider a set-theoretic version of mereology based on the inclusion relation $\newcommand\of{\subseteq}\of$ and analyze how well it might serve as a foundation of mathematics. After establishing the non-definability of $\in$ from $\of$, we identify the natural axioms for $\of$-based mereology, which constitute a finitely axiomatizable, complete, decidable theory. Ultimately, for these reasons, we conclude that this form of set-theoretic mereology cannot by itself serve as a foundation of mathematics. Meanwhile, augmented forms of set-theoretic mereology, such as that obtained by adding the singleton operator, are foundationally robust.

In light of the comparative success of membership-based set theory in the foundations of mathematics, since the time of Cantor, Zermelo and Hilbert, a mathematical philosopher naturally wonders whether one might find a similar success for mereology, based upon a mathematical or set-theoretic parthood relation rather than the element-of relation $\in$. Can set-theoretic mereology serve as a foundation of mathematics? And what should be the central axioms of set-theoretic mereology?

We should like therefore to consider a mereological perspective in set theory, analyzing how well it might serve as a foundation while identifying the central axioms. Although set theory and mereology, of course, are often seen as being in conflict, what we take as the project here is to develop and investigate, within set theory, a set-theoretic interpretation of mereological ideas. Mereology, by placing its focus on the parthood relation, seems naturally interpreted in set theory by means of the inclusion relation $\of$, so that one set $x$ is a part of another $y$, just in case $x$ is a subset of $y$, written $x\of y$. This interpretation agrees with David Lewis’s Parts of Classes (1991) interpretation of set-theoretic mereology in the context of sets and classes, but we restrict our attention to the universe of sets. So in this article we shall consider the formulation of set-theoretic mereology as the study of the structure $\langle V,\of\rangle$, which we shall take as the canonical fundamental structure of set-theoretic mereology, where $V$ is the universe of all sets; this is in contrast to the structure $\langle V,{\in}\rangle$, usually taken as central in set theory. The questions are: How well does this mereological structure serve as a foundation of mathematics? Can we faithfully interpret the rest of mathematics as taking place in $\langle V,\of\rangle$ to the same extent that set theorists have argued (with whatever degree of success) that one may find faithful representations in $\langle V,{\in}\rangle$? Can we get by with merely the subset relation $\of$ in place of the membership relation $\in$?

Ultimately, we shall identify grounds supporting generally negative answers to these questions. On the basis of various mathematical results, our main philosophical thesis will be that the particular understanding of set-theoretic mereology via the inclusion relation $\of$ cannot adequately serve by itself as a foundation of mathematics. Specifically, the following theorem and corollary show that $\in$ is not definable from $\of$, and we take this to show that one may not interpret membership-based set theory itself within set-theoretic mereology in any straightforward, direct manner.

Theorem. In any universe of set theory $\langle V,{\in}\rangle$, there is a definable relation $\in^*$, different from $\in$, such that $\langle V,{\in^*}\rangle$ is a model of set theory, in fact isomorphic to the original universe $\langle V,{\in}\rangle$, for which the corresponding inclusion relation $$u\subseteq^* v\quad\longleftrightarrow\quad \forall a\, (a\in^* u\to a\in^* v)$$ is identical to the usual inclusion relation $u\subseteq v$.

Corollary. One cannot define $\in$ from $\subseteq$ in any model of set theory, even allowing parameters in the definition.

A counterpoint to this is provided by the following theorem, however, which identifies a weak sense in which $\of$ may identify $\in$ up to definable automorphism of the universe.

Theorem. Assume ZFC in the universe $\langle V,\in\rangle$. Suppose that $\in^*$ is a definable class relation in $\langle V,{\in}\rangle$ for which $\langle V,\in^*\rangle$ is a model of set theory (a weak set theory suffices), such that the corresponding inclusion relation $$u\subseteq^* v\quad\iff\quad\forall a\,(a\in^* u\to a\in^* v)$$is the same as the usual inclusion relation $u\subseteq v$. Then the two membership relations are isomorphic $$\langle V,\in\rangle\cong\langle V,\in^*\rangle.$$

That counterpoint is not decisive, however, in light of the question whether we really need $\in^*$ to be a class with respect to $\in$, a question resolved by the following theorem, which shows that set-theoretic mereology does not actually determine the $\in$-isomorphism class or even the $\in$-theory of the $\in$-model in which it arises.

Theorem. For any two consistent theories extending ZFC, there are models $\langle W,{\in}\rangle$ and $\langle W,{\in^*}\rangle$ of those theories, respectively, with the same underlying set $W$ and the same induced inclusion relation $\of=\of^*$.

For example, we cannot determine in $\of$-based set-theoretic mereology whether the continuum hypothesis holds or fails, whether the axiom of choice holds or fails or whether there are large cardinals or not. Initially, the following central theorem may appear to be a positive result for mereology, since it identifies precisely what are the principles of set-theoretic mereology, considered as the theory of $\langle V,{\of}\rangle$. Namely, $\of$ is an atomic unbounded relatively complemented distributive lattice, and this is a finitely axiomatizable complete theory. So in a sense, this theory simply is the theory of $\of$-based set-theoretic mereology.

Theorem. Set-theoretic mereology, considered as the theory of $\langle V,\of\rangle$, is precisely the theory of an atomic unbounded relatively complemented distributive lattice, and furthermore, this theory is finitely axiomatizable, complete and decidable.

But upon reflection, since every finitely axiomatizable complete theory is decidable, the result actually appears to be devastating for set-theoretic mereology as a foundation of mathematics, because a decidable theory is much too simple to serve as a foundational theory for all mathematics. The full spectrum and complexity of mathematics naturally includes all the instances of many undecidable decision problems and so cannot be founded upon a decidable theory. Finally, it follows as a corollary that the structure consisting of the hereditarily finite sets under inclusion forms an elementary substructure of the full set-theoretic mereological universe $$\langle \text{HF},\of\rangle\prec\langle V,\of\rangle.$$ Consequently set-theoretic mereology cannot properly treat or even express the various concepts of infinity that arise in mathematics.

Some previous posts on this blog:

# Freiling’s axiom of symmetry, or throwing darts at the real line, Graduate Student Colloquium, April 2016

This will be a talk I’ll give at the CUNY Graduate Center Graduate Student Colloquium on Monday, April 11 (new date!), 2016, 4-4:45 pm.  The talk will be aimed at a general audience of mathematics graduate students.

Abstract. I shall give an elementary presentation of Freiling’s axiom of symmetry, which is the principle asserting that if $x\mapsto A_x$ is a function mapping every real $x\in[0,1]$ in the unit interval to a countable set of such reals $A_x\subset[0,1]$, then there are two reals $x$ and $y$ for which $x\notin A_y$ and $y\notin A_x$.  To argue for the truth of this principle, Freiling imagined throwing two darts at the real number line, landing at $x$ and $y$ respectively: almost surely, the location $y$ of the second dart is not in the set $A_x$ arising from that of the first dart, since that set is countable; and by symmetry, it shouldn’t matter which dart we imagine as being first. So it may seem that almost every pair must fulfill the principle. Nevertheless, the principle is independent of the axioms of ZFC and in fact it is provably equivalent to the failure of the continuum hypothesis.  I’ll introduce the continuum hypothesis in a general way and discuss these foundational matters, before providing a proof of the equivalence of $\neg$CH with the axiom of symmetry. The axiom of symmetry admits natural higher dimensional analogues, such as the case of maps $(x,y)\mapsto A_{x,y}$, where one seeks a triple $(x,y,z)$ for which no member is in the set arising from the other two, and these principles also have an equivalent formulation in terms of the size of the continuum.

# Set Theory Day at the CUNY Graduate Center, March 11, 2016

Vika Gitman, Roman Kossak and Miha Habič have been very kind to organize what they have called Set Theory Day, to be held Friday March 11 at the CUNY Graduate Center in celebration of my 50th birthday. This will be an informal conference focussing on the research work of my various PhD graduate students, and all the lectures will be given by those who were or are currently a PhD student of mine. It will be great! I am very pleased to count among my former students many who have now become mathematical research colleagues and co-authors of mine, and I am looking forward to hearing the latest. If you want to hear what is going on with infinity, then please join us March 11 at the CUNY Graduate Center!

(The poster was designed by my student Erin Carmody, who graduated last year and now has a position at Nebraska Wesleyan.)

# Diamond on the ordinals

I was recently surprised to discover that if there is a definable well-ordering of the universe, then the diamond principle on the ordinals holds for definable classes, automatically. In fact, the diamond principle for definable classes is simply equivalent in ZFC to the existence of a definable well-ordering of the universe. It follows as a consequence that the diamond principle for definable classes, although seeming to be fundamentally scheme-theoretic, is actually expressible in the first-order language of set theory.

In set theory, the diamond principle asserts the existence of a sequence of objects $A_\alpha$, of growing size, such that any large object at the end is very often anticipated by these approximations.  In the case of diamond on the ordinals, what we will have is a definable sequence of $A_\alpha\subseteq\alpha$, such that for any definable class of ordinals $A$ and any definable class club set $C$, there are ordinals $\theta\in C$ with $A\cap\theta=A_\theta$.  This kind of principle typically allows one to undertake long constructions that will diagonalize against all the large objects, by considering and reacting to their approximations $A_\alpha$. Since every large object $A$ is often correctly approximated that way, this enables many such constructions to succeed.


Theorem. In $\ZFC$, if there is a definable well-ordering of the universe, then $\Diamond_{\Ord}$ holds for definable classes. That is, there is a $p$-definable sequence $\langle A_\alpha\mid\alpha<\Ord\rangle$, such that for any definable class $A\of\Ord$ and any definable closed unbounded class of ordinals $C\of\Ord$ (allowing parameters), there is some $\theta\in C$ with $A\cap\theta=A_\theta$.

Proof. The theorem is proved as a theorem scheme; namely, I shall provide a specific definition for the sequence $\vec A=\langle A_\alpha\mid\alpha<\Ord\rangle$, using the same parameter $p$ as the definition of the global well-order and with a definition of closely related syntactic complexity, and then prove as a scheme, a separate statement for each definable class $A\of\Ord$ and class club $C\of\Ord$, that there is some $\alpha\in C$ with $A\cap\alpha=A_\alpha$. The definitions of the classes $A$ and $C$ may involve parameters and have arbitrary complexity.

Let $\lhd$ be the definable well-ordering of the universe, definable by a specific formula using some parameter $p$. I define the $\Diamond_{\Ord}$-sequence $\vec A=\langle A_\alpha\mid\alpha<\Ord\rangle$ by transfinite recursion. Suppose that $\vec A\restrict\theta$ has been defined. I shall let $A_\theta=\emptyset$ unless $\theta$ is a $\beth$-fixed point above the rank of $p$ and there is a set $A\of\theta$ and a closed unbounded set $C\of\theta$, with both $A$ and $C$ definable in the structure $\langle V_\theta,\in\rangle$ (allowing parameters), such that $A\cap\alpha\neq A_\alpha$ for every $\alpha\in C$. In this case, I choose the least such pair $(A,C)$, minimizing first on the maximum of the logical complexities of the definitions of $A$ and of $C$, and then minimizing on the total length of the defining formulas of $A$ and $C$, and then minimizing on the Gödel codes of those formulas, and finally on the parameters used in the definitions, using the well-order $\lhd\restrict V_\theta$. For this minimal pair, let $A_\theta=A$. This completes the definition of the sequence $\vec A=\langle A_\alpha\mid\alpha\in\Ord\rangle$.

Let me remark on a subtle point, since the meta-mathematical issues loom large here. The definition of $\vec A$ is internal to the model, and at stage $\theta$ we ask about subsets of $\theta$ definable in $\langle V_\theta,\in\rangle$, using the truth predicate for this structure. If we were to run this definition inside an $\omega$-nonstandard model, it could happen that the minimal formula we get is nonstandard, and in this case, the set $A$ would not actually be definable by a standard formula. Also, even when $A$ is definable by a standard formula, it might be paired (with some constants), with a club set $C$ that is defined only by a nonstandard formula (and this is why we minimize on the maximum of the complexities of the definitions of $A$ and $C$ together). So one must give care in the main argument keeping straight the distinction between the meta-theoretic natural numbers and the internal natural numbers of the object theory $\ZFC$.

Let me now prove that the sequence $\vec A$ is indeed a $\Diamond_{\Ord}$-sequence for definable classes. The argument follows in spirit the classical proof of $\Diamond$ in $L$, subject to the mathematical issues I mentioned. If the sequence $\vec A$ is not a diamond sequence, then there is some definable class $A\of\Ord$, defined in $\langle V,\in\rangle$ by a specific formula $\varphi$ and parameter $z$, and definable club $C\of\Ord$, defined by some $\psi$ and parameter $y$, with $A\cap\alpha\neq A_\alpha$ for every $\alpha\in C$. We may assume without loss that these formulas are chosen so as to be minimal in the sense of the construction, so that the maximum of the complexities of $\varphi$ and $\psi$ are as small as possible, and the lengths of the formulas, and the Gödel codes and finally the parameters $z,y$ are $\lhd$-minimal, respectively, successively. Let $m$ be a sufficiently large natural number, larger than the complexity of the definitions of $\lhd$, $A$, $C$, and large enough so that the minimality condition we just discussed is expressible by a $\Sigma_m$ formula. Let $\theta$ be any $\Sigma_m$-correct ordinal above the ranks of the parameters used in the definitions. It follows that the restrictions $\lhd\restrict V_\theta$ and also $A\cap\theta$ and $C\cap\theta$ and $\vec A\restrict\theta$ are definable in $\langle V_\theta,\in\rangle$ by the same definitions and parameters as their counterparts in $V$, that $C\cap\theta$ is club in $\theta$, and that $A\cap\theta$ and $C\cap\theta$ form a minimal pair using those definitions with $A\cap\alpha\neq A_\alpha$ for any $\alpha\in C\cap\theta$. Thus, by the definition of $\vec A$, it follows that $A_\theta=A\cap\theta$. Since $C\cap\theta$ is unbounded in $\theta$ and $C$ is closed, it follows that $\theta\in C$, and so $A_\theta=A\cap\theta$ contradicts our assumption about $A$ and $C$. So there are no such counterexample classes, and thus $\vec A$ is a $\Diamond_{\Ord}$-sequence with respect to definable classes, as claimed.
QED

Theorem. The following are equivalent over $\ZFC$.

1. There is a definable well-ordering of the universe, using some set parameter $p$.
2. $V=\HOD_{\{p\}}$, for some set $p$.
3. $\Diamond_{\Ord}$ holds for definable classes. That is, there is a set parameter $p$ and a definable sequence $\vec A=\langle A_\alpha\mid\alpha<\Ord\rangle$, such that for any definable class $A\of\Ord$ and definable class club $C\of\Ord$, there is some $\alpha\in C$ with $A\cap\alpha=A_\alpha$.

Proof. Let me first give the argument, and then afterward discuss some issues about the formalization, which involves some subtle issues.

($1\to 2$) $\newcommand\rank{\text{rank}}$Suppose that $\lhd$ is a $p$-definable well-ordering of $V$, which means that every set has a $\lhd$-minimal element. Let us refine this order by defining $x\lhd’ y$, just in case $\rank(x)<\rank(y)$ or $\rank(x)=\rank(y)$ and $x\lhd y$. The new order is also a well-order, which now respects rank. In particular, the order $\lhd’$ is set-like, and so every object $x$ is the $\alpha^{th}$ element with respect to the $\lhd’$-order, for some ordinal $\alpha$. Thus, every object is definable from $p$ and an ordinal, and so $V=\HOD_{\{p\}}$, as desired.

($2\to 1$) If $V=\HOD_{\{p\}}$, then we have the canonical well-order of $\HOD$ using parameter $p$, similar to how one shows that the axiom of choice holds in $\HOD$. Namely, define $x\lhd y$ if and only if $\rank(x)<\rank(y)$, or the ranks are the same, but $x$ is definable from $p$ and ordinal parameters in some $V_\theta$ with a smaller $\theta$ than $y$ is, or the ranks are the same and the $\theta$ is the same, but $x$ is definable in that $V_\theta$ by a formula with a smaller Gödel code, or with the same formula but smaller ordinal parameters. It is easy to see that this is a $p$-definable well-ordering of the universe.

($1\to 3$) This is the content of the theorem above.

($3\to 1$) If $\vec A$ is a $p$-definable $\Diamond_{\Ord}$-sequence for definable classes, then it is easy to see that if $A$ is a set of ordinals, then $A$ must arise as $A_\alpha$ for unboundedly many $\alpha$. In $\ZFC$, using the axiom of choice, it is a standard fact that every set is coded by a set of ordinals. So let us define that $x\lhd y$, just in case $x$ is coded by a set of ordinals that appears earlier on $\vec A$ than any set of ordinals coding $y$. This is clearly a well-ordering, since the map sending $x$ to the ordinal $\alpha$ for which $A_\alpha$ codes $x$ is an $\Ord$-ranking of $\lhd$. So there is a $p$-definable well-ordering of the universe.
QED

An observant reader will notice some meta-mathematical issues concerning the previous theorem. The issue is that statements 1 and 2 are known to be expressible by statements in the first-order language of set theory, as single statements, but for statement 3 we have previously expressed it only as a scheme of first-order statements. So how can they be equivalent? The answer is that the full scheme-theoretic content of statement 3 follows already from instances in which the complexity of the definitions of $A$ and $C$ are bounded. Basically, once one gets the global well-order, then one can construct a $\Diamond_{\Ord}$-sequence that works for all definable classes. In this sense, we may regard the diamond principle $\Diamond_{\Ord}$ for definable classes as not really a scheme of statements, but rather equivalent to a single first-order assertion.

Lastly, let me consider the content of the theorems in Gödel-Bernays set theory or Kelley-Morse set theory. Of course, we know that there can be models of these theories that do not have $\Diamond_{\Ord}$ in the full second-order sense. For example, it is relatively consistent with ZFC that an inaccessible cardinal $\kappa$ does not have $\Diamond_\kappa$, and in this case, the structure $\langle V_\kappa,\in,V_{\kappa+1}\rangle$ will satisfy GBC and even KM, but it won’t have $\Diamond_{\Ord}$ with respect to all classes, even though it has a definable well-ordering of the universe (since there is such a well-ordering in $V_{\kappa+1}$). But meanwhile, there will be a $\Diamond_{\Ord}$-sequence that works with respect to classes that are definable from that well-ordering and parameters, simply by following the construction given in the theorem.

This leads to several extremely interesting questions, about which I am currently thinking, concerning instances where we can have $\Diamond_\kappa$ for definable classes in $V_\kappa$, even when the full $\Diamond_\kappa$ fails. Stay tuned!

# Set-theoretic mereology: the theory of the subset relation is decidable


To give a few examples, if $\newcommand\HF{\text{HF}}\HF$ is the set of hereditarily finite sets, then $\langle\HF,\of\rangle$, using the usual subset relation, is an unbounded atomic locally Boolean lattice. More generally, if $V$ is any model of set theory (even a very weak theory is sufficient), then $\langle V,\of\rangle$ is an unbounded atomic locally Boolean lattice.

I should like to prove here that the theory of unbounded atomic locally Boolean lattice orders is decidable, and furthermore admits elimination of quantifiers down to the language including the Boolean operations and the relations expressing the height or size of an object, $|x|\geq n$ and $|x|=n$.

Theorem. Every formula in the language of lattices is equivalent, over the theory of unbounded atomic locally Boolean lattices, to a quantifier-free formula in the language of the order $a\of b$, equality $a=b$, meet $a\intersect b$, join $a\union b$, relative complement $a-b$, constant $0$, the unary relation $|x|\geq n$, and the unary relation $|x|=n$, where $n$ is respectively any natural number.

Proof. We prove the result by induction on formulas. The collection of formulas equivalent to a quantifier-free formula in that language clearly includes all atomic formulas and is closed under Boolean combinations. So it suffices to eliminate the quantifier in a formula of the form $\exists x\, \varphi(x,\ldots)$, where $\varphi(x,\ldots)$ is quantifier-free in that language. Let us make a number of observations that will enable various simplifying assumptions about the form of $\varphi$.

Because equality of terms is expressible by the identity $a=b\iff a\of b\of a$, we do not actually need $=$ in the language (and here I refer to the use of equality in atomic formulas of the form $s=t$ where $s$ and $t$ are terms, and not to the incidental appearance of the symbol $=$ in the unary predicate $|x|=n$, which is an unrelated use of this symbol, a mere stylistic flourish). Similarly, in light of the equivalence $a\of b\iff |a-b|=0$, we do not need to make explicit reference to the order $a\of b$. So we may assume that all atomic assertions in $\varphi$ have the form $|t|\geq n$ or $|t|=n$ for some term $t$ in the language of meet, join, relative complement and $0$. We may omit the need for explicit negation in the formula by systematically applying the equivalences:
$$\neg(|t|\geq n)\iff \bigvee_{k<n}|t|=k\quad\text{ and}$$
$$\neg(|t|=n)\iff (|t|\geq n+1)\vee\bigvee_{k<n}|t|=k.$$
So we have reduced to the case where $\varphi$ is a positive Boolean combination of expressions of the form $|t|\geq n$ and $|t|=n$.

Let us consider the form of the terms $t$ that may arise in the formula. List all the variables $x=x_0,x_1,\ldots,x_N$ that arise in any of the terms appearing in $\varphi$, and consider the Venn diagram corresponding to these variables. The cells of this Venn diagram can each be described by a term of the form $\bigwedge_{i\leq N} \pm x_i$, which I shall refer to as a cell term, where $\pm x_i$ means that either $x_i$ appears or else we have subtracted $x_i$ from the other variables. Since we have only relative complements in a locally Boolean lattice, however, and not absolute complements, we need only consider the cells where at least one variable appears positively, since the exterior region in the Venn diagram is not actually represented by any term. In this way, every term in the language of locally Boolean lattices is a finite union of such cell terms, plus $\emptyset$ (which I suppose can be viewed as an empty union). Note that distinct cell terms are definitely representing disjoint objects in the lattice.

Next, by considering the possible sizes of $s-t$, $s\intersect t$ and $t-s$, observe that
$$|s\union t|\geq n\iff \bigvee_{i+j+k=n}(|s|\geq i+j)\wedge(|s\intersect t|\geq j)\wedge(|t|\geq j+k).$$
Through repeated application of this, we may reduce any assertion about $|t|$ for a term to a Boolean combination of assertions about cell terms. (Note that size assertions about $\emptyset$ are trivially settled by the theory and can be eliminated.)

Let us now focus on the quantified variable $x$ separately from the other variables, for it may appear either positively or negatively in such a cell term. More precisely, each cell term in the variables $x=x_0,x_1,\ldots,x_N$ is equivalent to $x\intersect c$ or $c-x$, for some cell term $c$ in the variables $x_1,\ldots,x_N$, that is, not including $x$, or to the term $x-(x_1\union\cdots\union x_N)$, which is the cell term for which $x$ is the only positive variable.

We have reduced the problem to the case where we want to eliminate the quantifier from $\exists x\, \varphi$, where $\varphi$ is a positive Boolean combination of size assertions about cell terms. We may express $\varphi$ in disjunctive normal form and then distribute the quantifier over the disjunct to reduce to the case where $\varphi$ is a conjunction of size assertions about cell terms. Each cell term has the form $x\intersect c$ or $c-x$ or $x-(x_1\union\cdots x_N)$, where $c$ is a cell term in the list of variables without $x$. Group the conjuncts of $\varphi$ that use the same cell term $c$ in this way together. The point now is that assertions about whether there is an object $x$ in the lattice such that certain cell terms obey various size requirements amount to the conjunction of various size requirements about cells in the variables not including $x$. For example, the assertion $$\exists x\,(|x\intersect c|\geq 3)\wedge(|x\intersect c|\geq 7)\wedge(|c-x|=2)$$ is equivalent (over the theory of unbounded atomic locally Boolean lattices) to the assertion $|c|\geq 9$, since we may simply let $x$ be all but $2$ atoms of $c$, and this will have size at least $7$, which is also at least $3$. If contradictory assertions are made, such as $\exists x\, (|x\intersect c|\geq 5\wedge |x\intersect c|=3)$, then the whole formula is equivalent to $\perp$, which can be expressed without quantifiers as $0\neq 0$.

Next, the key observation of the proof is that assertions about the existence of such $x$ for different cell terms in the variables not including $x$ will succeed or fail independently, since those cell terms are representing disjoint elements of the lattice, and so one may take the final witnessing $x$ to be the union of the witnesses for each piece. So to eliminate the quantifier, we simply group together the atomic assertions being made about the cell terms in the variables without $x$, and then express the existence assertion as a size requirement on those cell terms. For example, the assertion $$\exists x\, (|c\intersect x|\geq 5)\wedge(|c-x|=6)\wedge (|d\intersect x|\geq 7),$$ where $c$ and $d$ are distinct cell terms, is equivalent to $$(|c|\geq 11)\wedge(|d|\geq 7),$$ since $c$ and $d$ are disjoint and so we may let $x$ be the appropriate part of $c$ and a suitable piece of $d$. The only remaining complication concerns instances of the term $x-(x_1\union\cdots\union x_N)$. But for these, the thing to notice is that any single positive size assertion about this term is realizable in our theory, since we have assumed that the lattice is unbounded, and so there will always be as many atoms as desired disjoint from any finite list of objects. But we must again pay attention to whether the requirements expressed by distinct clauses are contradictory.

Altogether, I have provided a procedure for eliminating quantifiers from any assertion in the language of locally Boolean lattices, down to the language augmented by unary predicates expressing the size of an object. This procedure works in any unbounded atomic locally Boolean lattice, and so the theorem is proved. QED

Corollary. The theory of unbounded atomic locally Boolean lattices is complete.

Proof. Every sentence in this theory is equivalent by the procedure to a quantifier-free sentence in the stated language. But since such sentences have no variables, they must simply be a Boolean combination of trivial size assertions about $0$, such as $(|0|\geq 2)\vee \neg(|0|=5)$, whose truth value is settled by the theory. QED

Corollary. The structure of hereditarily finite sets $\langle\HF,\of\rangle$ is an elementary substructure of the entire set-theoretic universe $\langle V,\of\rangle$, with the inclusion relation.

Proof. These structures are both unbounded atomic locally Boolean lattices, and so they each support the quantifier-elimination procedure. But they agree on the truth of any quantifier-free assertion about the sizes of hereditarily finite sets, and so they they must agree on all truth assertions about objects in $\HF$. QED

Corollary. The structure $\langle V,\of\rangle$ has a decidable theory. The structure $\langle\HF,\of\rangle$ has a decidable elementary diagram, and hence a computably decidable presentation.

Proof. The theory is the theory of unbounded atomic locally Boolean lattices. Since the structure $\langle\HF,\of\rangle$ has a computable presentation via the Ackerman coding of hereditarily finite sets, for which the subset relation and the size relations are computable, it follows that we may also compute the truth of any formula by first reducing it to a quantifier-free assertions of those types. So this is a computably decidable presentation. QED