Prädikatenlogik: Wie überprüfen Sie selbst die logische Struktur Ihrer eigenen Argumente?

Wahrheitstabellen reichen nicht aus, um die Logik erster Ordnung (mit Quantoren) zu erfassen, daher verwenden wir stattdessen Inferenzregeln. Jede Folgerungsregel wird so gewählt, dass sie solide ist, was bedeutet, dass Sie, wenn Sie mit wahren Aussagen beginnen und die Regel anwenden, nur wahre Aussagen ableiten werden. Wir sagen, dass diese Regeln wahrheitserhaltend sind. Wenn Sie sorgfältig genug auswählen, können Sie es so machen, dass die Regeln nicht nur wahrheitserhaltend sind, sondern es Ihnen auch ermöglichen, jede (wohlgeformte) Aussage abzuleiten, die notwendigerweise (in allen Situationen) wahr ist.

Was Sie wahrscheinlich suchen (nämlich eine praktische Möglichkeit, die logische Gültigkeit Ihrer Argumente streng zu überprüfen), ist die natürliche Deduktion. Es gibt viele verschiedene Stile, der intuitivste Typ ist der Fitch-Stil , der Unterkontexte durch Einrückung oder eine ähnliche visuelle Abgrenzung markiert. Das folgende System verwendet Einrückungen und folgt meiner Meinung nach der Intuition am ehesten.$\def\block#1{\begin{array}{ll}\ &{#1}\end{array}} \def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}} \def\sub#1#2{\text{#1}:\\\block{#2}} \def\imp{\Rightarrow} \def\eq{\Leftrightarrow} \def\nn{\mathbb{N}} \def\none{\varnothing} \def\pow{\mathcal{P}}$

---

Kontexte

Jede Zeile ist entweder eine Überschrift oder eine Anweisung. Wir setzen einen Doppelpunkt nach jeder Überschrift und einen Punkt nach jeder Anweisung. Jeder Header gibt einen Subkontext an (der im aktuellen Kontext enthalten ist), und die Zeilen, die von diesem Header gesteuert werden, werden durch die Einrückung angezeigt. Der vollständige Kontext jeder Zeile wird durch alle Header angegeben, die sie regeln (dh alle nächsten Header darüber auf jeder niedrigeren Einrückungsebene).

Eine verschachtelte Fallanalyse könnte beispielsweise so aussehen:

  $\sub{If $A$}{\sub{If $B$}{...} \\ \sub{If $¬B$}{...}} \\ \sub{If $\neg A$}{...}$

Und über ein willkürliches Mitglied einer Sammlung nachdenken$S$würde aussehen wie:

  $\sub{Given $x{∈}S$}{...}$

Beachten Sie, dass das, was in manchen Zusammenhängen gesagt wird, in anderen Zusammenhängen ungültig sein kann. Sobald Sie das Prinzip hinter Kontexten und Einrückungen verstanden haben, sind die folgenden Regeln sehr natürlich. Beachten Sie auch, dass für die Logik erster Ordnung diese beiden Arten von Kontextheadern (für bedingte Unterkontexte bzw. universelle Unterkontexte) die einzigen Arten sind, die benötigt werden.

Syntaxregeln

Eine Aussage muss eine atomare (unteilbare) Aussage oder eine zusammengesetzte Aussage sein, die auf die übliche Weise unter Verwendung von Booleschen Operationen oder Quantoren gebildet wird, mit der Einschränkung, dass nicht jede Variable, die durch einen Quantor gebunden ist, bereits verwendet wird, um auf ein Objekt im aktuellen Kontext zu verweisen , und dass es keine verschachtelten Quantoren gibt, die dieselbe Variable binden.

Natürliche Abzugsregeln

Jede Folgerungsregel hat die Form:

  $\fitch{\text{X}}{\text{Y}}$

Das heißt, wenn die letzten Zeilen, die Sie geschrieben haben, mit "X" übereinstimmen, können Sie unmittelbar danach auf derselben Einrückungsebene "Y" schreiben. Jede Anwendung einer Inferenzregel ist auch an den aktuellen Kontext gebunden, nämlich den Kontext von "X". Wir werden nicht ständig den „aktuellen Kontext“ erwähnen.

---

Boolesche Operationen

Nehmen Sie irgendwelche Aussagen$A,B,C$(im aktuellen Kontext).

restate : Wenn wir etwas beweisen, können wir es im gleichen Kontext noch einmal bestätigen.

  $\fitch{A.\\ ...}{A.}$

Beachten Sie, dass "$...$" bezeichnen eine beliebige Anzahl von Zeilen, die sich mindestens auf der dargestellten Einrückungsebene befinden. In der obigen Regel bedeutet dies, dass alle seit dem früheren Schreiben von " geschriebenen Zeilen$A.$" muss sich im selben Kontext (oder einem Unterkontext) befinden.

In der Praxis schreiben wir eigentlich nie dieselbe Zeile zweimal. Um anzuzeigen, dass wir eine Zeile in einem Beweis weglassen können, markiere ich sie mit eckigen Klammern wie folgt:

  $\fitch{A. \\ ...}{[A.]}$

⇒sub       ⇒restate     (Wir können einen bedingten Subkontext erstellen, in dem$A$hält.)

  $\fitch{}{\sub{If $A$}{[A.]}}$   $\fitch{B. \\ ... \\ \sub{If $A$}{...}}{\block{[B.]}}$

⇒Einleitung       ⇒elim

  $\fitch{\sub{If $A$}{... \\ B.}}{[A \imp B.]}$   $\fitch{A \imp B. \\ A.}{B.}$

∧Einleitung     ∧elim

  $\fitch{A. \\ B.}{A \land B.}$   $\fitch{A \land B.}{[A.] \\ [B.]}$

∨Einleitung     ∨elim

  $\fitch{A.}{[A \lor B.] \\ [B \lor A.]}$   $\fitch{A \lor B. \\ A \imp C. \\ B \imp C.}{C.}$

¬intro     ¬elim     ¬¬elim

  $\fitch{A \imp \bot.}{\neg A.}$   $\fitch{A. \\ \neg A.}{\bot.}$   $\fitch{\neg \neg A.}{A.}$

Beachten Sie, dass wir durch die Verwendung von ¬intro und ¬¬elim die folgende zusätzliche Inferenzregel erhalten können:

  $\fitch{\neg A \imp \bot.}{A.}$

was dem entspricht, wie man zu beweisen versuchen würde$A$ durch Widerspruch , nämlich um zu zeigen, dass vorausgesetzt$\neg A$impliziert eine Unwahrheit.

⇔Einleitung     ⇔elim

  $\fitch{A \imp B. \\ B \imp A.}{A \eq B.}$   $\fitch{A \eq B.}{[A \imp B.] \\ [B \imp A.]}$

Quantoren und Gleichheit

Die Regeln hier gelten für eingeschränkte Quantifizierer, weil wir normalerweise in Bezug auf sie denken. Zuerst brauchen wir einige Definitionen.

Benutzte Variable : Eine Variable, die im Header eines enthaltenden ∀-Kontexts oder in einem vorangegangenen ∃-Eliminierungsschritt ("let") in einem enthaltenden Kontext deklariert ist.

Nicht verwendete Variable : Eine Variable, die nicht verwendet wird.

Frische Variable : Eine Variable, die in keiner vorherigen Anweisung in irgendeinem enthaltenden Kontext erscheint.

Objektausdruck : Ein Ausdruck, der sich auf ein Objekt bezieht (z. B. eine verwendete Variable oder ein Funktionssymbol, das auf Objektausdrücke angewendet wird).

Eigentum mit$k$Parameter : Eine Zeichenfolge$P$mit einigen Leerzeichen, wobei jedes Leerzeichen ein Etikett von hat$1$Zu$k$, sodass jedes Leerzeichen in ersetzt wird$P$durch einen Objektausdruck ergibt eine Aussage. Wenn$k = 2$, Dann$P(E,F)$ist das Ergebnis des Ersetzens jedes beschrifteten Leerzeichens$1$von$E$und Ersetzen jedes markierten Leerzeichens$2$von$F$. Ähnlich für andere$k$.

In diesem Abschnitt,$E,F$(falls beteiligt) können beliebige Objektausdrücke (im aktuellen Kontext) sein.

Wir beginnen mit den folgenden Regeln, die einen Typ aller Objekte liefern.

Universum :$obj$ist ein Typ.

  $\fitch{}{[E{∈}obj.]}$

Nehmen Sie jetzt einen beliebigen Typ$S$und eine 1-Parameter-Eigenschaft$P$und eine unbenutzte Variable$x$das taucht nicht auf$S$oder$P$.

∀sub           ∀restate         (Wir können einen ∀-Subkontext erzeugen, in dem$x$ist vom Typ$S$.)

  $\fitch{}{\sub{Given $x{∈}S$}{[x{∈}S.]}}$   $\fitch{A. \\ ... \\ \sub{Given $x{∈}S$}{...}}{\block{[A.]}}$($x$darf nicht vorkommen$A$)

∀Einführung           ∀elim

  $\fitch{\sub{Given $x{∈}S$}{... \\ P(x).}}{\forall x{∈}S\ ( \ P(x) \ ).}$   $\fitch{\forall x{∈}S\ ( \ P(x) \ ). \\ E{∈}S.}{P(E).}$($E$darf keine ungenutzten Variablen mit teilen$P$)

∃Einleitung           ∃elim

  $\fitch{E{∈}S. \\ P(E).}{\exists x{∈}S\ ( \ P(x) \ ).}$   $\fitch{\exists x{∈}S\ ( \ P(x) \ ).}{\text{Let $y{∈}S$ such that $P(y)$}. \\ [y{∈}S.] \\ [P(y).]}$(Wo$y$ist eine frische Variable)

=Einführung       =elimin

  $\fitch{}{[E=E.]}$   $\fitch{E=F. \\ P(E).}{P(F).}$($F$darf keine ungenutzte Variable mit teilen$P$)

Umbenennen von Variablen

Schließlich sind die folgenden Regeln zur Variablenumbenennung redundant, würden aber Beweise verkürzen.

∀umbenennen         ∃umbenennen

  $\fitch{\forall x{∈}S\ ( \ P(x) \ ).}{[\forall y{∈}S\ ( \ P(y) \ ).]}$   $\fitch{\exists x{∈}S\ ( \ P(x) \ ).}{[\exists y{∈}S\ ( \ P(y) \ ).]}$

  (Wo$y$ist eine unbenutzte Variable, die nicht in erscheint$P$)

Kurz Formen

Der Einfachheit halber schreiben wir "$\forall x,y{∈}S\ ( \ P(x,y) \ )$„als Kurzform für“$\forall x{∈}S\ ( \ \forall y{∈}S\ ( \ P(x,y) \ ) \ )$", und ähnlich für weitere Variablen und für "$\exists$". Wir werden auch verschachtelte ∀-Unterkontext-Header in der folgenden Form komprimieren:

  $\sub{Given $x{∈}S$}{\sub{Given $y{∈}S$}{...}}$

Zu:

  $\sub{Given $x,y{∈}S$}{...}$

Zusätzlich, "$\exists! x{∈}S\ ( \ P(x) \ )$" ist eine Kurzform für "$\exists x{∈}S\ ( \ P(x) \land \forall y{∈}S\ ( \ P(y) \imp x=y \ ) \ )$".

---

Beispiel

Hier ist ein Beispiel, wo$S,T$sind alle Arten und$P$ist eine beliebige Eigenschaft mit zwei Parametern.

Zuerst mit allen angezeigten Zeilen:

  Wenn$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$: [⇒sub]
    $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$. [⇒sub]
    Let$a{∈}S$so dass$\forall y{∈}T\ ( \ P(a,y) \ )$. [∃elim]
    $a{∈}S$. [∃elim]
    $\forall y{∈}T\ ( \ P(a,y) \ )$. [∃elim]
    $\forall z{∈}T\ ( \ P(a,z) \ )$. [∀umbenennen]
    Gegeben$y{∈}T$: [∀sub]
      $y{∈}T$. [∀sub]
      $\forall z{∈}T\ ( \ P(a,z) \ )$. [∀wiederholen]
      $y{∈}T$. [wiederholen]
      $P(a,y)$. [∀elim]
      $a{∈}S$. [∀wiederholen]
      $\exists x{∈}S\ ( \ P(x,y) \ )$. [∃Einführung]
    $\forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [∀Einleitung]
  $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ ) \imp \forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [⇒Einleitung]

Schließlich mit allen Zeilen in eckigen Klammern entfernt:

  Wenn$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$: [⇒sub]
    Let$a{∈}S$so dass$\forall y{∈}T\ ( \ P(a,y) \ )$. [∃elim]
    Gegeben$y{∈}T$: [∀sub]
      $P(a,y)$. [∀elim]
      $\exists x{∈}S\ ( \ P(x,y) \ )$. [∃Einführung]
    $\forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [∀Einleitung]
  $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ ) \imp \forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [⇒Einleitung]

Dieser endgültige Beweis ist sauber und dennoch leicht computerüberprüfbar.

Definitive Erweiterung

Um Definitionen zu erleichtern , die Beweise erheblich verkürzen können, haben wir auch die folgenden definitorialen Erweiterungsregeln.

Für jede$k$-parameter-Eigenschaft$P$und frisches Prädikatsymbol$Q$:

  $\fitch{}{\text{Let $Q(x_1,...x_k) ≡ P(x_1,...x_k)$ for each $x_1{∈}S_1$ and ... and $x_k{∈}S_k$.} \\ [∀x_1{∈}S_1\ \cdots ∀x_k{∈}S_k\ ( \ Q(x_1,...x_k) ⇔ P(x_1,...x_k) \ ).]}$

Für jede$(k+1)$-parameter-Eigenschaft$R$und frisches Funktionssymbol$f$:

  $\fitch{∀x_1{∈}S_1 \cdots ∀x_k{∈}S_k\ ∃!y{∈}T ( \ R(x_1,...x_k,y) \ ) } {\text{Let $f : S_1{×}{\cdots}{×}S_k{→}T$ such that $R(x_1,...x_k,f(x_1,...x_k))$ for each $x_1{∈}S_1$ and ... and $x_k{∈}S_k$.} \\ [∀x_1{∈}S_1\ \cdots ∀x_k{∈}S_k\ ( \ f(x_1,...x_k)∈T ∧ R(x_1,...x_k,f(x_1,...x_k)) \ ).]}$

Diese Regeln sind insofern überflüssig, als dass jede beweisbare Aussage, die keines der neuen Symbole verwendet, bewiesen werden kann, ohne die definitorische Erweiterung zu verwenden.

Anmerkungen

Die obigen Regeln vermeiden die üblichen Schwierigkeiten, die viele andere Systeme haben, wo Variablen, die für Zeugen existentieller Aussagen verwendet werden, von Variablen unterschieden werden müssen, die für beliebige Objekte verwendet werden. Der Grund ist, dass hier jede Variable entweder durch einen ∀-Unterkontext oder durch eine „let“-Anweisung spezifiziert wird; dh es gibt keine freien Variablen. Die Tatsache, dass jede Variable gebunden ist, hängt stark damit zusammen, dass dieses System ein leeres Universum zulässt, wenn es keine anderen Axiome gibt.

Außerdem wird jede Variable durch einen eindeutigen Header oder eine "let"-Anweisung im aktuellen Kontext angegeben; mit anderen Worten, es gibt keine variable Abschattung. Dies ist so beabsichtigt, und in der tatsächlichen mathematischen Praxis halten wir uns auch daran, obwohl die meisten anderen formalen Systeme dies nicht tun. Als Konsequenz werden Sätze wie „$\exists x\ \forall x\ ( x=x )$." kann in diesem System einfach nicht geschrieben werden. Wenn Sie solche schrecklichen Sätze zulassen möchten, müssten Sie die Regeln entsprechend ändern, aber es wird höchstwahrscheinlich Kopfschmerzen verursachen.

Schließlich gab es einige subtile technische Entscheidungen. Für die Quantifiziererregeln, der Grund, warum ich das verlangt habe$x$taucht nicht auf$S,P$ist, dass wir, wenn wir später Regeln zum Spezifizieren von Typen hinzufügen, normalerweise Variablennamen in seiner Syntax haben würden, was Probleme verursachen würde. Wenn wir zum Beispiel im aktuellen Kontext geschrieben haben "$x∈\{y:y∈S∧y∈T\}$" Und "$x∈U$"Es wird nicht sinnvoll sein, das Schreiben zuzulassen"$∃y∈U\ ( y∈\{y:y∈S∧y∈T\} )$". Ebenso, wenn wir geschrieben haben "$x=\{y:P(y)\}$" Und "$∃y∈U\ ( Q(x,y) )$"Wir wollen das Schreiben nicht zulassen"$∃y∈U\ ( Q(\{y:P(y)\},y) )$".

Damit eine Variable nach dem Verlassen des Subkontexts, in dem sie deklariert wurde, wieder frisch wird, habe ich gefordert, dass die ⇒intro- und ∀intro-Regeln nur unmittelbar nach dem entsprechenden ⇒-Subkontext oder ∀-Subkontext angewendet werden können. Es wäre einfacher, eine neue Variable einfach als eine zu definieren, die in keiner vorherigen Zeile vorkommt, aber dann können uns in einem langen Beweis leicht die frischen Variablennamen ausgehen.

~ ~ ~ ~ ~ ~ ~

Um die Flexibilität dieses Systems zu veranschaulichen, werde ich sowohl die Peano-Arithmetik als auch die Mengenlehre als zusätzliche Regeln ausdrücken, die dem System einfach hinzugefügt werden können.

Peano-Arithmetik

Fügen Sie den Typ hinzu$\nn$und die Symbole von PA, nämlich die Konstantensymbole$0,1$und das$2$-Funktionssymbole eingeben$+,·$und das$2$-Eingabe Prädikat-Symbol$<$.

Fügen Sie die Axiome von PA hinzu$^-$, angepasst von hier :

• $\forall x,y{∈}\nn\ ( \ x+y ∈ \nn \ )$.
• $\forall x,y{∈}\nn\ ( \ x·y ∈ \nn \ )$.
• $\forall x,y{∈}\nn\ ( \ x+y=y+x \ )$.
• $\forall x,y{∈}\nn\ ( \ x·y=y·x \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x+(y+z)=(x+y)+z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x·(y·z)=(x·y)·z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x·(y+z)=x·y+x·z \ )$.
• $\forall x{∈}\nn\ ( \ x+0=x \ )$.
• $\forall x{∈}\nn\ ( \ x·1=x \ )$.
• $\forall x{∈}\nn\ ( \ \neg x<x \ )$.
• $\forall x,y{∈}\nn\ ( \ x<y \lor y<x \lor x=y \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \land y<z \imp x<z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \imp x+z<y+z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \land 0<z \imp x·z<y·z \ )$.
• $\forall x,y{∈}\nn\ ( \ x<y \imp \exists z{∈}\nn\ ( \ x+z=y \ ) \ )$.
• $0<1$.
• $\forall x{∈}\nn\ ( \ 0=x \lor 1=x \lor 1<x \ )$.

Fügen Sie die Induktionsaxiome hinzu, und zwar für jede Eigenschaft$P$mit nur den Symbolen von PA und Quantoren über$\nn$füge das folgende Axiom hinzu (wobei$k$taucht nicht auf$P$):

• $P(0) \land \forall k{∈}\nn\ ( \ P(k) \imp P(k+1) \ ) \imp \forall k{∈}\nn\ ( \ P(k) \ )$.

Mengenlehre

Fügen Sie den Typ hinzu$set$und die Regel, dass jedes Mitglied von$set$ist auch ein typ.

Fügen Sie die unären Funktionssymbole hinzu$\pow,\bigcup$, die binären Funktionssymbole$×,→$, und das Konstantensymbol$\none$. Wir verwenden das binäre Prädikat-Symbol wieder$\in$, da es keine Zweideutigkeit geben wird. Fügen Sie auch die folgenden Regeln (in jedem Kontext) für die andere Notation hinzu:

• Wenn$E,F \in obj$, Dann$(E,F) \in obj$Und$\{E,F\} \in set$.
• Wenn$S,T \in set$, Dann$S×T \in set$Und$(S{→}T) \in set$Und$\pow(S) \in set$.
• Wenn$S,T \in set$Und$f \in (S{→}T)$Und$x \in S$, Dann$f(x) \in T$.
• Wenn$S \in set$Und$\forall x{∈}S\ ( \ x \in set \ )$, Dann$\bigcup(S) \in set$.

Fügen Sie die folgenden Axiome hinzu:

• Extensionalität :   $\forall S,T{∈}set\ ( \ S=T \eq \forall x{∈}obj\ ( \ x \in S \eq x \in T \ ) \ ).$
• leerer Satz :   $\forall x{∈}obj\ ( \ \neg x \in \none \ ).$
• Natur :   $\nn{∈}set$.
• power-set :   $\forall S{∈}set\ ( \ \pow(S) = \{ T : T \in set \land \forall x{∈}T\ ( \ x \in S \ ) \} ).$
• Paar :   $\forall x,y{∈}obj\ ( \ \{x,y\} = \{ z : z=x \lor z=y \} ).$
• bestelltes Paar :   $\forall x,y{∈}obj\ \forall z,w{∈}obj\ ( \ (x,y)=(z,w) \eq x=z \land y=w \ ).$
• Produkttyp :   $\forall S,T{∈}set\ ( \ S×T = \{ t : \exists x{∈}S\ \exists y{∈}T\ ( \ t=(x,y) \ ) \} \ ).$
• Funktionstyp :   $\forall S,T{∈}set\ ( \ (S→T) = \\ \{ F : F \in \pow(S×T) \land \forall x{∈}S\ \exists! y{∈}T\ ( \ (x,y) \in F \ ) \} \ ).$
• Funktionsanwendung :   $\forall S,T{∈}set\ \forall f{∈}(S{→}T)\ \forall x{∈}S\ ( \ (x,f(x)) \in f \ ).$
• Vereinigung :   $\forall S{∈}set\ ( \ \bigcup(S) = \{ x : \exists T{∈}set\ ( \ x \in T \land T \in S \ ) \} \ ).$
• Wahl :   $\forall S,T{∈}set\ \forall R{∈}\pow(S×T)\ ( \ \forall x{∈}S\ \exists y{∈}T\ ( \ (x,y) \in R \ ) \\ \imp \exists f{∈}(S{→}T)\ \forall x{∈}S\ ( \ (x,f(x)) \in R \ ) \ ).$

Fügen Sie die folgenden Regeln hinzu:

Typ-Notation

Nehmen Sie (im aktuellen Kontext) eine beliebige Eigenschaft$P$und Objektausdruck$E$und unbenutzte Variable$x$.

Dann$\{ x : P(x) \}$ist ein Typ und seine Mitgliedschaft wird geregelt durch:

  $\fitch{}{E \in \{ x : P(x) \} \eq P(E).}$. ($x$darf nicht vorkommen$E$oder$P$)

Verständnis

Nimm irgendein Eigentum$P$und unbenutzte Variable$x$.

  $\fitch{S \in set.}{\{ x : x \in S \land P(x) \} \in set.}$. ($x$darf nicht vorkommen$S$oder$P$)

Ersatz

Such dir irgendeine aus$2$-parameter-Eigenschaft$P$und ungenutzte Variablen$x,y$.

  $\fitch{S \in set. \\ \forall x{∈}S\ \exists! y{∈}obj\ ( \ P(x,y) \ ).}{\{ y : \exists x{∈}S\ ( \ P(x,y) \ ) \} \in set.}$($x,y$darf nicht vorkommen$S$oder$P$)

Induktion

Nimm irgendein Eigentum$P$mit$1$Parameter ab$\nn$.

  $\fitch{P(0). \\ \forall k{∈}\nn\ ( \ P(k) \imp P(k+1) \ ).}{\forall k{∈}\nn\ ( \ P(k) \ ).}$($k$darf nicht vorkommen$P$)

Die Induktionsregel fasst die Induktionsaxiome für PA zusammen, und im Wesentlichen besteht der einzige Unterschied darin, dass die Eigenschaft$P$kann Mengenoperationen und Quantifizierung über Mengen umfassen.

Funktionsnotation

Diese Regel ist theoretisch unnötig, aber pragmatisch sehr praktisch (in der Informatik auch als Lambda-Ausdrücke bekannt).

Nimm irgendein Set$S$und jeder Objektausdruck$E$mit$1$Parameter ab$S$, und unbenutzte Variable$x$.

Dann$( S\ x \mapsto E(x) )$ist ein Objekt und sein Verhalten wird bestimmt durch:

  $\fitch{\forall x{∈}S\ ( \ E(x) \in T \ ). \\ f = ( S\ x \mapsto E(x) ).}{f \in (S→T) \land \forall x{∈}S ( \ f(x) = E(x) \ ).}$

Grundlegendes System

Die Kombination der obigen Peano-Arithmetik plus der Mengenlehre ergibt ein grundlegendes System, das im Wesentlichen so stark wie ZFC, aber viel benutzerfreundlicher ist. Es ist auch agnostisch gegenüber der Existenz von Objekten, die keine Mengen sind, und geht nicht einmal davon aus, dass die Mitglieder von$\nn$sind Sätze. Es behandelt auch kartesische Produkte und geordnete Paare als eingebaute abstrakte Begriffe. So verwenden wir sie in der eigentlichen Mathematik. (Genauer gesagt interpretiert das obige System ZFC minus Regularität direkt.)