6
$\begingroup$

Consider a set theory with the following axioms:

  1. separation: $\exists y \forall x (x \in y \leftrightarrow \phi \land x \in a)$ where $y$ is not free in $\phi$
  2. reflection: $\phi \to \exists u \phi^u$

where $\phi^u$ bounds all unbounded quantifiers in $\phi$ to $u$ (see this question). This theory proves:

Result Parameters Formula $\phi$
existence $\top$
pairing $a,b$ $\exists x (x = a) \land \exists x (x = b)$
union $a$ $\forall x_{\in a} \forall y_{\in x} \exists z (z = y)$
infinity $a$ $\exists x (x = a) \land \forall x \exists y (x \in y \land \forall z_{\in y} (z = x))$
collection for a $\Delta_0$ formula $\psi$ $a$ $\forall x_{\in a} \exists y \psi$
transitive model for a $\Delta_0$ formula $\psi$ $\psi \land \forall x \forall y_{\in x} \exists z (z = y)$

What is the consistency strength and interpretability strength of this theory? Can it prove full collection? Has it been studied in the literature?

Improve this question
$\endgroup$
8
  • $\begingroup$ Are you working in a language with bounded quantifiers as primitive syntactic objects different from unbounded quantifiers? In the standard first-order language of set theory, bounded quantifiers are just abbreviations for certain constructs using normal (unbounded) quantifiers, hence it is syntactically impossible to relativize unbounded quantifiers, but not bounded quantifiers. I think your confusion in the other question stems from the fact that normally the relativization notation $\phi^u$ is used only when $u$ is transitive and all parameters of the formula belong to $u$, ... $\endgroup$
    – Emil Jeřábek
    Commented Sep 20, 2022 at 19:10
  • 1
    $\begingroup$ ... in which case relativizing bounded quantifiers does not actually do anything: when $a\in u$ and $u$ is transitive, then $\exists x\in u\,(x\in a\land\psi^u)$ is equivalent to $\exists x\,(x\in a\land\psi^u)$. $\endgroup$
    – Emil Jeřábek
    Commented Sep 20, 2022 at 19:13
  • $\begingroup$ @EmilJeřábek See the quote from reference 3 in the linked question. One can branch on the structure of the formula inside the quantifier, allowing one to relativize unbounded quantifiers only. $\endgroup$
    – user76284
    Commented Sep 20, 2022 at 19:27
  • $\begingroup$ Sure you can do that. But this will recognize only one particular form as a “bounded” quantifier, while its trivial syntactic modifications will still count as “unbounded”. Thus, for example, $(\exists x\,(x\in a\land\psi))^u=\exists x\,(x\in a\land\psi^u)$, while $(\exists x\,(\psi\land x\in a))^u=\exists x\in u\,(\psi^u\land x\in a)$. Is this really what you want? The only robust way of defining the relativization of formulas is to relativize all quantifiers, while keeping in mind that relativized bounded quantifiers (of whatever form) can be simplified for transitive $u$. $\endgroup$
    – Emil Jeřábek
    Commented Sep 21, 2022 at 6:27
  • $\begingroup$ @EmilJeřábek Yes, it only captures bounded quantifiers written in the standard way. $\endgroup$
    – user76284
    Commented Sep 21, 2022 at 16:46

1 Answer 1

Reset to default
7
$\begingroup$

This theory is mutually interpretable with second-order arithmetic $\mathsf{Z}_2$ and $\mathsf{ZFC}-\mathsf{PowerSet}$ (and hence equiconsistent with them). Note that the mentioned theories are well-known to be mutually interpretable: the interpretation of $\mathsf{ZFC}-\mathsf{PowerSet}$ in $\mathsf{Z}_2$ is achieved by carriying out the construction of $L$.

Trivially your theory is a subtheory of $\mathsf{ZFC}-\mathsf{PowerSet}$ and hence is interpretable there. The non-trivial part of interpreting $\mathsf{Z}_2$ in your theory is to show there that there is a model of second-order Peano arithmetic (in the signature with just the successor).

For that you simply take any set $A$ such that it contains an empty set and for any $x\in A$ there is a set of the form $\{x\}\cup x\in A$, i.e. it satisfies $$(\exists x\in A)(\forall y\in x) y\ne y \land (\forall x\in A)(\exists y\in A)((\forall z\in x)z\in y \land (\forall z\in y)(z=x\lor z\in x)).$$ Then you consider (set-encoded) binary relations $E$ on $A$ s.t. $x_1 \mathrel{E} x_2$, for all empty $x_1,x_2\in A$ and for every $x_1 \mathrel{E} x_2$ and $y_1,y_2$ of the shapes $\{x_1\}\cup x_1$, $\{x_2\}\cup x_2$ we have $y_1\mathrel{E} y_2$. Then you construct a least binary relation $E_0$ like this. For this you, starting from a Cartesian square $U$ of $A$ (a set containing at least one presentation of pair $(x,y)$, for all $x,y\in A$), construct the set $E_0\subseteq U$ that consists of all $z\in U$ of the form $(x,y)$ such that some presentation of $(x,y)$ is in every binary relation of the considered form. You put $N$ to be the subset of $A$ consisting only of $E_0$-reflexive points. Finally you define the successor relation $x \mathsf{R} y$ to be $(\exists x',y'\in N)(x\mathrel{E} x'\land y\mathrel{E} y'\land \text{$y'$ is of the shape $\{x'\}\cup x'$})$. The structure $(N,E,S)$, where $E$ serves as equality clearly will be a model of second-order Peano arithmetic.

Your theory doesn't prove collection. In fact even the extension of Zermelo set theory with choice $\mathsf{ZC}$ by your reflection principle doesn't prove collection. For this let me show that $\mathsf{ZFC}$ proves consistency of this theory. We cosider an $\omega$-sequence of ordinals $\omega=\alpha_0<\alpha_1<\ldots$ such that each $\alpha_{n+1}$ is least such that for every transitive model $M$, there is a transitive model $M'\in V_{\alpha_{n+1}}$ for which $M\cap V_{\alpha_n}=M'\cap V_{\alpha_n}$ and $M$ and $M'$ satisfy the same first-order formulas with parameters from $M\cap V_{\alpha_n}$. It is easy to see that for $\alpha_\omega=\lim_{n<\omega} \alpha_n$ the model $V_{\alpha_\omega}$ is a model of $\mathsf{ZC}$ togethe r with reflection.

Don't know if this theory was studied.

Improve this answer
$\endgroup$
8
  • $\begingroup$ Thank you. Do you happen to know of a similar reflection axiom that yields a stronger theory? $\endgroup$
    – user76284
    Commented Sep 21, 2022 at 16:42
  • $\begingroup$ Yes, sure, $\varphi\to\exists u(\varphi^u\land (\forall x\in u)(\psi(x)\mathrel{\leftrightarrow} \psi^u(x)))$. It implies collection over pure first-order logic. $\endgroup$
    – Fedor Pakhomov
    Commented Sep 22, 2022 at 17:15
  • $\begingroup$ Two formulas in the schema... Is it possible to simplify that somehow? $\endgroup$
    – user76284
    Commented Oct 4, 2022 at 22:57
  • $\begingroup$ Indeed there is a room for simplification, the schemata $\exists u(\forall x\in u)(\psi(x)\mathrel{\leftrightarrow}\psi^u(x))$ is equivalent to the previous one. $\endgroup$
    – Fedor Pakhomov
    Commented Oct 5, 2022 at 8:26
  • $\begingroup$ Nice. So just separation + $\exists u (\forall x \in u) (\psi(x) \leftrightarrow \psi^u(x))$ (where $\psi^u$ bounds unbounded quantifiers) seems to create a pretty powerful theory. Is the exact strength of this theory known? (I can ask a separate question if you'd like.) $\endgroup$
    – user76284
    Commented Oct 5, 2022 at 16:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .