# Is this reflection schema equivalent to second order Bernays reflection?

This posting comes as a possible salvage to this earlier presented reflective theory which was proved inconsistent. Attesting the particulars of the underlying language in reflection axioms.

Working in mono-sorted first order logic with equality $$="$$ and membership $$\in"$$:

• Define: $$set(x) \equiv_{df} \exists y \, (x \in y)$$

• Axiomatize:

1. Extensionality: $$( a \subseteq b \land b \subseteq a \to a=b)$$

2. Separation: $$(set(a) \to \exists \ set \ x : \forall y \, (y \in x \leftrightarrow y \in a \land \phi ))$$

3. Reflection: $$(\varphi \to \exists \ set \ x : \text { trs}(x) \land \varphi^x)$$

where formulas $$\phi, \varphi$$ do not use $$x"$$; $$\varphi$$ do not use $$="$$; $$\varphi^x$$ is obtained from $$\varphi$$ by merely bounding its quantifiers by $$\subseteq x"$$ if the quantified variable appears only on the right of symbol $$\in$$, and by $$\in x"$$ whenever it appears on the left. $$\text { trs}"$$ stands for is transitive.

Can this syntactic restriction on $$\varphi^x$$ manage to escape inconsistency?

I conjecture that this reflection scheme would be equivalent to second order Bernays reflection schema (page 21) over the rest of axioms of this theory.

This theory is inconsistent.

We note that by 1 and 2 that if set(x) and y⊆x, then set(y).

(a) There is a v such that ∀x(set(x)-->x∈v).

Proof:Suppose not. Then ∀v∃s∃t(s∈t∧s∉v). By 3 there is transitive x such that

  set(x) and ∀v(v⊆x-->∃s∃t(s∈x∧t∈x∧s∈t∧s∉v). In particular

(x⊆x-->∃s∃t(s∈x∧t∈x∧s∈t∧s∉x).  But this is impossible.


Suppose that ∀x(set(x)-->x∈V).

(b)V∉V

Proof:Suppose V∈V. By 2, there is an x such that set(x) and ∀y(y∈x<-->y∈V∧y∉y).

  Then x∈x<-->x∉x.


Then ∃w(w∉w∧∀t(t∈V-->t∈w)). By 3, there is a transitive x such that

∃w(w∈x∧(w∉w∧∀t(t∈x∧t∈V-->t∈w))). But then x=w, and thus w∈w.