Preconditions[]
We don't know the truth of the set theory in our real world. For example, what value of x1 satisfies ∃n(2ℵ0=ℵn)→x1=n∧¬∃n(2ℵ0=ℵn)→x1=0, after all?
To make mathmatical arguments possible, I assume that there exists a variable assignment s, such that for every ZFC theorem θ written in LFOST, Sat([θ],s) holds, where LFOST denotes the language of first-order set-theory that Rayo defined. This does not answer the above question, but fortunately it is not required in order to define the busy beaver function.
Although the valid LFOST variable symbols form xi, I freely use other symbols for readability. It should not affect the length calculation.
L(θ) denotes the length of a LFOST word θ by precedent.
Basic Definitions[]
| Abbreviation | Definition | Length |
|---|---|---|
| x=y | 3 | |
| x∈y | 3 | |
| θ∧ξ | (θ∧ξ) | L(θ)+L(ξ)+3 |
| ¬θ | (¬θ) | L(θ)+3 |
| (θ∨ξ) | ¬(¬θ∧¬ξ) | L(θ)+L(ξ)+12 |
| θ∨ξ | (θ∨ξ) | L(θ)+L(ξ)+12 |
| (θ→ξ) | ¬(¬θ∧ξ) | L(θ)+L(ξ)+9 |
| θ→ξ | (θ→ξ) | L(θ)+L(ξ)+9 |
| ∀x(θ) | ¬∃x(¬θ) | L(θ)+10 |
| ∀x(θ→ξ) | ¬∃x(θ∧¬ξ) | L(θ)+L(ξ)+13 |
| ∀x(θ→¬ξ) | ¬∃x(θ∧ξ) | L(θ)+L(ξ)+10 |
| ∀x1..∀x_n(θ→¬ξ) | ¬∃x1..∃x_n(θ∧ξ) | L(θ)+L(ξ)+4*n+6 |
| θ↔ξ | (θ→ξ)∧(ξ→θ) | 2*(L(θ)+L(ξ))+21 |
| ∀x1..∀x_n∃y1...∃y_m(θ) | ¬∃x1..∃x_n¬∃y1...∃y_m(θ) | L(θ)+(n+m)*4+6 |
Ordered Pairs[]
I employed the "shorter" definition (that is, (x,y)={x,{x,y}} instead of {{x},{x,y}}) because I assumed the Axiom of Regularity just like other ZFC axioms as written in the Preconditions section.
| Abbreviation | Definition | Length |
|---|---|---|
| {x1,x2}=y | x1∈y∧x2∈y∧¬∃z(z∈y∧¬z=x1∧¬z=x2) | 40 |
| (x1,x2)=y | ∃z({x1,x2}=z∧{x1,z}=y) | 87 |
| (x1,x2,x3)=y | ∃z((x2,x3)=z∧(x1,z)=y) | 181 |
| (x1,x2,x3,x4)=y | ∃z((x2,x3,x4)=z∧(x1,z)=y) | 275 |
| (x1,x2,...,x_n)=y | ∃z((x2,x3,...,x_n)=z∧(x1,z)=y) | 87+94*(n-2) |
| (x1,x2)∈y | ∃z((x1,x2)=z∧z∈y) | L((x1,x2)=y)+10=97 |
| (x1,x2,...,x_n)∈y | ∃z((x1,x2,...,x_n)=z∧z∈y) | 97+94*(n-2) |
Functions[]
| Abbreviation | Definition | Length |
|---|---|---|
| f(x)=y | (x,y)∈f | 97 |
| f(x1,x2)=y | (x1,x2,y)∈f | 191 |
| xfy=z | f(x1,x2)=y | 191 # infix notation |
| f(x1,x2)=(y1,y2) | (x1,x2,y1,y2)∈f | 285 |
| f(x1,x2)=(y1,y2,y3) | (x1,x2,y1,y2,y3)∈f | 87+94*3+10=379 |
| f(x1,x2)=(y1,y2,y3,y4) | (x1,x2,y1,y2,y3,y4)∈f | 87+94*4+10=473 |
| IsFn(f(x)=y) | f(x)=y∧∀z(f(x)=z→y=z) | L(f(x)=y)*2+19 |
| IsFn(f(x1,x2)=(y1,y2)) | f(x1,x2)=(y1,y2)∧∀z1∀z2(f(x1,x2)=(z1,z2)→y1=z1∧y2=z2) | L(f(x1,x2)=(y1,y2))*2+29 |
Natual Numbers[]
| Abbreviation | Definition | Length |
|---|---|---|
| X⊆Y | ∀x(x∈X→x∈Y) | 19 |
| Def0(0) | ¬∃x(x∈0) | 10 |
| Def1(1) | 0∈1∧¬∃x(x∈1∧¬x=0) | 25 |
| IsLimit(x) | 0∈x∧∀y(y∈x→∃z(y∈z)) | 29 |
| Meaning: x is a limit ordinal if it is an ordinal. | ||
| IsNat(x) | 6+16+16+6+19+3+10+32=108 | |
| 0∈x∧ # x is not zero. | 3+3=6 | |
| ∀y(y∈x→( | 3+13=16 | |
| ∀z(z∈y→( | 3+13=16 | |
| z∈x∧ # x is transitive. | 3+3=6 | |
| ∀w(w∈z→w∈y) # y is transitive, | 3+3+13=19 | |
| ))∧ # hence x is an ordinal. | 3 | |
| ∃z(y∈z)∧ # x is a limit ordinal. | 4+3+3=10 | |
| ¬IsLimit(y) # x is the least limit ordinal. | 3+29=32 | |
| )) | ||
| Succ(x)=y | y∈ℕ∧x∈y∧¬∃z(z∈ℕ∧x∈z∧z∈y) | 34 |
| must ensure x∈ℕ | ||
| Def2(2) | Succ(1)=2 | 34 |
| Def+(+:ℕ×ℕ→ℕ) | 446+291=737 | |
| ∀x∀y∃z(x∈ℕ∧y∈ℕ→(z∈ℕ∧IsFn(x+y=z)∧ | 4*3+6+3+3+3+9+3+3+191*2+19+3=446 | |
| y=0→x=z∧∃y'(Succ(y)=y'∧∃z'(x+y'=z'∧Succ(z)=z'))) | 3+9+3+3+4+34+3+4+191+3+34=291 | |
| x<y | x∈y | 3 |
| x1+x2+x3=y | ∃z(x1+x2=z∧((x3=0∧y=z)∨(x3=1∧Succ(z)=y))) | 4+191+3+3+3+3+12+3+3+34=259 |
| valid only if x3 is 0 or 1 | ||
| Div2(x)=y | ∃z(y+y=z∧(z=x∨Succ(z)=x)) | 4+191+3+3+12+34=247 |
| Meaning: ⌊x/2⌋=y where ⌊⌋ is the floor function. | ||
| Mod2(x)=y | ∃z∃w(z+z=w∧((w=x∧y=0)∨(Succ(w)=x∧y=1))) | 4+4+191+3+3+3+3+12+34+3+3=263 |
| Meaning: x mod 2 = y. | ||
Although LFOST does not contain constant symbols, we can define "constants" and use them as if they are constant symbols. For example, we can write a formula (∃0(Def0(0))∧φ) to use a "constant symbol" 0 in φ.
Turing Machines[]
I fixed following elements for simplicity and according to Rado's original paper.
- The set of states is {0,1,...,n}.
- The set of tape alphabets is {0,1}.
- The blank symbol is 0.
- The initial state is 1.
- The halting state is 0.
| Abbreviation | Definition | Length |
|---|---|---|
| IsTranFunc(δ,n) | 26+36+797=859 | |
| ∀q∀c∃w∃d∃q'( | 5*4+6=26 | |
| q<n∧c<2→(w<2∧d<2∧q'<n∧ | 3+3+3+9+3+3+3+3+3+3+=36 | |
| IsFn(δ(q,c)=(w,d,q')))) | 379*2+39=797 | |
| Meaning: δ is a transition function of a (n-1)-state TM. | ||
| q: the current state. | ||
| c: the current tape symbol at the head. | ||
| w: the written symbol to the tape. | ||
| d: moving directions. 0=left, 1=right. | ||
| q': the next state. | ||
| DefΔ(Δ,n) | ∀δ(δ∈Δ↔IsTranFunc(δ,n)) | unused (see below) |
| Meaning: Δ is the set of all transition functions of (n-1)-state TMs. The Rayo name does not have to include Δ. IsTranFunc(δ,n) will implicitly define the domain of δ. | ||
| DefConf(Conf:Δ×ℕ→ℕ×2×ℕ×n) | 16+995+24+36+71+855+16+36+36+775=2860 | |
| ∃l∃c∃r∃q( | 4*4=16 | |
| IsFn(Conf(δ,s)=(l,c,r,q))∧ | 473*2+49=995 | |
| l∈ℕ∧c<2∧r∈ℕ∧q<n∧ | 3+3+3+3+3+3+3+3=24 | |
| s=0→l=0∧c=0∧r=0∧q=1∧ | 3+9+3+3+3+3+3+3+3+3=36 | |
| (∃s'(Succ(s)=s')→(∃l'∃c'∃r'∃q'∃w∃d( | 4+34+9+4*6=71 | |
| Conf(δ,s')=(l',c',r',q')∧δ(q,c)=(w,d,q')∧ | 473+3+379=855 | |
| ∃f∃b∃f'∃b'( | 4*4=16 | |
| (d=0→f=l∧b=r∧f'=l'∧b'=r')∧ | 3+9+3+3+3+3+3+3+3+3=36 | |
| (d=1→f=r∧b=l∧f'=r'∧b'=l')∧ | 3+9+3+3+3+3+3+3+3+3=36 | |
| (f'=Div2(f)∧c'=Mod2(f)∧b'=b+b+w)) | 247+3+263+3+259=775 | |
| )))) | ||
| Meaning: the configuration of a (n-1)-state TM with transition function δ is (l,c,r,q) at step s. Callers must quantify δ and s. | ||
| l: the content of left-hand tape (encoded in a bit string). | ||
| c: the symbol at the current head. | ||
| r: the content of right-hand tape (encoded in a bit string). | ||
| q: the current state. | ||
| DefSteps(Steps:Δ→ℕ) | 227+874+2879+480+513+492=5465 | |
| ∀δ∃s(IsFn(Steps(δ)=s)∧ | 2*4+6+97*2+19=227 | |
| IsTranFunc(δ,n)→(s∈ℕ∧ | 859+9+3+3=874 | |
| ∃Conf(DefConf(Conf:Δ×ℕ→ℕ×2×ℕ×n))∧∃l∃c∃r( | 4+2860+3+4*3=2879 | |
| (∃t(Conf(δ,t)=(l,c,r,0)∧ | 4+473+3=480 | |
| ∀u∀l'∀c'∀r'(Conf(δ,u)=(l',c',r',0)→¬u<t))→s=t)∧ | 4*4+6+473+3+9+3+3=513 | |
| (¬∃t(Conf(δ,t)=(l,c,r,0))→s=0) | 3+4+473+9+3=492 | |
| ))) | ||
| Meaning: (n-1)-state TM with transition function δ halts at step s. | ||
| DefShift(Shift:ℕ→ℕ) | 227+18+5472+104+114=5935 | |
| ∀n∃s(IsFn(Shift(n)=s)∧ | 2*4+6+97*2+19=227 | |
| n∈ℕ→(s∈ℕ∧ | 3+9+3+3=18 | |
| ∃Steps(DefSteps(Steps:Δ→ℕ))∧ | 4+5465+3=5472 | |
| ∃δS(Steps(δS)=s∧ | 4+97+3=104 | |
| ∀δ∀t(Steps(δ)=t→¬s<t) | 2*4+6+97+3=114 | |
| ))) | ||
| Meaning: the slowest (n-1)-state TM halts at step s. | ||
| n=265536 | 819+42*5-53-70=906 | |
| Taken from p進大好きbot's excellent blog post with some modifications: | ||
| Omitted (_IsTwo(x_j)∧) because we already have 2. | -(50+3)=-53 | |
| Replaced _IsOrdinal(x_i) with x_i∈ℕ. | -73+3=-70 | |
| Shift(265536)=x1 | 205+6686+1010=7901 | |
| ∃0(Def0(0)∧∃1(Def1(1)∧∃ℕ(IsNat(ℕ)∧∃2(Def2(2)∧ | 10+25+108+34+7*4=205 | |
| ∃+Def+(+:ℕ×ℕ→ℕ∧∃Shift(DefShift(Shift:ℕ→ℕ)∧ | 737+5935+7*2=6686 | |
| ∃n(n=265536∧Shift(n)=x1))))))) | 4+906+3+97=1010 | |
| Meaning: the slowest (265536-1)-state TM halts at step x1. | ||
∴Rayo(7901)>Shift(265536)>BB(265536-1)>BB(10100)
Is 10¹⁰⁰ large enough?[]
As I shown in the above example, once we define a constant, we can refer it with only one symbol regardless of the definition length. Similarly, once we define a function, we can refer it with a constant length regardless of the definition length. I believe 10100 is large enough.