Sasquatch

Emlightened extended Little Bigeddon and defined Sasquatch (Big Bigeddon) in her blog post on March 27, 2017 as follows.

We work in the language \((\in, \bar\in, \lt)\), where equality is a defined symbol. \(\in\), \(\bar\in\) and \(\lt\) are binary predicates, we also define the unary functions \(F\) and \(R\) from these.

Fix a Godel numbering of formulae:

• \(\ulcorner t_1 \in t_2 \urcorner = \langle 0, \llcorner t_1 \lrcorner, \llcorner t_2 \lrcorner \rangle\)
• \(\ulcorner \varphi \wedge \psi \urcorner = \langle 1, \ulcorner \varphi \urcorner, \ulcorner \psi \urcorner \rangle\)
• \(\ulcorner \lnot\varphi \urcorner = \langle 2, \ulcorner \varphi \urcorner \rangle\)
• \(\ulcorner \forall x_i\varphi \urcorner = \langle 3, \llcorner x_i \lrcorner, \ulcorner \varphi \urcorner \rangle\)

And of terms:

• \(\llcorner x_i \lrcorner = \langle 4, i \rangle\)
• \(\llcorner a \lrcorner = \langle 5, a \rangle\)
• \(\llcorner R(t) \lrcorner = \langle 6, \llcorner t \lrcorner \rangle\)
• \(\llcorner F(t') \lrcorner = \langle 7, \llcorner t' \lrcorner \rangle\)

Where \(t'\) contains no free variables, and \(\llcorner a \lrcorner\) represents the set \(a\)

Fix \(\lt\) to be a wellordering of \(V\). As there is no guarantee that this is, in general, definable, let it be the standard wellorder of \(HOD\) in the standard class forcing extension \(V[G]\) where \(V=HOD\).

Let \(\llcorner a\lrcorner \bar \in \llcorner b\lrcorner \leftrightarrow a\in b\) for all sets \(a\), \(b\), and adjunction be the binary function \((a,b)\mapsto a\cup\{b\}\).

If \((\bar\in,R,F)\vDash t\text{ is an ordinal}\), define \(R(t)\) inductively as \(R(0) = \emptyset\), \(R(\alpha) = (\text{closure of }R(\beta)\cup\{R(\beta)\}\cup C\text{ under adjunction and }F)^\bar\in\) where \(C=(5\times V)^\in\)\(\beta\) is the \(\bar\in\)-maximal element of \(\alpha\) if it exists, and \(R(\lambda) = \cup^\bar\in\{R(\theta):\theta\bar\in\lambda\}\) if it does not. Otherwise, \(R(t)=\emptyset\).

Note that we don't explicitly define \(R\) in \(V\), just for \(\bar\in\). This makes no difference as only the \(\bar\in\) behaviour of \(R\) matters, and we can simply let it's \(\in\) value be \(\llcorner R(\cdot)\lrcorner\) if necessary..

Define \(F(\ulcorner \phi \urcorner)\) (for unary \(\phi\), possibly with parameters) to be \(\{a\}\) where \(a\) is the \(\lt\)-minimal element of \(V\) such that \((\bar\in,R,F)\vDash\phi(a)\) if \(\exists b \varphi(b)\), where \(\varphi\) is obtained by repacing the function \(R\) with a function enumerating the \(\Sigma_n\)-correct cardinals, where \(\phi \in \Sigma_n\) (n minimal, and \(\emptyset\) otherwise.

I conjecture that, for fixed \(V\) and \(\in\), this produces unique values of \(\bar\in\) and \(\lt\). (In the case of ambiguity of 'standard' in the definition of the \(HOD\) class ordering, we'll go with the first one that Thomas Jech taught anyone.) Assuming this to be the case (and even if it's not), we define Sasquatch as:

The largest number \(k\) such that there is some unary formula \(\phi\) in the language \(\{\bar\in,Q\}\) (where \(Q(a,b) \leftrightarrow R(a)=b\)) of quantifier rank \(\leq 12\uparrow\uparrow 12\) such that \(\exists! a (\phi(a)) \wedge \phi(k)\).

Retrieved on April 29, 2017 from the blog post of Emlightened by Fish. License is under CC BY-SA 3.0 according to Fandom's policy.