5
$\begingroup$

My understanding is that Godel's first theorem says that there is a sentence that is in a sense true in a formal system F but cannot be derived in that system.

I then hear that Godel actually goes on to construct such a sentence.

My question is, what would this even look like?

For example, in Peano Arithmetic would it be something like:

5 + 3 * 15 ... = ...? Is it long? Is it short? Could it be written on a piece of paper?

If not what is wrong with my thinking?

Thanks

$\endgroup$
  • 3
    $\begingroup$ It is very very very long. The sentence was not constructed, a (partial) recipe for constructing the sentence was given. Since then some "natural" sentences have been constructed, not using the recipe. $\endgroup$ – André Nicolas Oct 10 '15 at 3:39
  • $\begingroup$ See the following post for the construction of the Gödel sentence: math.stackexchange.com/a/34927/137499 $\endgroup$ – Burak Oct 10 '15 at 3:41
  • $\begingroup$ Thanks for that, just how long is the actual formula though out of curiosity. My original question stands on whether it could be written on a piece of paper (however large). Another question is whether we know the first and/or last symbols in it $\endgroup$ – sloth Oct 10 '15 at 8:06
  • 2
    $\begingroup$ Someone on this site has tried to write it; see Hagen von Eitzen's answer to this post. $\endgroup$ – Mauro ALLEGRANZA Oct 10 '15 at 9:45
  • 1
    $\begingroup$ For a brief exercise on "encoding", see this post. If you perform the first steps in the arithmetization process, you can "taste" how it works ... and "measure" how far you have to go to produce an example of Gödel sentence. $\endgroup$ – Mauro ALLEGRANZA Oct 10 '15 at 9:50
17
$\begingroup$

Here's an explicit example, due to Hagen von Eitzen (I've made this answer community wiki so I don't get rep bonus for someone else's hard work):

¬∃b:∃c:∃d:〈∃e:∃f:∃g:〈a=((((((e+ f)+ g)· ((e+ f)+ g))· ((e+ f)+ g))+ ((e+ f)· (e+ f)))+ e) ∧ ∃h:∃i:〈〈∃j:h=(j· Si) ∧ 〈∃j:h=(d+ (j· S(i· Sg))) ∧ ∃j:(d+ j)=(i· Sg)〉〉 ∧ ∀j:〈∃k:S(j+ k)=g ⇒ ∀k:∀l:〈〈〈∃m:h=(k+ (m· S(i· Sj))) ∧ ∃m:(k+ m)=(i· Sj)〉 ∧ 〈∃m:e=(l+ (m· S(f· Sj))) ∧ ∃m:(l+ m)=(f· Sj)〉〉 ⇒ 〈〈¬l=SSSSSSSSSS0 ⇒ 〈〈∃m:h=S(k+ (m· S(i· SSj))) ∧ ∃m:S(k+ m)=(i· SSj)〉 ∧ 〈∃m:b=(l+ (m· S(c· Sj))) ∧ ∃m:(l+ m)=(c· Sj)〉〉〉 ∧ 〈l=SSSSSSSSSS0 ⇒ 〈〈〈∃m:h=S((a+ k)+ (m· S(i· SSj))) ∧ ∃m:S((a+ k)+ m)=(i· SSj)〉 ∧ 〈∃m:b=SSSSSSSSS(m· S(c· S(a+ k))) ∧ ∃m:SSSSSSSSSm=(c· S(a+ k))〉〉 ∧ ∀m:〈∃n:S(m+ n)=a ⇒ 〈∃n:b=SSSSSSSS(n· S(c· S(m+ k))) ∧ ∃n:SSSSSSSSn=(c· S(m+ k))〉〉〉〉〉〉〉〉〉 ∧ ∃e:∃f:∃g:∃h:∃i:〈〈〈〈〈∃j:i=(j· Sf) ∧ ∃j:i=(j· S(f· Sg))〉 ∧ ∀j:∀k:∀l:〈〈〈∃m:S(j+ m)=g ∧ 〈∃m:i=(k+ (m· S(f· Sj))) ∧ ∃m:(k+ m)=(f· Sj)〉〉 ∧ 〈∃m:i=(l+ (m· S(f· SSj))) ∧ ∃m:(l+ m)=(f· SSj)〉〉 ⇒ 〈k=l ∨ 〈∃m:e=(m· S(f· Sj)) ∧ 〈k=Sl ∨ l=Sk〉〉〉〉〉 ∧ ∀j:〈∃k:S(j+ k)=g ⇒ ∀k:∀l:∀m:∀n:〈〈〈〈〈∃o:e=(k+ (o· S(f· Sj))) ∧ ∃o:(k+ o)=(f· Sj)〉 ∧ 〈∃o:h=(l+ (o· S(f· Sj))) ∧ ∃o:(l+ o)=(f· Sj)〉〉 ∧ 〈∃o:h=(m+ (o· S(f· SSj))) ∧ ∃o:(m+ o)=(f· SSj)〉〉 ∧ 〈∃o:h=(n+ (o· S(f· SS(m+ j)))) ∧ ∃o:(n+ o)=(f· SS(m+ j))〉〉 ⇒ 〈〈〈〈〈〈∃o:((j+ l)+ o)=g ∧ 〈∃o:SSSSSSSSSo=k ⇒ l=S0〉〉 ∧ 〈〈〈k=0 ∨ k=SSSSSSS0〉 ∨ k=SSSSSSSS0〉 ⇒ l=Sm〉〉 ∧ 〈〈〈〈〈〈k=S0 ∨ k=SS0〉 ∨ k=SSS0〉 ∨ k=SSSS0〉 ∨ k=SSSSS0〉 ∨ k=SSSSSS0〉 ⇒ 〈l=S(m+ n) ∧ ∀o:〈〈∃p:〈∃q:S(p+ q)=m ∧ 〈∃q:e=(o+ (q· S(f· SS(j+ p)))) ∧ ∃q:(o+ q)=(f· SS(j+ p))〉〉 ∧ ∃p:〈∃q:S(p+ q)=n ∧ 〈∃q:e=(o+ (q· S(f· SS((m+ j)+ p)))) ∧ ∃q:(o+ q)=(f· SS((m+ j)+ p))〉〉〉 ⇒ 〈〈∀p:¬〈〈∃q:S(p+ q)=m ∧ 〈∃q:e=SSSSSS(q· S(f· SS(j+ p))) ∧ ∃q:SSSSSSq=(f· SS(j+ p))〉〉 ∧ 〈∃q:e=(o+ (q· S(f· SSS(j+ p)))) ∧ ∃q:(o+ q)=(f· SSS(j+ p))〉〉 ∨ ∀p:¬〈〈∃q:S(p+ q)=n ∧ 〈∃q:e=SSSSSS(q· S(f· SS((m+ j)+ p))) ∧ ∃q:SSSSSSq=(f· SS((m+ j)+ p))〉〉 ∧ 〈∃q:e=(o+ (q· S(f· SSS((m+ j)+ p)))) ∧ ∃q:(o+ q)=(f· SSS((m+ j)+ p))〉〉〉 ⇒ ∀p:¬〈〈∃q:S(p+ q)=(m+ n) ∧ 〈∃q:e=SSSSSS(q· S(f· SS(j+ p))) ∧ ∃q:SSSSSSq=(f· SS(j+ p))〉〉 ∧ 〈∃q:e=(o+ (q· S(f· SSS(j+ p)))) ∧ ∃q:(o+ q)=(f· SSS(j+ p))〉〉〉〉〉〉〉 ∧ ∀o:〈〈∃p:e=(o+ (p· S(f· SSj))) ∧ ∃p:(o+ p)=(f· SSj)〉 ⇒ 〈〈〈〈〈〈k=0 ∨ k=S0〉 ∨ k=SS0〉 ∨ k=SSSSSSS0〉 ⇒ 〈〈〈〈o=S0 ∨ o=SS0〉 ∨ o=SSS0〉 ∨ o=SSSSSS0〉 ∨ o=SSSSSSS0〉〉 ∧ 〈〈〈〈k=SSS0 ∨ k=SSSS0〉 ∨ k=SSSSS0〉 ∨ k=SSSSSSSS0〉 ⇒ 〈〈o=SSSS0 ∨ o=SSSSS0〉 ∨ ∃p:SSSSSSSSp=o〉〉〉 ∧ 〈k=SSSSSS0 ⇒ ∃p:SSSSSSSSSSp=o〉〉〉〉 ∧ ∀o:〈〈∃p:e=(o+ (p· S(f· SS(m+ j)))) ∧ ∃p:(o+ p)=(f· SS(m+ j))〉 ⇒ 〈〈〈k=0 ⇒ k=o〉 ∧ 〈〈〈k=S0 ∨ k=SS0〉 ∨ k=SSSSSS0〉 ⇒ 〈〈〈〈o=S0 ∨ o=SS0〉 ∨ o=SSS0〉 ∨ o=SSSSSS0〉 ∨ o=SSSSSSS0〉〉〉 ∧ 〈〈〈k=SSS0 ∨ k=SSSS0〉 ∨ k=SSSSS0〉 ⇒ 〈〈o=SSSS0 ∨ o=SSSSS0〉 ∨ ∃p:SSSSSSSSp=o〉〉〉〉〉 ∧ 〈j=0 ⇒ k=0〉〉〉〉〉 ∧ ∃j:〈〈〈g=S(j+ d) ∧ ∃k:e=(k· S(f· Sj))〉 ∧ ∀k:¬〈〈∃l:S(k+ l)=d ∧ 〈∃l:b=SSSSSS(l· S(c· Sk)) ∧ ∃l:SSSSSSl=(c· Sk)〉〉 ∧ ∃l:b=(l· S(c· SSk))〉〉 ∧ ∀k:∀l:〈〈∃m:S(k+ m)=d ∧ 〈∃m:b=(l+ (m· S(c· Sk))) ∧ ∃m:(l+ m)=(c· Sk)〉〉 ⇒ 〈∃m:e=(l+ (m· S(f· SS(j+ k)))) ∧ ∃m:(l+ m)=(f· SS(j+ k))〉〉〉〉 ∧ ∀j:∀k:〈〈∃l:e=(l· S(f· Sj)) ∧ 〈∃l:h=(k+ (l· S(f· SSj))) ∧ ∃l:(k+ l)=(f· SSj)〉〉 ⇒ 〈〈〈〈∃l:e=SSSSSS(l· S(f· SSj)) ∧ ∃l:SSSSSSl=(f· SSj)〉 ∧ 〈∃l:e=SSSSSSSSSS(l· S(f· SSSj)) ∧ ∃l:SSSSSSSSSSl=(f· SSSj)〉〉 ∧ 〈〈〈〈〈〈∃l:e=SSSSSSS(l· S(f· SSSSj)) ∧ ∃l:e=SSS(l· S(f· SSSSSj))〉 ∧ ∃l:e=SSSSSSSS(l· S(f· SSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSj))〉 ∧ ∃l:e=SSSSSSSSS(l· S(f· SSSSSSSSj))〉 ∨ 〈〈〈∃l:e=SSS(l· S(f· SSSSj)) ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSj))〉 ∧ ∃l:e=SSSSSSSSS(l· S(f· SSSSSSSj))〉 ∧ 〈〈∃l:e=SSSS(l· S(f· SSSSSj)) ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSSj))〉 ∨ 〈∃l:e=SSSSS(l· S(f· SSSSSj)) ∧ ∃l:e=SSSSSSSSS(l· S(f· SSSSSSSSj))〉〉〉〉 ∨ 〈〈〈〈〈〈〈〈∃l:e=SSSSSS(l· S(f· SSSSj)) ∧ ∃l:e=SSSSSSSSSSS(l· S(f· SSSSSj))〉 ∧ ∃l:e=SSS(l· S(f· SSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSSj))〉 ∧ ∃l:e=SSSSSSSS(l· S(f· SSSSSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSSS(l· S(f· SSSSSSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSSSSSSSj))〉 ∧ ∃l:e=SSSSSSSSSSS(l· S(f· SSSSSSSSSSSSSSj))〉 ∧ 〈〈〈∃l:e=SSSS(l· S(f· SSSSSSSj)) ∧ ∃l:e=SSSSSSSS(l· S(f· SSSSSSSSSSSj))〉 ∧ ∃l:e=SSSS(l· S(f· SSSSSSSSSSSSj))〉 ∨ 〈〈〈∃l:e=SSSSS(l· S(f· SSSSSSSj)) ∧ ∃l:e=SSSS(l· S(f· SSSSSSSSSSSj))〉 ∧ 〈∃l:e=SSSSS(l· S(f· SSSSSSSSSSSSj)) ∧ ∃l:SSSSSl=(f· SSSSSSSSSSSSj)〉〉 ∧ ∃l:e=SSSSSSSSSS(l· S(f· SSSSSSSSSSSSSSSj))〉〉〉〉〉 ∨ ∃l:∃m:〈〈〈〈∃n:S(l+ n)=j ∧ ∃n:e=(n· S(f· Sl))〉 ∧ 〈∃n:h=(m+ (n· S(f· SSl))) ∧ ∃n:(m+ n)=(f· SSl)〉〉 ∧ ∀n:∀o:∀p:〈〈〈〈∃q:i=(n+ (q· S(f· SSl))) ∧ ∃q:(n+ q)=(f· SSl)〉 ∧ ∃q:((l+ o)+ q)=j〉 ∧ 〈∃q:i=(p+ (q· S(f· SS(l+ o)))) ∧ ∃q:(p+ q)=(f· SS(l+ o))〉〉 ⇒ ∃q:(p+ q)=n〉〉 ∧ 〈〈〈〈〈〈〈〈〈〈〈∀n:∀o:〈〈∃p:S(n+ p)=m ∧ 〈∃p:e=(o+ (p· S(f· SS(n+ j)))) ∧ ∃p:(o+ p)=(f· SS(n+ j))〉〉 ⇒ ∃p:e=(o+ (p· S(f· SS(n+ l))))〉 ∨ 〈〈〈∃n:e=SSS(n· S(f· SSj)) ∧ ∃n:SSSn=(f· SSj)〉 ∧ k=m〉 ∧ ∃n:∃o:〈〈S(n+ o)=k ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSS(p+ j))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SSS(p+ (l+ n)))))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=n ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ (j+ o))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (j+ o)))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SSS(p+ l))))〉〉〉〉 ∨ 〈〈〈∃n:e=SSSSSSS(n· S(f· SSj)) ∧ ∃n:SSSSSSSn=(f· SSj)〉 ∧ k=SSm〉 ∧ ∀n:∀o:〈〈∃p:S(n+ p)=m ∧ 〈∃p:e=(o+ (p· S(f· SSSS(n+ j)))) ∧ ∃p:(o+ p)=(f· SSSS(n+ j))〉〉 ⇒ 〈∃p:e=(o+ (p· S(f· SS(n+ l)))) ∧ ∃p:(o+ p)=(f· SS(n+ l))〉〉〉〉 ∨ 〈〈〈∃n:e=SSSSSSS(n· S(f· SSl)) ∧ ∃n:SSSSSSSn=(f· SSl)〉 ∧ m=SSk〉 ∧ ∀n:∀o:〈〈∃p:S(n+ p)=k ∧ 〈∃p:e=(o+ (p· S(f· SSSS(n+ l)))) ∧ ∃p:(o+ p)=(f· SSSS(n+ l))〉〉 ⇒ 〈∃p:e=(o+ (p· S(f· SS(n+ j)))) ∧ ∃p:(o+ p)=(f· SS(n+ j))〉〉〉〉 ∨ ∃n:∃o:〈〈〈〈〈〈∃p:h=(n+ (p· S(f· SSSl))) ∧ ∃p:(n+ p)=(f· SSSl)〉 ∧ S(n+ o)=m〉 ∧ 〈∃p:e=SSSSSSSS(p· S(f· SSSj)) ∧ ∃p:SSSSSSSSp=(f· SSSj)〉〉 ∧ 〈∃p:e=SSSSSSSS(p· S(f· SSSS(j+ n))) ∧ ∃p:SSSSSSSSp=(f· SSSS(j+ n))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=n ∧ 〈∃r:e=(q+ (r· S(f· SSSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSSS(p+ j))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ l)))) ∧ ∃r:(q+ r)=(f· SSS(p+ l))〉〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSSSS(p+ (j+ n))))) ∧ ∃r:(q+ r)=(f· SSSSS(p+ (j+ n)))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ (l+ n))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (l+ n)))〉〉〉〉 ∨ ∃n:∃o:〈〈〈〈〈〈∃p:h=(n+ (p· S(f· SSSj))) ∧ ∃p:(n+ p)=(f· SSSj)〉 ∧ S(n+ o)=k〉 ∧ 〈∃p:e=SSSSSSSS(p· S(f· SSSl)) ∧ ∃p:SSSSSSSSp=(f· SSSl)〉〉 ∧ 〈∃p:e=SSSSSSSS(p· S(f· SSSS(l+ n))) ∧ ∃p:SSSSSSSSp=(f· SSSS(l+ n))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=n ∧ 〈∃r:e=(q+ (r· S(f· SSSS(p+ l)))) ∧ ∃r:(q+ r)=(f· SSSS(p+ l))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSS(p+ j))〉〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSSSS(p+ (l+ n))))) ∧ ∃r:(q+ r)=(f· SSSSS(p+ (l+ n)))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ (j+ n))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (j+ n)))〉〉〉〉 ∨ 〈〈∃n:e=SS(n· S(f· SSl)) ∧ ∃n:SSn=(f· SSl)〉 ∧ ∀n:∀o:〈〈∃p:S(n+ p)=k ∧ 〈∃p:e=(o+ (p· S(f· SS(n+ j)))) ∧ ∃p:(o+ p)=(f· SS(n+ j))〉〉 ⇒ ∃p:e=(o+ (p· S(f· SSS(n+ l))))〉〉〉 ∨ ∃n:〈〈〈∃o:h=(n+ (o· S(f· SSSl))) ∧ ∃o:(n+ o)=(f· SSSl)〉 ∧ 〈∃o:e=SS(o· S(f· SSl)) ∧ ∃o:SSo=(f· SSl)〉〉 ∧ ∀o:∀p:〈〈∃q:S(o+ q)=k ∧ 〈∃q:e=(p+ (q· S(f· SS(o+ j)))) ∧ ∃q:(p+ q)=(f· SS(o+ j))〉〉 ⇒ ∃q:e=(p+ (q· S(f· SSS(o+ (l+ n)))))〉〉〉 ∨ 〈k=SSm ∧ ∃n:∃o:〈〈〈〈S(n+ o)=m ∧ 〈∃p:e=S(p· S(f· SSj)) ∧ ∃p:Sp=(f· SSj)〉〉 ∧ 〈∃p:e=S(p· S(f· SSl)) ∧ ∃p:Sp=(f· SSl)〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSSSS(p+ (j+ n))))) ∧ ∃r:(q+ r)=(f· SSSSS(p+ (j+ n)))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SSS(p+ l))))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=n ∧ 〈∃r:e=(q+ (r· S(f· SSSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSSS(p+ j))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SSS(p+ (l+ o)))))〉〉〉〉 ∨ ∃n:∃o:∃p:∃q:〈〈〈m=SSq ∧ 〈∃r:e=SSSSSS(r· S(f· SSl)) ∧ ∃r:SSSSSSr=(f· SSl)〉〉 ∧ 〈∃r:e=(n+ (r· S(f· SSSl))) ∧ ∃r:(n+ r)=(f· SSSl)〉〉 ∧ 〈∀r:〈∃s:〈∃t:S(s+ t)=p ∧ 〈∃t:e=(r+ (t· S(f· S(o+ s)))) ∧ ∃t:(r+ t)=(f· S(o+ s))〉〉 ⇒ ∀s:¬〈〈∃t:S(s+ t)=q ∧ 〈∃t:e=SSSSSS(t· S(f· SSSS(l+ s))) ∧ ∃t:SSSSSSt=(f· SSSS(l+ s))〉〉 ∧ 〈∃t:e=(r+ (t· S(f· SSSSS(l+ s)))) ∧ ∃t:(r+ t)=(f· SSSSS(l+ s))〉〉〉 ∧ ∃r:∃s:〈〈∃t:r=(t· Ss) ∧ 〈∃t:r=(k+ (t· S(s· Sq))) ∧ ∃t:(k+ t)=(s· Sq)〉〉 ∧ ∀t:∀u:∀v:∀w:〈〈〈〈∃x:S(t+ x)=q ∧ 〈∃x:r=(u+ (x· S(s· St))) ∧ ∃x:(u+ x)=(s· St)〉〉 ∧ 〈∃x:r=(v+ (x· S(s· SSt))) ∧ ∃x:(v+ x)=(s· SSt)〉〉 ∧ 〈∃x:e=(w+ (x· S(f· SSSS(l+ t)))) ∧ ∃x:(w+ x)=(f· SSSS(l+ t))〉〉 ⇒ 〈〈¬w=n ⇒ 〈〈∃x:e=(w+ (x· S(f· SS(j+ u)))) ∧ ∃x:(w+ x)=(f· SS(j+ u))〉 ∧ v=Su〉〉 ∧ 〈w=n ⇒ 〈∀x:∀y:〈〈∃z:S(x+ z)=p ∧ 〈∃z:e=(y+ (z· S(f· S(o+ x)))) ∧ ∃z:(y+ z)=(f· S(o+ x))〉〉 ⇒ 〈∃z:e=(y+ (z· S(f· SS((x+ u)+ j)))) ∧ ∃z:(y+ z)=(f· SS((x+ u)+ j))〉〉 ∧ v=(p+ u)〉〉〉〉〉〉〉〉 ∨ ∃n:〈∀o:〈〈〈∃p:S(o+ p)=j ∧ ∃p:e=(p· S(f· So))〉 ∧ ∀p:∀q:∀r:〈〈〈〈∃s:i=(q+ (s· S(f· So))) ∧ ∃s:(q+ s)=(f· So)〉 ∧ 〈∃s:i=(r+ (s· S(f· SS(p+ o)))) ∧ ∃s:(r+ s)=(f· SS(p+ o))〉〉 ∧ ∃s:S((o+ p)+ s)=j〉 ⇒ ∃s:S(q+ s)=r〉〉 ⇒ ∀p:¬〈〈〈∃q:h=(p+ (q· S(f· So))) ∧ ∃q:(p+ q)=(f· So)〉 ∧ ∃q:〈∃r:S(q+ r)=p ∧ 〈∃r:e=(n+ (r· S(f· S(o+ q)))) ∧ ∃r:(n+ r)=(f· S(o+ q))〉〉〉 ∧ ∀q:¬〈〈∃r:S(q+ r)=p ∧ 〈∃r:e=SSSSSS(r· S(f· S(o+ q))) ∧ ∃r:SSSSSSr=(f· S(o+ q))〉〉 ∧ 〈∃r:e=(n+ (r· S(f· SS(o+ q)))) ∧ ∃r:(n+ r)=(f· SS(o+ q))〉〉〉〉 ∧ 〈〈〈∃o:e=SSSSSS(o· S(f· SSj)) ∧ ∃o:SSSSSSo=(f· SSj)〉 ∧ 〈∃o:e=(n+ (o· S(f· SSSj))) ∧ ∃o:(n+ o)=(f· SSSj)〉〉 ∧ ∀o:∀p:〈〈∃q:S(o+ q)=m ∧ 〈∃q:e=(p+ (q· S(f· SSSS(o+ j)))) ∧ ∃q:(p+ q)=(f· SSSS(o+ j))〉〉 ⇒ 〈∃q:e=(p+ (q· S(f· SS(o+ l)))) ∧ ∃q:(p+ q)=(f· SS(o+ l))〉〉〉〉〉 ∨ ∃n:∃o:〈〈〈〈∃p:S(n+ p)=j ∧ ∃p:e=(p· S(f· Sn))〉 ∧ 〈∃p:h=(o+ (p· S(f· SSn))) ∧ ∃p:(o+ p)=(f· SSn)〉〉 ∧ ∀p:∀q:∀r:〈〈〈〈∃s:i=(p+ (s· S(f· SSn))) ∧ ∃s:(p+ s)=(f· SSn)〉 ∧ ∃s:((n+ q)+ s)=j〉 ∧ 〈∃s:i=(r+ (s· S(f· SS(n+ q)))) ∧ ∃s:(r+ s)=(f· SS(n+ q))〉〉 ⇒ ∃s:(r+ s)=p〉〉 ∧ 〈〈〈〈〈〈〈∃p:e=SS(p· S(f· SSj)) ∧ ∃p:SSp=(f· SSj)〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=m ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSS(p+ j))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SS(p+ l))))〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ (j+ m))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (j+ m)))〉〉 ⇒ ∃r:e=(q+ (r· S(f· SS(p+ n))))〉〉 ∨ 〈〈〈∃p:e=S(p· S(f· SSl)) ∧ ∃p:Sp=(f· SSl)〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ l)))) ∧ ∃r:(q+ r)=(f· SSS(p+ l))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SS(p+ n)))) ∧ ∃r:(q+ r)=(f· SS(p+ n))〉〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=k ∧ 〈∃r:e=(q+ (r· S(f· SS(p+ j)))) ∧ ∃r:(q+ r)=(f· SS(p+ j))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ (l+ o))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (l+ o)))〉〉〉〉 ∨ 〈〈∃p:e=SSS(p· S(f· SSj)) ∧ ∃p:SSSp=(f· SSj)〉 ∧ ∃p:∃q:∃r:〈〈〈〈〈S(p+ q)=k ∧ S(p+ r)=m〉 ∧ S(r+ q)=o〉 ∧ ∀s:∀t:〈〈∃u:S(s+ u)=p ∧ 〈∃u:e=(t+ (u· S(f· SSS(s+ j)))) ∧ ∃u:(t+ u)=(f· SSS(s+ j))〉〉 ⇒ ∃u:e=(t+ (u· S(f· SSS(s+ l))))〉〉 ∧ ∀s:∀t:〈〈∃u:S(s+ u)=r ∧ 〈∃u:e=(t+ (u· S(f· SSS(s+ n)))) ∧ ∃u:(t+ u)=(f· SSS(s+ n))〉〉 ⇒ 〈∃u:e=(t+ (u· S(f· SSS(s+ (l+ p))))) ∧ ∃u:(t+ u)=(f· SSS(s+ (l+ p)))〉〉〉 ∧ ∀s:∀t:〈〈∃u:S(s+ u)=q ∧ 〈∃u:e=(t+ (u· S(f· SSS(s+ (j+ p))))) ∧ ∃u:(t+ u)=(f· SSS(s+ (j+ p)))〉〉 ⇒ ∃u:e=(t+ (u· S(f· SSS(s+ (n+ r)))))〉〉〉〉 ∨ ∃p:〈〈〈〈〈〈〈〈∃q:e=SSSSSS(q· S(f· SSj)) ∧ ∃q:SSSSSSq=(f· SSj)〉 ∧ 〈∃q:e=(p+ (q· S(f· SSSj))) ∧ ∃q:(p+ q)=(f· SSSj)〉〉 ∧ 〈∃q:e=SSSSSS(q· S(f· SSn)) ∧ ∃q:SSSSSSq=(f· SSn)〉〉 ∧ 〈∃q:e=(p+ (q· S(f· SSSn))) ∧ ∃q:(p+ q)=(f· SSSn)〉〉 ∧ 〈∃q:e=S(q· S(f· SSSSn)) ∧ ∃q:Sq=(f· SSSSn)〉〉 ∧ ∀q:∀r:〈〈∃s:S(q+ s)=m ∧ 〈∃s:e=(r+ (s· S(f· SSSS(q+ j)))) ∧ ∃s:(r+ s)=(f· SSSS(q+ j))〉〉 ⇒ 〈∃s:e=(r+ (s· S(f· SSSSS(q+ n)))) ∧ ∃s:(r+ s)=(f· SSSSS(q+ n))〉〉〉 ∧ ∀q:∀r:∀s:〈〈〈∃t:S(q+ t)=m ∧ 〈∃t:e=(r+ (t· S(f· SS(l+ q)))) ∧ ∃t:(r+ t)=(f· SS(l+ q))〉〉 ∧ 〈∃t:e=(s+ (t· S(f· SSSS(j+ q)))) ∧ ∃t:(s+ t)=(f· SSSS(j+ q))〉〉 ⇒ 〈〈s=p ⇒ r=SSSSSSSSS0〉 ∧ 〈¬s=p ⇒ r=s〉〉〉〉 ∧ ∃q:∃r:〈〈∃s:q=SSSS((m+ l)+ (s· S(r· SSSSj))) ∧ ∃s:SSSS((m+ l)+ s)=(r· SSSSj)〉 ∧ ∀s:∀t:∀u:∀v:∀w:〈〈〈〈〈∃x:S(s+ x)=m ∧ 〈∃x:q=(t+ (x· S(r· SSSS(j+ s)))) ∧ ∃x:(t+ x)=(r· SSSS(j+ s))〉〉 ∧ 〈∃x:q=(u+ (x· S(r· SSSSS(j+ s)))) ∧ ∃x:(u+ x)=(r· SSSSS(j+ s))〉〉 ∧ 〈∃x:e=(v+ (x· S(f· SSSS(j+ s)))) ∧ ∃x:(v+ x)=(f· SSSS(j+ s))〉〉 ∧ 〈∃x:e=(w+ (x· S(f· St))) ∧ ∃x:(w+ x)=(f· St)〉〉 ⇒ 〈〈v=p ⇒ 〈〈u=SSt ∧ 〈∃x:e=(p+ (x· S(f· SSt))) ∧ ∃x:(p+ x)=(f· SSt)〉〉 ∧ w=SSSSSSSS0〉〉 ∧ 〈¬v=p ⇒ 〈u=St ∧ w=v〉〉〉〉〉〉〉 ∨ 〈∃p:〈〈〈S(n+ o)=j ∧ 〈∃q:i=(p+ (q· S(f· Sl))) ∧ ∃q:(p+ q)=(f· Sl)〉〉 ∧ 〈∃q:i=(p+ (q· S(f· SSj))) ∧ ∃q:(p+ q)=(f· SSj)〉〉 ∧ ∀q:∀r:〈〈∃s:S((l+ q)+ s)=j ∧ 〈∃s:i=(r+ (s· S(f· SS(l+ q)))) ∧ ∃s:(r+ s)=(f· SS(l+ q))〉〉 ⇒ ∃s:S(p+ s)=r〉〉 ∧ 〈〈〈∃p:e=S(p· S(f· SSj)) ∧ ∃p:Sp=(f· SSj)〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=m ∧ 〈∃r:e=(q+ (r· S(f· SSS(p+ j)))) ∧ ∃r:(q+ r)=(f· SSS(p+ j))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SS(p+ l)))) ∧ ∃r:(q+ r)=(f· SS(p+ l))〉〉〉 ∧ ∀p:∀q:〈〈∃r:S(p+ r)=o ∧ 〈∃r:e=(q+ (r· S(f· SS(p+ n)))) ∧ ∃r:(q+ r)=(f· SS(p+ n))〉〉 ⇒ 〈∃r:e=(q+ (r· S(f· SSS(p+ (j+ m))))) ∧ ∃r:(q+ r)=(f· SSS(p+ (j+ m)))〉〉〉〉〉〉〉〉〉〉〉〉

| cite | improve this answer | |
$\endgroup$
  • 5
    $\begingroup$ Hm... While dazzling, it would be great if someone could unpack this (preferably in English -- I struggle with mathematical German which is the language Hagen writes in). $\endgroup$ – user43208 May 12 '18 at 1:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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