Attempt VII

This my seventh attempt at trying to formalize the John function, ...

ZFC Axioms:

0. Axiom schema of Set Builder Notation: "$(\forall E)(\exists Y)(\forall x)[x \in Y \Leftrightarrow x \in E \and Q(x)]$" Where Q(x) is a formula in ZFC set theory.

-“From axiom 0, the set Y = $\lbrace x \in E | Q(x) \rbrace$.”

1. Axiom of Empty Set: ¨$\exist x\forall y \lnot (y\in x)$¨

2. Axiom of Extensionality: "$\forall x \forall y (\forall Z(Z \in x \Leftrightarrow Z \in y) \implies x = y)$"Where x and y are sets.

-"Empty set is notated $~\empty ~$"

3. Axiom of Pairing: "$\forall a\forall b \exists X \forall Y[Y \in X\Leftrightarrow (Y = a \or Y = b)]$" Where a and b are sets.

4. Axiom of subsets: "$\forall n, m \forall A \exists B \forall x (x \in B \Leftrightarrow [x \in A \and p(x,n, m, A)])$" where n, m, and x are sets and p is a property.

5. Axiom of Union: "$\forall A \exists B \forall c (c \in B \Leftrightarrow \exists D (c \in D \and D \in A ))$"

6. Axiom of Power sets: "$\forall x \exists P(x) \forall z[z \in P(x) \Leftrightarrow \forall w (w \in z \implies w \in P(x)) ]$" Where x, P(x), and z are sets

7. Axiom of Foundation: "$\forall S [S \neq \empty \implies (\exists x \in S)S \cap x = \empty ]$"

8. Axiom of infinity: "$\exist S (\empty \in S \and \forall x \in S ((x-1)\cup \lbrace x-1\rbrace \in S))$"

9. Axiom of replacement: "$\exists x \forall y \in a(\exists z A(y,z) \implies \exists z \in x A(y,z))$"

10. Axiom of choice: "$\forall X [\empty \notin X \implies \exists f:X \rightarrow \bigcup X( \forall A \in X(f(A)\in A)]$"

---

Terms for John Function:

-Define $\Leftrightarrow$as "material equivalence", define $\lnot p$ as "not p", and define $\notin$as "$\lnot \in$.”

-"For any sets A and B, $A \cup B = \lbrace x|x \in A \or x \in B \rbrace$."

-“For any sets A and B, $A \cap B = \lbrace x|x \in A \and x \in B \rbrace$.”

-"For any set n, n-1 = N(n) = $\lbrace x \in \omega|x \cup \lbrace x\rbrace = n \rbrace$

-"For any sets X and Y, $X \subset Y$is true if $(X \cup Y) = Y$" and "For any sets X and Y, $X\subseteq Y$is true if $(X \subset Y) \or (X = Y)$is true."

-"For any sets X and Y, $X \supset Y$is true if $Y \subset X$is true." and "For any sets X and Y, $X \supseteq Y$is true if $(Y \subset X) \or (X = Y)$is true."

-Natural Number definition:"$\N = \lbrace x| x = (x-1)\cup \lbrace x-1\rbrace \rbrace$"

-“For any sets A and B, $A \setminus B = \lbrace x|x \in A \and x \notin B \rbrace$.”

-"For any set S, the power set is$P(S) = \lbrace A | A \subseteq S \rbrace$where A is a finite set of natural numbers."

-"For any set n, n+1 = A(n) = $n \cup \lbrace n \rbrace$"

-"For any set n, n+m = $\overbrace{A(A(\cdots A(n)\cdots))}^{m}$"

-"For any set n, n-m = $\overbrace{N(N( \cdots N(n) \cdots )) }^{m}$"

-"For any set n, $n \times m = \overbrace { n + (n + (n+ (\cdots (n+n) \cdots ) ))}^{m ~amount~of~n 's }$"

-"For any set n, $E(n,m) = \overbrace{ n \times (n \times( \cdots (n \times n ) \cdots )) }^{m~amount~of~n's}$"

-"For any set n, $n \uparrow \uparrow m =\overbrace{ E(E(\cdots E(n) \cdots ))}^{m}$"

-"For any set n, $n \uparrow \uparrow \uparrow m = \overbrace{ n \uparrow\uparrow(n\uparrow\uparrow(\cdots (n \uparrow\uparrow n) \cdots ))}^{m~amount~of~n's}$"

-"For any set n, $n \uparrow\uparrow\uparrow\uparrow m = \overbrace{n\uparrow\uparrow\uparrow(n\uparrow\uparrow\uparrow(n\uparrow\uparrow\uparrow(\cdots (n\uparrow\uparrow\uparrow n ) \cdots)))}^{m~amount~of~n's}$"

-"For any set n, $n \uparrow\uparrow\uparrow\uparrow\uparrow m =\overbrace{n\uparrow\uparrow\uparrow\uparrow(n\uparrow\uparrow\uparrow\uparrow(n\uparrow\uparrow\uparrow\uparrow(\cdots (n\uparrow\uparrow\uparrow\uparrow n) \cdots )))}^{m~amount~of~n's}$"

-The empty set is notated "$\emptyset$"

---

ZFC Language:

If L= ZFC set theory, then L = { { }, ( ), [ ], V₁, V₂, …,C₁, C₂, …, f1^a(f1), f2^a(f2), …, =,$\exist , \forall , \lnot , \and , \or , \Leftrightarrow ,\implies, \in , \empty , \mid$}

Where V are variables, C are constants, f^i is a i-ary function symbol, where a(function) assigns a natural number as the function’s “aray” (For example, f1^a(f1) could make it so that f1 is a 3-ary function).” $\lnot$is "not," $\emptyset$is the empty set, and | is ¨such that"

---

Define Johns function as follows:

-"For any two functions f and g, f[>]g is true if $\forall x \exists y (\forall z > y(f(z)>g(z)))$is true"

-"For any two functions f and g, f[=]g is true if $\forall x \exists y (\forall z > y(f(z) = g(z))$is true."

-For any formula F, sym(F) = The amount of symbols in formula F.

-For any finite set, A, define max(A) as $max(A)= \lbrace x | \forall y \in A (x > y) \rbrace$.

-For any function f, and any ZFC formula F, $f \curlyvee F$is true if the function f is described by the formula F.

-For any set of functions, S,$S[[n]] =\lbrace x | \forall f \in S ~(f(n) = x) \rbrace$

---

"$John(x) = f':\N \rightarrow \N =$$((\forall(f(x)\in Fx) \exists f'(x)) \and ((\omega > f'(x)>max(\lbrace Fx \setminus \lbrace f'(x) \rbrace \rbrace)) \and \lnot (f' [>] John \or f' [=] John)$, where F_x = $\lbrace (f:\N \rightarrow \N) |\forall F \in \lbrace F | sym(F) \leq x \rbrace \exists z((f:\N \rightarrow \N) \curlyvee z) \rbrace[[x]]$, and where F and z in the F_x definition are ZFC formulae"

John^a(n) = $\overbrace{John(John(John(\cdots(n)\cdots)))}^{a~John's}$

John’s Number = $John^{15}(3\uparrow \uparrow\uparrow\uparrow\uparrow 3)$

*P.S. John is NOT my real name, it’s my father’s*