Panorama 17. 6. 2013

Noch einmal eine Zusammenfassung des Teils dieser Sitzung, der der Wiederholung und Diskussion der Gödelschen Unvollständigkeitssätze gewidmet war. Dies enthält nun wieder ein paar Feinheiten, die das ganze vielleicht schwieriger erscheinen lassen als es ist. Außer allen Sätzen sind vor allem die Teile in Fettdruck wichtig.

Wir haben uns noch einmal mit den Gödelschen Unvollständigkeitssätzen beschäftigt. Die einfachste Form, die wir formuliert hatten, war:

Satz. Ist $X\supset\mathrm{PA}$ rekursiv aufzählbar und $\mathcal N\models X$, so ist $X$ unvollständig.

Dabei ist $X$ eine Menge von Aussagen in der Sprache der Arithmetik. Nun ist eine solche Aussage zunächst ein rein syntaktisches Gebilde, es ist erst nach Interpretation der Aussage sinnvoll, davon zu reden, ob sie wahr oder falsch ist. Aussagen in der Sprache der Arithmetik können wir aber immer als Aussagen über natürliche Zahlen interpretieren und damit wahr oder falsch nennen. Wenn wir $\mathcal N\models X$ schreiben, so heißt dies gerade, dass alle Aussagen aus $X$ so interpretiert wahr sind. Wenn wir das so verstehen, können wir auch schreiben:

Satz. Ist $X\supset\mathrm{PA}$ rekursiv aufzählbar und enthält $X$ nur wahre Aussagen, so existiert eine wahre Aussage, die sich nicht aus $X$ ableiten lässt.

Der Beweis hiervon lässt sich einfacher skizzieren als ich das in einer früheren Sitzung getan hatte: Es ist möglich, eine Aussage $\gamma$ zu konstruieren, die gerade sagt, dass $\gamma$ nicht aus $X$ ableitbar ist. Wäre $\gamma$ falsch, so ließe sich $\gamma$ also ableiten, es ließe sich aus $X$ also eine falsche Aussage ableiten, was im Widerspruch dazu steht, dass $X$ nur wahre Aussagen enthält. Damit ist $\gamma$ also wahr und nicht aus $X$ ableitbar.

Eigentlich möchte man aber nicht nur über Mengen wahrer Aussagen sprechen. Redet man vom ersten Gödelschen Unvollständigkeitssatz meint man meist eine Form des folgenden, auch wenn dies eigentlich eine Verstärkung des Satzes durch Rosser ist.

Satz. Ist $X\supset\mathrm{PA}$ rekursiv aufzählbar und konsistent, so ist $X$ unvollständig.

Es gibt also eine Aussage, so dass weder diese Aussage noch ihre Negation aus $X$ ableitbar sind. Aber Achtung: Dies muss nicht auf unsere oben konstruierte Aussage $\gamma$ zutreffen, Rossers Konstruktion ist eine andere. Wer in einer populären Darstellung also diese starke Fassung formuliert, dann aber zum Beweis einen Satz der Art „ich bin nicht beweisbar“ vorbringt, der schummelt.

Durchaus aber folgt für die Aussage $\gamma$ von oben, dass $X$ inkonsistent ist, wenn $\gamma$ aus $X$ ableitbar ist. (Wenn $\gamma$ aus $X$ ableitbar ist, so ist diese Tatsache auch in $X$ beweisbar, das heißt $\neg\gamma$ ist aus $X$ ableitbar.)  Das heißt aber, dass $X$ genau dann konsistent ist, wenn $\gamma$ nicht aus $X$ ableitbar ist, was wiederum die Aussage von $\gamma$ ist. Die Grundlage des Beweises des zweiten Gödelschen Unvollständigkeitssatzes ist nun, dass sich die Äquivalenz von $\gamma$ und $Con_X$ (der Konsistenz von $X$) auch in $X$ beweisen lässt. Dies liefert:

Zweiter Gödelscher Unvollständigkeitssatz. Ist $X\supset\mathrm{PA}$ rekursiv aufzählbar und konsistent, so ist $Con_X$ nicht aus $X$ ableitbar.

Betrachten wir ein Beispiel: PA selbst ist konsistent. Dies liegt daran, dass PA ein Modell hat, nämlich das Standardmodell $\mathcal N$. Kurz: PA enthält nur wahre Aussagen. (Dies ist ein Beweis der Konsistenz von PA, den wir in „unserer Mathematik“ geführt haben, in der es ja die Menge der natürlichen Zahlen gibt. Dies ist also ein Beweis der Konsistenz von PA in ZF. Keine Unvollstänidgkeitssätze wurden verletzt.) Also ist $Con_{\mathrm{PA}}$ nicht in PA beweisbar. Das heißt aber, dass $X:=\mathrm{PA} + \neg Con_{\mathrm{PA}}$ konsistent ist. (Wäre $X$ inkonsistent, so ließe sich aus $\mathrm{PA} + \neg Con_{\mathrm{PA}}$ ein Widerspruch herleiten, die Aussage $Con_{\mathrm{PA}}$ wäre also in PA per Widerspruch beweisbar.) $X$ ist also eine konsistente Theorie, die eine falsche Aussage enthält (wobei falsch wie gesagt nur bedeutet, dass sie im Standardmodell $\mathcal N$ nicht gilt). Wir wissen insbesondere, dass auch $X$ unvollständig ist. Aber: Ist $\gamma$ die Aussage, die behauptet, dass $\gamma$ in $X$ nicht beweisbar ist, so ist $\gamma$ wie gehabt äquivalent zu $Con_X$. Da $Con_X$ aber $Con_{\mathrm PA}$ impliziert, ist $\neg\gamma$ aus $X$ ableitbar. $X$ ist also konsistent, behauptet aber seine eigene Inkonsistenz.

All das gilt wie schon früher bemerkt nicht nur für die Sprache der Arithmetik und PA, sondern wo immer man genug Mathematik nachbilden kann, um sinnvoll über Beweisbarkeit zu reden. Insbesondere gilt das für die Sprache der Mengenlehre und ZF, also:

Satz.  Ist $X\supset\mathrm{ZF}$ rekursiv aufzählbar und konsistent, so ist $X$ unvollständig und $Con_X$ nicht aus $X$ ableitbar.

Wir müssen hier nur aufpassen: Im Gegensatz zu der Situation bei PA dürfen wir hier nicht einfach „in ZF lässt sich die Konsistenz von ZF nicht beweisen“ behaupten. Dass es überhaupt eine Aussage gibt, die sich in ZF nicht beweisen lässt, heißt ja, dass ZF konsistent ist. Hätten wir tatsächlich einen Beweis dieser Tatsache, den wir in unserer üblichen Mathematik, also in ZFC, geführt hätten, so würde also ZFC die Konsistenz von ZF beweisen. Von Gödel wissen wir aber (das wurde in einer früheren Sitzung berichtet), dass wenn ZF konsistent ist, auch ZFC konsistent ist. ZFC würde also seine eigene Konsistenz beweisen, was nach dem zweiten Gödelschen Unvollständigkeitssatz nur möglich ist, wenn ZFC inkonsistent ist, was wir doch nicht hoffen wollen. Wir müssen also genau sein und sagen: „Wenn ZF konsistent ist, lässst sich in ZF die Konsistenz von ZF nicht beweisen.“

Panorama 3. 6. 2013

Nun mit einigen Fehlern weniger: Mehr beweisbar Unbeweisbares.

Panorama 31. 5. 2013

Abschluss Unabhängigkeitssätze
Den zweiten Unvollständigkeitssatz habe ich noch einmal umformuliert.

Panorama 24. und 27. 5. 2013

Der erste Gödelsche Unvollständigkeitssatz

Alles technische habe ich dem bereits erwähnten Lehrbuch von Rautenberg entnommen.
Eine nicht-technische Darstellung des Beweises findet sich in dem Buch von Franzén, das sich auch mit der Rezeption des Satzes außerhalb der Mathematik beschäftigt.

Wir haben zunächst die Peano-Axiome im Rahmen der Mengenlehre formuliert. Diese beschreiben die natürlichen Zahlen mit der Nachfolgeroperation bis auf Isomorphie eindeutig, was in Aufgabe 21 gezeigt wurde.

Wir haben dann die Peano-Arithmetik als Theorie erster Ordnung (also in der Prädikatenlogik erster Stufe) eingeführt. Diese ist in der Sprache der Arithmetik $\mathcal L_{\mathrm{ar}}$ formuliert, die ein Konstantenymbol $0$ sowie Funktionssymbole $S$ (Nachfolger), $+$ und $\cdot$ enthält. Aus dem Rautenberg:

Peano-Arithmetik PA

Dabei ist zu beachten, dass das Induktionsschema für jede Formel $\varphi$ ein Axiom liefert, das Axiomensystem $\mathrm{PA}$ ist also unendlich. Dennoch lässt sich von einer gegeben Formel „mechanisch“ feststellen, ob sie eines der Axiome von $\mathrm{PA}$ ist, das wird noch wichtig sein.

Das Standardmodell $\mathcal N$ von $\mathrm{PA}$, also in gewisser Hinsicht das beabsichtige Modell, besteht aus der Menge der hatürlichen Zahlen $\mathbb N$ zusammen mit der Null, sowie der üblichen Nachfolgeroperation, Addition und Multiplikation. Da $\mathrm{PA}$ ein Modell hat, haben wir also sofort (mit dem Korrektheitssatz) den

Satz. $PA$ ist konsistent.

Man muss ein wenig arbeiten, um das einzusehen, aber in $\mathrm{PA}$ lassen sich tatsächlich alle elementaren Zahlentheoretischen Beweise durchführen, sowie ein guter Teil der diskreten Mathematk. $\mathrm{PA}$ taugt damit als Repräsentant für finitistische Mathematik.

Für jede natürliche Zahl $n\in\mathbb N$ definieren den die entsprechende Zahl bezeichnenden Term $\underline n:=\underbrace{SS\cdots S}_{n}0$. Als Warnung und im Gegensatz zu Aufgabe 21 weisen wir auf die Existenz von Nichtstandardmodellen hin.

Satz. Es gibt ein Modell $\mathcal M$ von $\mathrm{PA}$, das außer $\left(\underline n\right)^{\mathcal M}$, $n\in\mathbb N$, noch weitere Elemente hat.

Auf den Beweis, der eine leichte Anwendung des Vollständigkeitssatzes ist, haben wir verzichtet. Der Interessierte findet dies als Satz 3.2 bei Rautenberg.

Das Induktionsschema leistet also nicht, was wir vielleicht erwartet hätten. Das mag zunächst verwundern, deutet aber bereits in Richtung des Unvollständigkeitssatzes.

Daraus, dass aber das Standardmodell nur die von $\underline n$ bezeichneten Elemente enthält, erhält man aber folgendes.

Satz/Definition. Es sei $\varphi=\varphi(x)\in\mathcal L_{\mathrm{ar}}$. Gilt $\mathrm{PA}\vdash\exists x\varphi(x)$, so existiert ein $n\in\mathbb N$ mit $\mathrm{PA}\not\vdash\neg\varphi(\underline n)$. Wir sagen, $\mathrm{PA}$ sei $\omega$-konsistent.

Beweis. Sonst gölte $\mathcal N\models\exists x\varphi(x)$, aber $\mathcal N\models\neg\varphi(\underline n)$ für alle $n\in\mathbb N$.

Wir wollen nun als eine Instanz des Gödelschen Unvollständigkeitssatzes skizzieren, dass $\mathrm{PA}$ unvollständig ist, dass also eine Aussage $\gamma\in\mathcal L_{\mathrm{ar}}$ mit $\mathrm{PA}\not\vdash\gamma$ und $\mathrm{PA}\not\vdash\neg\gamma$ existiert. Der Beweis basiert nun darauf, dass der Begriff der Ableitbarkeit in $\mathrm{PA}$ sich arithmetisch (also als Aussage über das Rechnen mit natürlichen Zahlen) formulieren lässt, und dass sich genug Tatsachen darüber in $\mathrm{PA}$ beweisen lassen.

Zunächst führt man ein Schema ein, nachdem man jeder Formel $\gamma$ injektiv eine Gödelnummer $n\in\mathbb N$ zuordnet. Wir schreiben dafür dann $\dot\gamma=n$ und $\lceil\gamma\rceil=\underline n$. Ebenso ordnen wir jeder potentiellen Herleitung einer Formel (man denke an etwas, das aussieht wie die lange Folge von Zeilen in Aufgabe 22. Dieses soll so sein, dass sich auch Formel $bew(n,m)$ angeben lässt, die „sagt“, dass $n$ Gödelnummer eines Beweises einer Formel mit Gödelnummer $m$ ist. Und in der Tat soll sich, wenn das der Fall ist, das auch in $PA$ herleiten lassen. Dies ist zu erreichen, da das Testen, ob etwas eine Herleitung ist, ja tatsächlich rein mechanisch möglich ist (man denke wieder an Aufgabe 22), und wie oben bereits behauptet sich solche Argumente in $\mathrm{PA}$ durchführen lassen. Natürlich wäre hier einiges zu zeigen. Wir können aber genau sagen, was wir erreichen wollen, nämlich, dass für jede jede Formel $\varphi$ die folgenden Implikationen gelten, wobei wir noch $bwb(m):=\exists n\,bew(n,m)$ setzen:\begin{align*}\mathrm{PA}\ \vdash\ \varphi\quad&\Rightarrow\quad\text{Ex. $n\in\mathbb N$ mit $\mathrm{PA}\vdash bew(\underline n,\lceil\varphi\rceil)$}\\&\Rightarrow\quad\mathrm{PA}\vdash bwb(\lceil\varphi\rceil),\\\mathrm{PA}\not\vdash\varphi\quad&\Rightarrow\quad\mathrm{PA}\vdash\neg bew(\underline n,\lceil\varphi\rceil)\text{ f.a. $n\in\mathbb N$}.\end{align*}Nächstes Ziel ist nun, eine Aussage $\gamma$ zu finden, die von sich selber behauptet, nicht in PA beweisbar zu sein. Genauer wollen wir\[\mathrm{PA}\vdash\,\gamma\leftrightarrow\neg bwb(\lceil\gamma\rceil).\]Für eine solche Aussage gilt in der Tat weder $\mathrm{PA}\vdash\gamma$ noch $\mathrm{PA}\vdash\neg\gamma$. Aus ersterem folgte nämlich einerseits aufgrund der Eigenschaft von $\gamma$, dass $\mathrm{PA}\vdash\neg bwb(\lceil\gamma\rceil)$ und andererseits aufgrund einer Eigenschaft von $bwb$, dass $\mathrm{PA}\vdash bwb(\lceil\gamma\rceil)$. Dies widerspräche der Konsistenz von $\mathrm{PA}$. Aus $\mathrm{PA}\not\vdash\gamma$ folgt nun aber nach obigem $\mathrm{PA}\vdash\neg bew(\underline n,\lceil\gamma\rceil)$ für alle $n\in\mathbb N$, was aufgrund der $\omega$-Konsistenz von $\mathrm{PA}$ impliziert, dass $\mathrm{PA}\not\vdash \exists n\,bew(n,\lceil\gamma\rceil)$, also nach Definition von $bwb$ und der Eigenschaft von $\gamma$ auch $\mathrm{PA}\not\vdash\neg\gamma$.

Die Frage ist nun also, wie man an eine solche Aussage $\gamma$ kommt, die etwas über sich selbst behauptet. Gödels Trick benutzt nun textuelle Ersetzung. Später hat Quine folgendes natürlichsprachliche Analogon angegeben:

„ergibt einen unbeweisbaren Satz, wenn man ihm sein Zitat voranstellt.“ ergibt einen unbeweisbaren Satz, wenn man ihm sein Zitat voranstellt.

Dieser Satz sagt von einem anderen, dass er unbeweisbar sei, und dieser andere ist aber gleich ihm selbst. Dabei entspricht das Zitieren mit Anführungszeichen dem Zitieren via Gödelnummer. Auf der technischen Seite zeigt man, dass es man eine Formel $sb(m,n,y)$ konstruieren kann, die sagt, dass $y$ die Gödelnummer der Formel ist, die man erhält, wenn man in der Formel mit Gödelnummer $m$ die Variable $x$ durch $\underline n$ ersetzt, genauer wollen wir für alle Formeln $\varphi=\varphi(x)$ und $n\in\mathbb N$\[PA\,\vdash\,sb(\lceil\varphi\rceil,\underline n,y)\leftrightarrow y=\lceil\gamma(\underline n)\rceil.\]Weiterhin setzt man nun $\beta(z):=\forall y(sb(z,z,y)\rightarrow\neg bwb(y))$ („Die Aussage, die man erhält, wenn man in die Formel mit Gödelnummer z für die Variable x gerade z einsetzt, ist nicht beweisbar“) und $\gamma:=\beta(\lceil\beta\rceil)$. So erhält man in der Tat\begin{align*}\mathrm{PA}\quad&\vdash\quad\gamma\leftrightarrow\forall y(y=\lceil\beta(\lceil\beta\rceil)\rceil\rightarrow\neg bwb(y)),\\\mathrm{PA}\quad&\vdash\quad\gamma\leftrightarrow\neg bwb(\lceil\beta(\lceil\beta\rceil)\rceil),\\\mathrm{PA}\quad&\vdash\quad\gamma\leftrightarrow\neg bwb(\lceil\gamma\rceil).\end{align*}Damit sind wir am Ziel angelangt.

Satz (Gödel). Für obige Aussage $\gamma\in\mathcal L_{\mathrm{ar}}$ gilt $\mathrm{PA}\not\vdash\gamma$ und $\mathrm{PA}\not\vdash\neg\gamma$. PA ist also unvollständig.

Wenn $\gamma$ in PA weder beweisbar noch widerlegbar ist, ist es dann trotzdem sinnvoll zu fragen, ob $\gamma$ wahr ist? In der Tat ist im allgemeinen in der Prädikatenlogik nur sinnvoll von Beweisbarkeit aus einer Formelmenge (wie hier PA) oder Wahrheit in einem Modell zu reden. Nun hat aber PA das Standardmodell $\mathcal N$, und wir können fragen, ob $\gamma$ in diesem erfüllt ist. Der Beweis zeigt, dass das tatsächlich dann der Fall ist, wenn $\gamma$ in PA nicht beweisbar ist.

Bemerkung. Für dieses $\gamma$ gilt $\mathcal N\models\gamma$. In diesem Sinne ist $\gamma$ also wahr.

Damit ist $\mathcal N$ auch Modell von $\mathrm{PA}\cup\{\gamma\}$. Ist diese Formelmenge nun vielleicht vollständig? Immerhin ist $\gamma$ aus ihr ja trivial ableitbar. Sicher ist sie es auch nicht, denn wir können obigen Beweis für sie wiederholen, nur muss $bew$ dann durch eine neue Formel, die die Beweisbarkeit in $\mathrm{PA}\cup\{\gamma\}$ beschreibt, ersetzt werden, und wir erhalten eine neue Aussage $\gamma'$, die in $\mathrm{PA}\cup\{\gamma\}$ weder beweis- noch widerlegbar ist. Allgemeiner könnten wir eine Formelmenge $X\supset\mathrm{PA}$ betrachten und für diese den Beweis durchführen. Es ist dabei lediglich wichtig, dass sich Beweisbarkeit in $X$ auch wieder durch eine Formel ausdrücken lässt. Dies ist gegeben, wenn sich wieder „mechanisch“ überprüfen lässt, ob eine gegebene Formel zu $X$ gehört oder nicht. Wir brauchen zur Formulierung des Ergebnisses daher einen Berechenbarkeitsbegriff, ein ausreichender ist der der rekursiven Aufzählbarkeit. Es gilt dann der folgende

Satz. Ist $X\supset\mathrm{PA}$ rekursiv aufzählbar und $\mathcal N\models X$, so ist $X$ unvollständig.

Man beachte, dass andererseits $X=\{\varphi\in\mathcal L_{\mathrm{ar}}\colon \text{$\varphi$ Aussage, $\mathcal N\models\varphi$}\}$ natürlich vollständig ist. Damit ist diese Menge nicht rekursiv aufzählbar.

Panorama 17. 5. 2013

Den ersten Teil der Vorlesung werde ich im vorherigen Eintrag mit einarbeiten, da er dort inhaltlich hingehört. Hier aber die „Folien“ zur Einführung logischer Grundbegriffe.


Und damit Sie mal eine solche gesehen haben und weil ich offenbar zu viel Zeit habe, hier mit\begin{align*}
AG:=\{&\forall x\forall y (x+y=y+x),
\\&\forall x\forall y\forall z((x+y)+z=x+(y+z)),
\\&\forall x(0+x=x),
\\&\forall x\neg\forall y\neg (x+y=0)
\}\end{align*}eine Herleitung von $AG\vdash\neg(c+a=c+b\land\neg a=b)$. Dabei muss man sich noch für jede Zeile überlegen, mit welcher Regel sie aus welchen vorhergehenden folgt.
\begin{align*}
&&AG&\ \vdash\ \forall x\forall y (x+y=y+x)&&\\
&&AG&\ \vdash\ \forall y (c+y=y+c)&&\\
&&AG&\ \vdash\ c+d=d+c&&\\
&&AG,c+d=0&\ \vdash\ c+d=d+c&&\\
&&AG,c+d=0&\ \vdash\ c+d=0&&\\
&&AG,c+d=0&\ \vdash\ d+c=0&&\\
&&AG,c+a=c+b&\ \vdash\ d+(c+a)=d+(c+a)&&\\
&&AG,c+a=c+b&\ \vdash\ c+a=c+b&&\\
&&AG,c+a=c+b&\ \vdash\ d+(c+a)=d+(c+b)&&\\
&&AG&\ \vdash\ \forall x\forall y\forall z((x+y)+z=x+(y+z))&&\\
&&AG&\ \vdash\ \forall y\forall z((d+y)+z=d+(y+z))&&\\
&&AG&\ \vdash\ \forall z((d+c)+z=d+(c+z))&&\\
&&AG&\ \vdash\ (d+c)+a=d+(c+a)&&\\
&&AG&\ \vdash\ (d+c)+a=(d+c)+a&&\\
&&AG&\ \vdash\ d+(c+a)=(d+c)+a&&\\
&&AG&\ \vdash\ (d+c)+b=d+(c+b)&&\\
&&AG&\ \vdash\ (d+c)+b=(d+c)+b&&\\
&&AG&\ \vdash\ d+(c+b)=(d+c)+b&&\\
&&AG,c+a=c+b&\ \vdash\ d+(c+a)=(d+c)+a&&\\
&&AG,c+a=c+b&\ \vdash\ (d+c)+a=d+(c+b)&&\\
&&AG,c+a=c+b&\ \vdash\ d+(c+b)=(d+c)+b&&\\
&&AG,c+a=c+b&\ \vdash\ (d+c)+a=(d+c)+b&&\\
&&AG,c+d=0,c+a=c+b&\ \vdash\ (d+c)+a=(d+c)+b&&\\
&&AG,c+d=0,c+a=c+b&\ \vdash\ d+c=0&&\\
&&AG,c+d=0,c+a=c+b&\ \vdash\ 0+a=0+b&&\\
&&AG&\ \vdash\ \forall x(0+x=x)&&\\
&&AG&\ \vdash\ 0+a=a&&\\
&&AG&\ \vdash\ 0+b=b&&\\
&&AG,c+d=0,c+a=c+b&\ \vdash\ 0+a=a&&\\
&&AG,c+d=0,c+a=c+b&\ \vdash\ 0+b=b&&\\
&&AG,c+d=0,c+a=c+b&\ \vdash\ a=b&&\\
&&AG,c+d=0,c+a=c+b,\neg a=b&\ \vdash\ a=b&&\\
&&AG,c+d=0,c+a=c+b,\neg a=b&\ \vdash\ \neg a=b&&\\
&&AG,c+d=0,c+a=c+b,\neg a=b&\ \vdash\ \neg c+d=0&&\\
&&AG,\neg c+d=0,c+a=c+b,\neg a=b&\ \vdash\ \neg c+d=0&&\\
&&AG,c+a=c+b,\neg a=b&\ \vdash\ \neg c+d=0&&\\
&&AG,c+a=c+b,\neg a=b&\ \vdash\ \forall y\neg c+y=0&&\\
&&AG&\ \vdash\ \forall x\neg\forall y\neg x+y=0&&\\
&&AG&\ \vdash\ \neg\forall y\neg c+y=0&&\\
&&AG,c+a=c+b,\neg a=b&\ \vdash\ \neg\forall y\neg c+y=0&&\\
&&AG,c+a=c+b,\neg a=b&\ \vdash\ a=b\\
&&AG,c+a=c+b,a=b&\ \vdash\ a=b\\
&&AG,c+a=c+b&\ \vdash\ a=b\\
&&AG,c+a=c+b,c+a=c+b\land\neg a=b&\ \vdash\ a=b\\
&&AG,c+a=c+b,c+a=c+b\land\neg a=b&\ \vdash\ c+a=c+b\land\neg a=b\\
&&AG,c+a=c+b,c+a=c+b\land\neg a=b&\ \vdash\ \neg a=b\\
&&AG,c+a=c+b,c+a=c+b\land\neg a=b&\ \vdash\ \neg(c+a=c+b\land\neg a=b)\\
&&AG,\neg c+a=c+b,c+a=c+b\land\neg a=b&\ \vdash\ \neg c+a=c+b\\
&&AG,\neg c+a=c+b,c+a=c+b\land\neg a=b&\ \vdash\ c+a=c+b\land\neg a=b&&\\
&&AG,\neg c+a=c+b,c+a=c+b\land\neg a=b&\ \vdash\ c+a=c+b&&\\
&&AG,\neg c+a=c+b,c+a=c+b\land\neg a=b&\ \vdash\ \neg(c+a=c+b\land\neg a=b)&&\\
&&AG,c+a=c+b\land\neg a=b&\ \vdash\ \neg(c+a=c+b\land\neg a=b)&&\\
&&AG,\neg(c+a=c+b\land\neg a=b)&\ \vdash\ \neg(c+a=c+b\land\neg a=b)&&\\
&&AG&\ \vdash\ \neg(c+a=c+b\land\neg a=b)&&\\
\end{align*}
Durch Weglassen vieler Zeilen und Benutzung von Abkürzungen wird das fast lesbar.
\begin{align*}
&&AG&\ \vdash\ c+d=d+c&&\\
&&AG,c+d=0&\ \vdash\ d+c=0&&\\
&&c+a=c+b&\ \vdash\ d+(c+a)=d+(c+b)&&\\
&&AG&\ \vdash\ (d+c)+a=d+(c+a)&&\\
&&AG&\ \vdash\ (d+c)+b=d+(c+b)&&\\
&&AG,c+a=c+b&\ \vdash\ (d+c)+a=(d+c)+b&&\\
&&AG,c+d=0,c+a=c+b&\ \vdash\ 0+a=0+b&&\\
&&AG&\ \vdash\ 0+a=a&&\\
&&AG&\ \vdash\ 0+b=b&&\\
&&AG,c+d=0,c+a=c+b&\ \vdash\ a=b&&\\
&&AG&\ \vdash\ \exists y(c+y=0)&&\\
&&AG,c+a=c+b&\ \vdash\ a=b\\
&&AG&\ \vdash\ c+a=c+b\rightarrow a=b&&\\
\end{align*}