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 all of its quantifiers by $``\subseteq x"$; and $``\text { trs}" $ stands for is transitive.

This theory can prove: Set existence, Empty, Pairing, set Union, Power, Infinity, over the set world of it, also it proves Substitution. It can also prove class comprehension scheme. So it appears to prove all axioms of $\sf MK$-$\sf Reg.$-$\sf Choice$.

Is this theory consistent?

If so, is it equivalent to Bernay's reflection?

  • 1
    $\begingroup$ I think your theory should be equiconsistent with $\mathsf{ZFC}+\{\text{"there is a $\Pi^1_n$-indescribable cardinal"}\mid n<\omega\}$. First-observe that fixing a finite fragment of your theory, and fixing $n$ larger than the number of quantifier alternations in instances of reflection in this fragment, $\mathsf{ZFC}$ will prove that the fragment holds in $V_{\kappa+1}$ for $\Pi^1_n$-indescribable cardinals $\kappa$. $\endgroup$ Dec 10, 2021 at 11:32
  • 1
    $\begingroup$ On the other hand it seems to be easy to show that your theory has $V$ as an internal model of itself + Regularity (where $V$ is the collection of all sets and classes whose transitive closure is well-founded). Next the idea would be to prove the existence of $\Pi^1_n$-indescribable cardinals in this internal modal by reflecting restriction of your Reflection axiom to $\Pi_n$-formulas. But I haven't really checked the details. $\endgroup$ Dec 10, 2021 at 11:32
  • $\begingroup$ @FedorPakhomov, this theory proves Bernays reflection axiom whose consistency is implied by existence of an $\omega$-Erdos cardinal, which appears way higher than the indescribables. en.wikipedia.org/wiki/Reflection_principle $\endgroup$ Dec 10, 2021 at 13:29
  • 1
    $\begingroup$ Note that claim in this wikipedia article doesn't contradict my claim. And the check that $V_{\kappa+1}$, for $\Pi^1_n$-indescribables give models of all finite fragments of your theory is extremely straightforward. $\endgroup$ Dec 10, 2021 at 15:41

2 Answers 2


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). Then ∃w∀t(t∈V-->t∈w). By 3 there is transitive x

such that set(x) and ∃w(w⊆x∧∀t(t⊆x∧t∈V-->t∈w)). Since t⊆x implies set(t),

t⊆x implies t∈x. By 2, there is a c such that t∈c<-->(t∈x∧t∉t). Since set(c),


  • $\begingroup$ @Zuhair, Thank you for the correction. $\endgroup$ Dec 12, 2021 at 18:39
  • $\begingroup$ @GregKiramyer. Thank you for your answer! I've written a possible salvage for this theory, see: mathoverflow.net/questions/410581/…. I hope this would remedy matters!? $\endgroup$ Dec 13, 2021 at 10:57

Here is a partial answer to the second question.

This theory does prove Bernays Reflection axiom, which I think can be stated as: $$ \forall a_1,...,\forall a_n (\varphi(a_1,..,a_n) \to \\\exists \ set \ x : \text { trs}(x) \land \varphi^x(a_1 \cap x,...,a_n \cap x))$$

Where $\varphi$ doesn't use $x$, and all of its free variables are among $a_1,..,a_n$. The other specifications remain the same except that $\varphi$ can use equality.

To see that, we take any formula $\varphi(a_1,..,a_n)$, then form the formula: $$\exists b_1,.., \exists b_n: b_1 \equiv a_n , .., b_n \equiv a_n \land \varphi(b_1|a_1,..,b_n|a_n)$$ Where $\equiv$ is the co-extensionality relation, i.e.; $a \equiv b$ is the formula $ \forall m \, (m \in a \leftrightarrow m \in b)$; and $b_i | a_i$ means that each $b_i$ replaces only and all the occurrences of $a_i$ in formula $\varphi(a_1,..,a_n)$. The intention is to have: $b_i = a_i \cap x$ upon reflecting the $b_i$'s on $x$. This is because each $b_i \equiv a_i$ would turn upon reflecting it on $x$ to: $\forall m \subseteq x \, (m \in b_i \leftrightarrow m \in a_i)$ and beforehand we already have each $b_i \subseteq x$, and since now we have all elements of $a_i$ that are subsets of $x$ being elements of $b_i$, so we have $b_i = a_i \cap x$, regarding the use of equality between two bound variables in $\varphi$, then those upon reflection on $x$ would be subsets of $x$, and so co-extensionality over them would be equivalent to equality between them (Extensionality and equality theory). So Bernays schema is provable in this theory. The problem is whether this theory is even stronger? Or even not consistent?

  • $\begingroup$ Is this an answer or an addition to the question? $\endgroup$
    – Alec Rhea
    Dec 9, 2021 at 16:36
  • $\begingroup$ this is a partial answer to the second question, it establishes that Bernays second order reflection schema is provable in this theory, but it doesn't prove the other direction of the equivalence nor does it answer the first question $\endgroup$ Dec 9, 2021 at 16:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.