Peano-Arithmetik/Beweisprädikat/Eigenschaften/Bemerkung

Das Beweisprädikat $\alpha (y)$ besitzt, wenn $\mathrm{\Gamma }$ die Peano-Arithmetik umfasst, einige ausdruckstarke Eigenschaften, die auch in $\mathrm{\Gamma }$ ableitbar sind. Der Beweis von diesen Eigenschaften ist aufwändig, da sie nicht abstrakt aus der Repräsentierbarkeit folgen, sondern im Beweiskalkül erarbeitet werden müssen. Wichtige Eigenschaften sind ($\mathrm{\Gamma }$ sei entscheidbar und enthalte die Peano-Arithmetik).

• Wenn $\mathrm{\Gamma }⊢s$, so ist $\Gamma ⊢\alpha (GN(s))$ für jeden Ausdruck $s\in L^{\mathrm{A}\mathrm{r}}$.
• Für je zwei Ausdrücke $s,t\in L^{\mathrm{A}\mathrm{r}}$ ist $\Gamma ⊢\alpha (GN(s\to t))\to (\alpha (GN(s))\to \alpha (GN(t)))$.
• Für jeden Ausdruck $s\in L^{\mathrm{A}\mathrm{r}}$ ist $\mathrm{\Gamma }⊢\alpha (GN(s))\to \alpha (GN(\alpha (GN(s))))$.