Sequenzenkalkül (Prädikatenlogik)

Erweiterung des aussagenlogischen Kalküls um Regeln für Quantoren und Gleichheit. Wichtig sind die Einschränkungen bei der Einführung von Konstanten.

Quantorenregeln:

• Allquantor rechts $(\Rightarrow \mathrm{\forall })$: $\frac{\mathrm{\Phi }\Rightarrow \mathrm{\Delta },\psi (c)}{\mathrm{\Phi }\Rightarrow \mathrm{\Delta },\mathrm{\forall }x\psi (x)}$, wobei $c$ eine neue Konstante ist (kommt nicht in $\mathrm{\Phi },\mathrm{\Delta },\psi$ vor).
• Existenzquantor links $(\mathrm{\exists }\Rightarrow )$: $\frac{\mathrm{\Phi },\psi (c)\Rightarrow \mathrm{\Delta }}{\mathrm{\Phi },\mathrm{\exists }x\psi (x)\Rightarrow \mathrm{\Delta }}$, wobei $c$ eine neue Konstante ist (Eigenvariablenbedingung).
• Allquantor links $(\mathrm{\forall }\Rightarrow )$: $\frac{\mathrm{\Phi },\psi (t)\Rightarrow \mathrm{\Delta }}{\mathrm{\Phi },\mathrm{\forall }x\psi (x)\Rightarrow \mathrm{\Delta }}$ für einen beliebigen Term $t$.
• Existenzquantor rechts $(\Rightarrow \mathrm{\exists })$: $\frac{\mathrm{\Phi }\Rightarrow \mathrm{\Delta },\psi (t)}{\mathrm{\Phi }\Rightarrow \mathrm{\Delta },\mathrm{\exists }x\psi (x)}$ für einen beliebigen Term $t$.

Gleichheitsregeln:

• $(=\Rightarrow )$: $\frac{\mathrm{\Phi },t=t\Rightarrow \mathrm{\Delta }}{\mathrm{\Phi }\Rightarrow \mathrm{\Delta }}$ (Reflexivität entfernen).
• Substitutionsregeln $(S\Rightarrow )$ und $(\Rightarrow S)$, die das Ersetzen gleicher Terme erlauben (Leibniz-Prinzip).