Peano-Arithmetik/Beweisprädikat/Eigenschaften/Bemerkung

Das Beweisprädikat ${}\alpha (y)$ besitzt, wenn ${}\Gamma$ die Peano-Arithmetik umfasst, einige ausdruckstarke Eigenschaften, die auch in ${}\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 (${}\Gamma$ sei entscheidbar und enthalte die Peano-Arithmetik).

• Wenn ${}\Gamma \vdash s$, so ist ${}\Gamma \vdash \alpha (GN(s))$ für jeden Ausdruck ${}s\in L^{\rm {Ar}}$.

• Für je zwei Ausdrücke ${}s,t\in L^{\rm {Ar}}$ ist ${}\Gamma \vdash \alpha (GN(s\rightarrow t))\rightarrow (\alpha (GN(s))\rightarrow \alpha (GN(t)))$.

• Für jeden Ausdruck ${}s\in L^{\rm {Ar}}$ ist ${}\Gamma \vdash \alpha (GN(s))\rightarrow \alpha (GN(\alpha (GN(s))))$.