Zwei Formeln bilden ein Beweispaar, wenn eine aus der anderen folgt; anders: Zwei natuerliche Zahlen m und n bilden ein PA-Beweispaar, gdw. m die Goedelnummer einer Ableitung ist, deren unterste Zeile die Kette mit der Goedelnummer n ist.
``Beweispaar'' ist ein 2-stelliges Praedikat.
Es existiert ein Algorithmus, um diese Eigenschaft zu entscheiden. Dazu geht man die Zeilen der Ableitung Zeile fuer Zeile nach unten, markiert die Axiome, und schaut, wenn eine Zeile kein Axiom ist, ob sie aufgrund einer gueltigen Schlussregel folgt, und wenn alle Nicht-Axiome aufgrund von Schlussregeln aus Axiomen folgen ist die Ableitung gueltig, sonst nicht.
Der Algorithmus ist primitiv rekursiv, d.h. er terminiert nach endlich vielen Schritten. Alle primitiv rekursiven Praedikate sind in PA repraesentierbar (kein Beweis dafuer), z.B. istPrim(x), Teiler(x,y), usw.
Praedikat Beweispaar(x, x'), wie repraesentiert bleibt offen (zu lang).
Koennten jetzt auch ausdruecken
(0=0 in Notation
uebersetzen, z.B. 666,111,666), d.h. es gibt eine Zahl a, die mit 0=0 ein Beweispaar
bildet, d.h. 0=0 ist ein Satz von PA.
sagt
aus, x' ist eine Satzzahl. Dies ist nicht primitiv rekursiv (wir muessten u.U.
unendlich lange suchen).