3
$\begingroup$

If we add to the wholeness axiom, the axiom of stratified\acyclic replacement, what would be the consistency state and strength of the resulting theory?

The wholeness axiom $\sf WA$, introduced by Paul Corazza, found to be consistent with $\sf V=HOD$, is axiomatized in the first order language with signature $\{ \in , j\}$, where $j$ is a primitive total one place function symbol. An "$\in$-formula" is a formula in which $j$ doesn't occur.

$\sf WA$ is the statement that "$j$ is a non-trivial elementary embedding from $V$ to $V$ over signature $\{ \in \}$".

More explicity:

  • $\exists x: j(x) \neq x$
  • if $\varphi(x_1,..,x_n)$ is an $\in$-formula, then: $$ \forall x_1,.., \forall x_n \\(\varphi(x_1,..,x_n) \iff \varphi(j(x_1),..,j(x_n)))$$

Now, the theory is:

$\sf ZC + \sf Rep^\in + WA$

where $\sf Rep^\in$ is replacement scheme restricted to $\in$-formulas.

To be especially noticed that there is no restriction on $\sf Z$, so $j$ can be used in instances of Separation.

Now, stratified replacement "$\sf Rep^\equiv $" is Replacement schema restricted to stratified formulas.

Stratification criterion is defined after Quine as in Stratified Comprehension, plus the requirement that $j(x)$ is one type higher than $x$.

Equivalently $\sf Rep^\equiv$ can be formalized by the restriction of replacement schema to acyclic formulas, with an edge stipulated to occur between $x$ and $j(x)$ in the definition of acyclic formula.

The rationale beyond this is that the stratification\acyclicity criterion precludes Kunen's known proof of the critical sequence $\langle \kappa_n | n \in \omega \rangle $, defined as usual by $\kappa_0 = \kappa = \operatorname{cp}(j)$ and $\kappa_{n+1} = j(\kappa_n)$, being a set.

So, formally the question is:

Would $\sf ZC + \sf Rep^\in + Rep^\equiv + WA$, be stronger than, $\sf ZC + \sf Rep^\in + WA$ ?

[After note]: Stratified replacement proved to be inconsistent, since it does capture the critical sequence as shown in the answer by Greg Kiramyer. But, still the Acyclic variant remains viable. I initially thought it to be equivalent to the stratified one; I'm realizing now that the proof of equivalence of acyclicity with stratification is not carried for the language using $j$ with this particular specifications of stratification, so they might not be equivalent!? Therefore Acyclic Replacement might stand a chance?!

$\endgroup$
10
  • $\begingroup$ I don't think you want to insist that $j(x)$ have rank exactly one higher than $x$, since for some values of $x$, such as the critical point $\kappa_0$, the value of $j(x)$ will be far higher in the set-theoretic rank hierarchy. But also, there are many $x$s that are fixed by $j$, with $j(x)=x$. Indeed, the definition of the fixed point requires one to refer to these instances, but this is not possible with a $j$-stratified formula. $\endgroup$ Jan 5, 2023 at 16:25
  • $\begingroup$ @JoelDavidHamkins, No, not "rank", I meant "type" after Quine as in NF, this is metatheoretic assignment over variables in a formula of the language. $j(x)$ this is a term symbol, this receives one type higher index (than that of $x$) when stratifying the formula, so you cannot have $j(x) = x $ for example, but you can have $x \in j(x)$, the acyclic version is harsher syntactically speaking, but it turns to be equivalent with stratification over weak axioms. $\endgroup$ Jan 5, 2023 at 16:32
  • $\begingroup$ Yes, I know, but the main idea behind Quine's type stratification is a proxy for set-theoretic rank. This is why when saying $x\in y$ you require that the numerical type (or rank, whatever) of the symbol $x$ is less than that of $y$. $\endgroup$ Jan 5, 2023 at 16:37
  • $\begingroup$ @JoelDavidHamkins, Ah! I see what you mean. To be precise Quine's type stratification is a proxy of TYPE in type theories like TST and TSTU, and this is different from the set rank concept, ranks are accumulative while types are not, actually if one is not careful and try to parallel ranks through stratification typing, then inconsistencies are expected to erupt. Yet of course there is some resemblances with ranks. $\endgroup$ Jan 5, 2023 at 16:44
  • $\begingroup$ But my point is that we may want naturally to refer to objects in $j(x)$ that are higher than $x$, and so the requirement should only be that the type of $j(x)$ is higher than $x$, not exactly one higher. $\endgroup$ Jan 5, 2023 at 16:45

1 Answer 1

5
$\begingroup$

The statement beginning "The rationale beyond" is not quite correct. The critical sequence can be constucted by exploiting the facts that $\bigcup j(x)$ will be assigned the same number as $x$ in a stratification assignment, $\bigcup x=x$ for any limit ordinal, and $\omega$ is well ordered by proper subset relation $\subsetneq$.

Let $F(W,K,x,y)$ be the "formula":

$x∈W \land \exists f: f \text { is a function } \land \\ dom(f)=\{t \in W \mid t \subseteq x\} \land \\ f(0)=K \land f(x)=y\land \\ \forall t((tβ‰ 0 \land t∈ dom(f)) \to \\f(t) = \bigcup j(f(\bigcup \{s∈W \mid s\subsetneq t\}))))$

Then for all $n \in \omega $, there is a unique $y$ such that $F(\omega,\kappa,n,y)$, the $n$-th element of the critical sequence, where $\kappa$ is the critical point of $j$.

$\endgroup$
8
  • $\begingroup$ Thank you for the correction. I eliminated the parenthesis. $\endgroup$ Jan 10, 2023 at 6:25
  • $\begingroup$ I don't see $y$ in the formula? Also why $K$ is there? Do you intend $y=f(x)$, if so, then this needs to be added to your formula. Can you clarify the rule of $K$? $\endgroup$ Jan 10, 2023 at 7:33
  • $\begingroup$ Yes, f(x)=y, but I do not know how to add it to your edit. In the last sentence, K is replaced by πœ…, the critical point. $\endgroup$ Jan 10, 2023 at 9:14
  • $\begingroup$ Good answer!!! The important note here is that your formula though stratified as I defined, yet it is NOT acyclic. I thought those are equivalent, but now I see that they may not be so. Do you have an acyclic variant of this formula? $\endgroup$ Jan 10, 2023 at 11:19
  • $\begingroup$ @Zuhair: If you change {π‘‘βˆˆπ‘Šβˆ£π‘‘βŠ†π‘₯} to {uβˆˆπ‘Šβˆ£uβŠ†π‘₯}, is it still not acyclic? I am too lazy to check. $\endgroup$ Jan 11, 2023 at 1:50

Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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