# Can these short set-building expressions of the finite set world extend to the infinite set world?

A formula of the form $$\forall \vec{p}\, \exists x \, \forall y\, (y \in x \leftrightarrow \phi(y,\vec{p}))$$

is to be named a "set-building" formula.

Now, when $$\vec{p}$$ includes a predicate symbol, then its to be called a second order set-building formula. Otherwise, it is first order. Also, by defining part in a set-building formula, I mean $$\phi(y,\vec{p})$$ in the above expression.

By atomic formula in the first order language of set theory, I mean single identity or membership formula, i.e. of the form $$x \in y$$ or $$x=y$$. While in the second order language it'll include as well formulas $$P(x_1,\ldots,x_n)$$ for any predicate symbol $$P$$.

The size of a formula is taken here to mean the number of its atomic subformulas. If a subformula have more than one occurrence, then each occurrence is counted as if it is a distinct formula.

Working in $${\sf ZF}-{\sf Reg.}+ {\sf HF} \text{ exists}$$:

Principle: Any first or second order set-building formula $$\phi$$ in the language of set theory whose defining part is of size $$\leq 4$$, that is satisfied by the set $$\sf HF$$ of all hereditarily finite sets, then it is satisfied by the whole world of sets $$V$$.

Now, clearly all set-building axioms of $$\sf ZFC$$ would be derived from the above rule. Second order Replacement can be written by set-building formula as:

$$\forall P \, \forall a \, \exists x \, \forall y \, (y \in x \leftrightarrow \exists z \in a ( P(z,y) \land \forall u \, (P(z,u) \to u=y)))$$

If we include function symbols in second order atomic formulas, i.e., consider $$F(x) \in y; F(x)=y$$ as second order atomic formulas, then one can even get a short formalization of Replacement as:

$$\forall F \, \forall a \, \exists x \, \forall y \, (y \in x \leftrightarrow \exists z \in a: F(z)= y )$$

Making all set-building rules of $$\sf ZFC$$ derivable using the above principle with defining parts of length $$\leq 2$$.

Now, the shortest expression of finiteness that I know of is the one written by Emil Jeřábek, which is: $$\neg\exists y\,(x\in y\land\forall a\in y\,\exists b\in y\,b\subsetneq a),$$ of size $$6$$.

if we increase the limit on the size of the defining part in the above principle to $$5$$ or even $$6$$. Does this give a clear inconsistency?

Even more daunting (but I think most likely inconsistent) is to say that every first or second order sentence of size $$\leq 5$$ true of the hereditarily finite set world, does generalize over the whole set world. All axioms of $${\sf ZFC}-{\sf Reg.}$$ other than Infinity, are instances of these sentences.

The intuitive idea behind this principle is that very short expressions in the first or second order language of set theory that can define sets and hold over the whole hereditarily finite set world, then the reason for them holding over the entirety of that world has nothing to do with finiteness, it is because they are general set principles! The reason is that they are too short to express finiteness, and so they are reasoned not to be a property of it, so they can go beyond it, and so we can restrict our scope of infinite set world to those infinite sets who obey those rules, since they can in some sense be regarded as close to the strict finite set realm.

• It’s not very clear to me whether you include ZF in the background theory, or if not, how you define $V_\omega$. But anyway, if $\phi(y)$ is the formula $\forall u\in y\,\exists v\in y\,u\in v$ of size $3$, then (ZF proves that) the corresponding set-building sentence is true in $V_\omega$ (as the only finite well-founded set that satisfies $\phi(y)$ is $y=\varnothing$, and $\{\varnothing\}$ exists), but it is false in $V$, as there are sets $y$ of arbitrarily large rank that satisfy $\phi(y)$ (e.g., all limit ordinals). Commented Jul 29 at 12:15
• OTOH, note that if the background theory is consistent with $V=V_\omega$, then it is also consistent with this “Principle” stated for all formulas. Commented Jul 29 at 12:33
• @EmilJeřábek, Yes! Your comment is right. I've modified the original question as to address this. I also mentioned the background theory. Here the set $\sf HF$ of all hereditarily finite sets (where finite is possessing a bijection with a von Neumann natural) is not $V_\omega$, it has non-well founded sets as well. So, the formula you mentioned is not necessarily satisfied in that world. Commented Jul 29 at 18:00
• @EmilJeřábek, if we keep the original choice of $V_\omega$ then we need to reduce the length of defining parts to $\leq 2$, and this would also derive all set-building rules of $\sf ZFC$. Commented Jul 31 at 6:37

let $$\phi(y)$$ be the formula: $$\forall a \, (a \in y \to \forall b \, ( \forall z \, (z \in b \to z=a) \to b \in y))$$, the set-building formula with this formula as its defining part, would define a set in $$\sf HF$$ which is $$\{\varnothing\}$$, but of course cannot be generalized to $$V$$. So, we need the size of the defining part to be $$\leq 3$$. However, this won't affect deriving the set-building rules of $$\sf ZF-Reg.$$ since its enough to have defining parts of size $$\leq 2$$
As regards the second question, the sentence: $$\forall a \neg \exists x \, :a \in x \land \forall y \in x \forall z (\forall u \in z(u=y) \to z \in x)$$, is true of $$\sf HF$$, but not true of $$V$$. So, we need to reduce the size of sentences to be $$\leq 4$$. However, this won't be enough to derive all axioms of $$\sf ZF-Reg-Infinity$$. A possible salvage is to allow formula sizes of $$\leq 5$$ but provided that the first order atomic formulas not exceeding $$3$$, this way we get to capture Separation as: $$\forall A \forall P \exists x: \forall y \, (y \in A \land P(y) \to y \in x) \land \forall y \, (y \in x \to P(y))$$, and the rest of axioms to be written in implicational form.
Of note, with these restrictions it appears that we can use $$V_\omega$$ instead of $$\sf HF$$ and thus maintain an approach that is consistent with Foundation, we need the defining parts of be of size $$\leq 2$$, and for sentences we need them to be of size $$\leq 5$$ but with the first order part of size $$\leq 3$$.
This renders this approach very narrow, that it can barely justify $$\sf ZFC$$. But, nevertheless, if it succeeds, then it speaks of a possible origin of familiarity of those axioms, thereby unravelling their natural genre, it shows that the roots of that lies in familiarity with rules of the strict finite set realm.