22
$\begingroup$

I want to get this as a tattoo as I love the role maths plays in the universe and the idea that the farthest reaches of what we can ever know, fall short of the limits of what is true, even in mathematics. I've done a lot of research but have yet to find a mathematical symbol version of this theorem.

Is there a way to show even a short part of/ the essence of it/ an example of it using symbols?

Sorry if it's inappropriate to ask this here - you just seem like the corner of the internet with my best hope. Any help would be greatly appreciated - I've been trying to find an answer to this for almost a year. Thank you!

$\endgroup$
  • 12
    $\begingroup$ "This tattoo is provably correct if and only if it is incorrect". $\endgroup$ – Asaf Karagila Jun 2 '15 at 14:32
5
$\begingroup$

A concise version of the first incompleteness theorem might be:

$$\texttt{neither }\;\; \mathbf{PA}\vdash\phi\;\;\texttt{ nor }\;\;\mathbf{PA}\vdash\neg\phi$$

And since I cannot resist, I have to add: but mind, it was the second incompleteness theorem which make the Hilbert Program blew up, not the first. ; )

PS: If you decide to imprint yourself with Hagen von Eitzen's Formula, I would love to see a picture.

$\endgroup$
  • $\begingroup$ Thank you! Learning lots today. I can't find a way of finding this out without sounding stupid but what does the PA actually stand for? $\endgroup$ – onedaylikethis Jun 2 '15 at 23:03
  • $\begingroup$ Interesting that you think the second theorem is more relevant. Do you think it's a more accurate representation of, basically, the idea that within any given system, there are claims which are true, but which cannot be proven to be true? If so do you think Yuval's version works... PA⧸⊢Con(PA) $\endgroup$ – onedaylikethis Jun 2 '15 at 23:05
  • $\begingroup$ PS. I wouldn't have been able to get the tattoo without checking on here first so I will share a pic =) Hopefully July! $\endgroup$ – onedaylikethis Jun 2 '15 at 23:06
  • $\begingroup$ It is meant to be the set of the Peano Axioms: en.wikipedia.org/wiki/… -- The second incompleteness theorem says that a theory cannot prove its own consistency. Be aware that both theorems state some conditions on the "systems", so it does not hold in any system. And also: the first incompl. th. says nothing about true or false, but that there is a formula which is not provable nor is its negation. $\endgroup$ – aphorisme Jun 2 '15 at 23:12
  • 2
    $\begingroup$ You could use $\neg \left( \textbf{PA} \vdash \phi \right) \wedge \neg \left(\textbf{PA} \vdash \neg \phi \right)$ $\endgroup$ – Steven Gubkin Jun 3 '15 at 17:12
51
$\begingroup$

If you have enough skin and endurance, the following is not exactly Gödel's theorem, but an instance of a statement as predicted by Gödel's theorem, that is - with a suitable interpretation - it states that it is not provable (which means that it must be true, but unprovable - or PA is inconsistent). But don't complain if it turns out there is a typo buried inside ...

¬∃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)))〉〉〉〉〉〉〉〉〉〉〉〉

$\endgroup$
  • 3
    $\begingroup$ What is the statement, and how did you generate this thing? $\endgroup$ – Spenser Jun 2 '15 at 14:25
  • 3
    $\begingroup$ Ha! Amazing. Funnily enough I am not looking to cover my entire body. But this is awesome. $\endgroup$ – onedaylikethis Jun 2 '15 at 14:31
  • 12
    $\begingroup$ @Spenser I generated it years ago in an attempt to make Hofstadters Gödel, Escher, Bach more "explicit". It follows the "recipe" as given there, including the precise formulation of axioms and rules of inference, and uses the Chinese Remainder Theorem to encode arbitrarily long sequences of naturals as three naturals. Also "b is a power of 10": ∃n:∃a:∃c:∃d:∃e: ∀p:∀q:∀r:∀s:∀t: ∃f:∃g: 〈〈S(a· SSc)=(b+ (d· S(Sc· Sn))) ∧ (b+ e)=(Sc· Sn)〉 ∧ 〈〈〈¬S(p+ r)=n ∨ ¬S(a· SSc)=(q+ (s· S(Sc· Sp)))〉 ∨ ¬(q+ t)=(Sc· Sp) 〉 ∨ 〈S(a· SSc)=((SSSSSSSSSS0· q)+ (f· S(Sc· SSp))) ∧ ((SSSSSSSSSS0· q)+ g)=(Sc· SSp)〉〉〉 $\endgroup$ – Hagen von Eitzen Jun 2 '15 at 15:10
  • 11
    $\begingroup$ I love that you have this just sitting around, waiting for an application. $\endgroup$ – Emily Jun 2 '15 at 17:41
  • 2
    $\begingroup$ What is the encoding of this formula? It's full of squares in my browser (Chrome). $\endgroup$ – MackTuesday Jun 2 '15 at 20:43
8
$\begingroup$

Gödel's second incompleteness theorem has a succinct description:

$$ PA \not{\vdash} Con(PA). $$

$\endgroup$
  • $\begingroup$ Ooh, Very nice. Thanks. I'm actually after the meaning of the first one. After posting this an explanation came up on this site actually. Do you think this could be used for the first one? F⊢GF↔¬ProvF(⌜GF⌝). $\endgroup$ – onedaylikethis Jun 2 '15 at 14:34
  • $\begingroup$ math.stackexchange.com/questions/839731/… $\endgroup$ – onedaylikethis Jun 2 '15 at 14:34
4
$\begingroup$

You could look at Raymond Smullyan's Godel's Incompleteness Theorems . It gives the development. I don't remember it being so expensive when I bought it, and my bookshelf is now inaccessible.

$\endgroup$
  • $\begingroup$ Thanks. Might try to find a way to peek at one for free. Pricey! $\endgroup$ – onedaylikethis Jun 2 '15 at 15:23

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.