Return to Question

Let Anterior Reflection be the following principle: $$\forall \vec{v}~ \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$

where $\varphi$ is a formula in $\sf FOL(=,\in)$ that doesn't use the symbol $X$, and $\varphi^{X"}$ refers to $\varphi$ being anteriorly bounded by $X$, that is a formula obtained from $\varphi$ by merely bounding some of its quantifiers by $X$ in such a manner that all preceding quantifiers must be bounded by $X$ also, i.e. the bounding by $X$ is closed anteriorly.

Note: bounding is of the form $\exists y \in X, \forall z \in X$.

Clearly, Anterior Reflection together with Specification principle would axiomatize $\sf ZF–Reg.–Powerset$, where Specification is: $$\forall \vec{v} ~ \forall A ~ \exists! x ~ \forall y ~ (y \in x \leftrightarrow y \in A \land \varphi) \text{ ;}$$ for every formula $\varphi$ not using the symbol "$x$".

If we upgrade anterior reflection to work on supertransitive sets, then with specification we get $\sf ZF–Reg.$.

Now, I think this is consistent.

What is the proof of consistency of anterior reflection?

Let Anterior Reflection be the following principle: $$\forall \vec{v}~ \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$

where $\varphi$ is a formula in $\sf FOL(=,\in)$ that doesn't use the symbol $X$, and $\varphi^{X"}$ refers to $\varphi$ being anteriorly bounded by $X$, that is a formula obtained from $\varphi$ by merely bounding some of its quantifiers by $X$ in such a manner that all preceding quantifiers (i.e. appearing on the left of it) must be bounded by $X$ also, i.e. the bounding by $X$ is closed anteriorly.

Note: bounding is of the form $\exists y \in X, \forall z \in X$.

Clearly, Anterior Reflection together with Specification principle would axiomatize $\sf ZF–Reg.–Powerset$, where Specification is: $$\forall \vec{v} ~ \forall A ~ \exists! x ~ \forall y ~ (y \in x \leftrightarrow y \in A \land \varphi) \text{ ;}$$ for every formula $\varphi$ not using the symbol "$x$".

If we upgrade anterior reflection to work on supertransitive sets, then with specification we get $\sf ZF–Reg.$.

Now, I think this is consistent.

What is the proof of consistency of anterior reflection?

Let Anterior Reflection be the following principle: $$\forall \vec{v} \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$

Where $\varphi$ is a formula in $\sf FOL(=,\in)$ that doesn't use the symbol $X$, and $\varphi^{X"}$ refers to $\varphi$ being anteriorly bounded by $X$, that is a formula obtained from $\varphi$ by merely bounding some of its quantifiers by $X$ in such a manner that all preceding quantifiers must be bounded by $X$ also, i.e. the bounding by $X$ is closed anteriorly.

Note: bounding is of the form $\exists y \in X, \forall z \in X$.

Clearly, Anterior Reflection together with Specification principle would axiomatize $\sf ZF-Reg.-Powerset$. Where Specification is: $$\forall \vec{v} \forall A \exists! x \forall y (y \in x \leftrightarrow y \in A \land \varphi)$$; for every formula $\varphi$ not using the symbol "$x$".

If we upgrade anterior reflection to work on supertransitive sets, then with specification we get $\sf ZF-Reg.$.

Now, I think this is consistent.

What is the proof of consistency of anterior reflection?

Let Anterior Reflection be the following principle: $$\forall \vec{v}~ \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$

where $\varphi$ is a formula in $\sf FOL(=,\in)$ that doesn't use the symbol $X$, and $\varphi^{X"}$ refers to $\varphi$ being anteriorly bounded by $X$, that is a formula obtained from $\varphi$ by merely bounding some of its quantifiers by $X$ in such a manner that all preceding quantifiers must be bounded by $X$ also, i.e. the bounding by $X$ is closed anteriorly.

Note: bounding is of the form $\exists y \in X, \forall z \in X$.

Clearly, Anterior Reflection together with Specification principle would axiomatize $\sf ZF–Reg.–Powerset$, where Specification is: $$\forall \vec{v} ~ \forall A ~ \exists! x ~ \forall y ~ (y \in x \leftrightarrow y \in A \land \varphi) \text{ ;}$$ for every formula $\varphi$ not using the symbol "$x$".

If we upgrade anterior reflection to work on supertransitive sets, then with specification we get $\sf ZF–Reg.$.

Now, I think this is consistent.

What is the proof of consistency of anterior reflection?

Let Anterior Reflection be the following principle: $$\forall \vec{v} \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$

Where $\varphi$ is a formula in $\sf FOL(=,\in)$ that doesn't use the symbol $X$, and $\varphi^{X"}$ refers to $\varphi$ being anteriorly bounded by $X$, that is a formula obtained from $\varphi$ by merely bounding some of its quantifiers by $X$ in such a manner that all preceding quantifiers must be bounded by $X$ also, i.e. the bounding by $X$ is closed anteriorly.

Note: bounding is of the form $\exists y \in X, \forall z \in X$.

Clearly, Anterior Reflection together with Specification principle would axiomatize $\sf ZF-Reg.-Powerset$. Where Specification is: $$\forall \vec{v} \forall A \exists! x \forall y (y \in x \leftrightarrow y \in A \land \varphi)$$; for every formula $\varphi$ not using the symbol "$x$".

If we upgrade it to anteriorly reflect on supertransitive sets, then with specification we get $\sf ZF-Reg.$.

Now, I think this is consistent.

What is the proof of consistency of anterior reflection?

Let Anterior Reflection be the following principle: $$\forall \vec{v} \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$

Where $\varphi$ is a formula in $\sf FOL(=,\in)$ that doesn't use the symbol $X$, and $\varphi^{X"}$ refers to $\varphi$ being anteriorly bounded by $X$, that is a formula obtained from $\varphi$ by merely bounding some of its quantifiers by $X$ in such a manner that all preceding quantifiers must be bounded by $X$ also, i.e. the bounding by $X$ is closed anteriorly.

Note: bounding is of the form $\exists y \in X, \forall z \in X$.

Clearly, Anterior Reflection together with Specification principle would axiomatize $\sf ZF-Reg.-Powerset$. Where Specification is: $$\forall \vec{v} \forall A \exists! x \forall y (y \in x \leftrightarrow y \in A \land \varphi)$$; for every formula $\varphi$ not using the symbol "$x$".

If we upgrade anterior reflection to work on supertransitive sets, then with specification we get $\sf ZF-Reg.$.

Now, I think this is consistent.

What is the proof of consistency of anterior reflection?