0
$\begingroup$

In Kanamori's Bernays and Set Theory pages 20-21, a first order reflection principle due to Bernays is mentioned, that of:

$$\sf \varphi \to \exists y \, (\text {Trans}(y) \land \varphi^y)$$ for formulas $\varphi$ without $\sf y$ or any class variables, where $\sf Trans(y) $ asserts that $\sf y$ is transitive; $\sf \varphi ^ y$ denotes the relativization of the formula $\varphi$ to the set $\sf y$, i.e., $\exists x$ is replaced by $\exists x \in \sf y$ and $\forall x$ by $\forall x \in \sf y$. Starting with the observation that set parameters $a_1,...,a_n$ can appear in $\varphi$ and $\sf y$ can be required to contain them by introducing clauses $\exists x(a_i \in x)$ into $\varphi$. Bernays just with his schema established Pair, Union, Infinity, and Replacement (schema)—in effect achieving a remarkably economical presentation of ZF.

My question: what is the proof of replacement from reflection? It's easy to see that Reflection can prove Pairing, Union, and Infinity. But the proof of Replacement is what's escaping me.

I tried to reflect the formula: $\exists x (a \in x) \land \forall m \in a \exists ! z: \phi(m,z)$ on the transitive set $\sf y$, but what we'll get is a set (which is $\sf y$) that contains the $z$'s of $\phi^\sf y$ among its elements, and I don't know how those are the same $z$'s of $\phi$?

Improve this question
$\endgroup$
6
  • 2
    $\begingroup$ This reflection doesn't imply Replacement even over Zermelo set theory. Indeed $\mathsf{ZF}$ proves existence of a model of $\mathsf{Z}+\mathsf{Ref}$ (where $\mathsf{Ref}$ is the reflection prinicple you stated). Namely it is $V_\kappa$ that is $\Sigma_1$-elementary submodel of $V$; such $\kappa$ exists by Levy Reflection. A reflection principle that actually implies Pair, Union, Infinity, and Replacement over Regularity+Separation+Extensionality is $\exists y(\mathsf{Trans}(y)\land \vec{p}\in y\land \forall \vec{x}\in y(\varphi(\vec{p},\vec{x})\leftrightarrow \varphi^y(\vec{p},\vec{x})))$. $\endgroup$
    – Fedor Pakhomov
    Commented Dec 13, 2021 at 17:27
  • $\begingroup$ @FedorPakhomov, but that's not what Kanamori seems to be saying. The referenced articled clearly speaks of the reflection axiom as I quoted and not the one you've mentioned. $\endgroup$
    – Zuhair Al-Johar
    Commented Dec 14, 2021 at 11:31
  • 2
    $\begingroup$ Then there should be mistake in Kanamori's paper. At least in proof theory it is relatively well-known that transitive model reflection (the principle that you have written) doesn't imply full scheme of replacement. Namely there are several papers about the proof theory of $\mathsf{KP}+\mathsf{Ref}$; and its proof-theoretic strength is known to be below that of the fragment $\Pi^1_2$-$\mathsf{CA}_0$ of the second-order arithmetic. $\endgroup$
    – Fedor Pakhomov
    Commented Dec 14, 2021 at 12:24
  • $\begingroup$ I think the proof of replacement might be the same as13. 3. 5 of Potter's Set Theory and its philosophy. That is, the scheme allow the use of set terms, or actually set functions. This way replacement would straighforwardly follow. $\endgroup$
    – Zuhair Al-Johar
    Commented Dec 17, 2021 at 16:52
  • $\begingroup$ @FedorPakhomov "A reflection principle that actually..." Do you know of any other, possibly simpler, axiom schemas with this property? $\endgroup$
    – user76284
    Commented Jan 11, 2023 at 1:43

1 Answer 1

Reset to default
1
$\begingroup$

The above reflection scheme does not imply the existence of an empty set, nor does it imply the existence of more than one element. In the domain with one element which is an element of itself, the reflection scheme holds.

Let T0 be the theory whose axioms are extensionality, foundation and the above reflection scheme. If ZF is consistent, then pairing, union, power set and some instances of separation are not provable from T0.

Proof:Let A=ωU{{1},{{1}}}. Let U(y) be a formula which holds iff y∈A or (y∉Vω and for every x∉Vω which is in the transitive closure of {y}, the intersection of Vω with the transitive closure of x is A).

Then relativized to U, the above reflection scheme holds, but pairing, union, some instances of separation, and power set do not.

Let T1 be the theory whose axioms are the axioms of T0, power set, and all instances of separation. Then if ZF is consistent, there are instances of replacement not provable from T1.

Proof: Define a sequence s by s0=0, and s(n+1)=U{b|there is a "formula 𝜑 with parameters from V(sn) such that b is the least ordinal for which 𝜑 holds in Vb"}

Let t=U{sn| n∈ω}. Then all the axioms of T1 hold in Vt, but there are instances of replacement that do not. For example,

let ψ(n,x) be a formula which holds iff n∈ω and x=sn.

Improve this answer
$\endgroup$
4
  • $\begingroup$ what that still stand if we added power to T1? $\endgroup$
    – Zuhair Al-Johar
    Commented Dec 12, 2021 at 6:56
  • $\begingroup$ @Zuhair, I have added power set to the axioms of T1. All the axioms of T1 except power set hold in L(ℵ1). $\endgroup$
    – Greg Kirmayer
    Commented Dec 12, 2021 at 22:45
  • 1
    $\begingroup$ How does one square this with the question's quote? $\endgroup$
    – user76284
    Commented Dec 13, 2021 at 3:16
  • $\begingroup$ @user76284, I think Bernays formulation allows the use of set terms, that is defined set symbols, or even defined predicate symbols, that way the result is immediate! $\endgroup$
    – Zuhair Al-Johar
    Commented Mar 1 at 8:03

You must log in to answer this question.

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