formales System zur Beschreibung der Prädikatenlogik (siehe auch elementare Sprache, logischer Kalkül), gelegentlich auch als Synonym für „Prädikatenlogik“ gebraucht.

Zum Aufbau von logischen Ausdrücken im Prädikatenkalkül (PK) können folgende Grundzeichen (Alphabet) benutzt werden:

1. Individuenvariablen : x₁, x₂, x₃,…,
2. Prädikatenvariablen : \({P}_{n}^{m},\), wobei n als Unterscheidungsindex dient und m die Stellenzahl der Prädikatenvariablen angibt (m, n = 1, 2, 3,… ),
3. Funktionenvariablen : \({F}_{n}^{m},\), wobei n wieder Unterscheidungsindex ist, und m die Stellenzahl der Funktionsvariablen bezeichnet (Funktionsvariablen müssen im PK nicht notwendig auftreten),
4. Aussagenlogische Funktoren : ¬, ∧, ∨, →, ↔ (siehe auch Aussagenkalkül),
5. Quantoren : ∃, ∀ (Existenzquantor, Allquantor),
6. das Gleichheitsszeichen : = (das Gleichheitszeichen muß im PK nicht vorkommen; man spricht dann vom Prädikatenkalkül ohne Gleichheit),
7. technische Zeichen : (, ) – die geeignet sind, das Zusammenfassen gewisser Teilausdrücke anzuzeigen.

Durch das Aneinanderreihen von jeweils endlich vielen Grundzeichen entstehen Zeichenreihen, aus denen induktiv die „sinnvollen“, nämlich Terme und Ausdrücke ausgesondert werden.

Terme:

1. Alle Individuenvariablen sind Terme.
2. Sind t₁,…, t_m Terme, dann ist (für jedes n) die Zeichenreihe \({F}_{n}^{m}({t}_{1},\ldots,{t}_{m})\) ein Term.
3. Keine weiteren Zeichenreihen sind Terme.

Ausdrücke:

• Sind t₁,…, t_m Terme, dann sind die Zeichenreihen \({P}_{n}^{m}({t}_{1},\ldots,{t}_{m})\) und t₁ = t₂ ( falls „=“ im PK auftritt) die einfachsten Ausdrücke, die prädikative oder atomare Ausdrücke genannt werden.
• Sind φ und ψ Ausdrücke, dann sind auch ^•¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) Ausdrücke.
• Ist x eine Individuenvariable und φ ein Ausdruck, in dem die Zeichenreihen ∃x oder ∀x nicht vorkommen, dann sind auch ∃x φ und ∀ x φ Ausdrücke.
• Keine weiteren Zeichenreihen sind Ausdrücke.

Zur inhaltlichen Interpretation eines solchen Kalküls wird der Begriff der Gültigkeit eines Ausdrucks in einem Individuenbereich benötigt. Dazu sei M eine nichtleere Menge (Individuenbe-reich) und B eine Abbildung, die jeder Variablen des PK ein entsprechendes Objekt über M wie folgt zuordnet: \begin{eqnarray}\begin{array}{l}B({x}_{i})\ \ :={a}_{i}\ \text{ist ein Element aus}\ M\text{.}\\ B({P}_{n}^{m})\ :={R}_{n}^{m}\ \text{ist eine}\ m\text{-stellige Relation, und}\\ B({F}_{n}^{m})\ :={f}_{n}^{m}\ \text{eine}\ m\text{-stellige Funktion}\,\mathrm{\ddot{u}}\text{ber}\ M.\end{array}\end{eqnarray}B heißt Interpretation oder Belegung der Variablen in M. B wird zu einer Abbildung B* erweitert, die jedem Term und jedem Ausdruck einen Wert zuordnet. Werte von Termen sind Elemente aus M, und Werte von Ausdrücken sind 1 (:= wahr) bzw. 0 (:= falsch). Das sind die Wahrheitswerte der klassischen zweiwertigen Logik; für mehrwertige Logiken kommen noch weitere Wahrheitswerte hinzu. Die Wertdefinition erfolgt wiederum induktiv über dem Aufbau der Terme bzw. der Ausdrücke.

Hat der Term t die Form \({F}_{n}^{m}({x}_{1},\ldots,{x}_{m})\), so ist \(B^* (t):={f}_{n}^{m}(B({x}_{1}),\ldots,B({x}_{m})).\)

Sind t₁,…, t_m Terme, und ist t ebenfalls ein Term der Gestalt \({F}_{n}^{m}({t}_{1},\ldots,{t}_{m})\), dann ist \(B^* (t):={f}_{n}^{m}(B({t}_{1}),\ldots,B({t}_{m})).\)

Ist nun φ ein prädikativer Ausdruck der Gestalt \({P}_{n}^{m}({t}_{1},\ldots,{t}_{m})\), dann ist \begin{eqnarray}B^* (\phi ):=\{\begin{array}{ll}1, & \text{falls}\ {R}_{n}^{m}(B^* ({t}_{1}),\ldots,B^* ({t}_{m}))\text{glit,}\\ 0, & \text{sonst}\text{.}\end{array}\end{eqnarray}

Diese Definition gilt sinngemäß auch für prädikative Ausdrücke der Gestalt t₁ = t₂, wenn in PK das Gleichheitszeichen vorkommt.

Sind φ und ψ Ausdrücke, dann gilt: \begin{eqnarray}\begin{array}{l}B^* (\neg \varphi ):=1-B^* (\neg \varphi ),\\ B^* (\varphi \wedge \psi ):=\min \{B^* (\varphi ),B^* (\psi )\},\\ B^* (\varphi \vee \psi ):=\max \{B^* (\varphi ),B^* (\psi )\},\\ B^* (\varphi \to \psi ):=\max \{1-B^* (\varphi ),B^* (\psi )\},\\ B^* (\varphi \leftrightarrow \psi ):=\left\{\begin{array}{ll}1, & \text{falls}\ B^* (\varphi ),B^* (\psi ),\\ 0, & \text{sonst}\text{.}\end{array}\right.\\ B^* (\exists x\ \varphi ):=\max \{B^{\prime*} (\varphi ):{B}^{^{\prime} }\mathop{=}\limits_{x}B\},\ \text{wobei}\ {B}^{^{\prime} }\mathop{=}\limits_{x}B\end{array}\end{eqnarray} bedeutet, daß B^′ eine beliebige Belegung in M ist, die sich von B höchstens in dem x zugeordneten Element unterscheidet. \begin{eqnarray}B^* (\forall x\ \varphi ):=\min\{{B^{\prime*} (\varphi ):B^{\prime*}}\mathop{=}\limits_{x}B\}.\end{eqnarray}

Die Belegung B erfüllt den Ausdruck φ in M, wenn B*(φ) = 1 ist. Ein Ausdruck heißt gültig in M, wenn φ durch jede Belegung in M erfüllt wird. Die in jedem nichtleeren Individuenbereich gültigen Ausdrücke heißen allgemeingültig oder logisch gültig. Die Menge ag der allgemeingültigen Ausdrücke ist nicht entscheidbar, d. h., es gibt keinen Algorithmus, der die Allgemeingültigkeit eines beliebigen Ausdrucks überprüft.

Andererseits läßt sich die Menge ag aus einer „überschaubaren“ (rekursiven) Menge Ax von logischen Axiomen mittels formaler Ableitungsregeln erzeugen. Ein Anliegen der Prädikatenlogik war es, ein möglichst einsichtiges System Ax mit wenigen „einfachen“ Ableitungsregeln zu schaffen, welches in dem Sinne vollständig ist, daß jeder allgemeingültige Ausdruck (und nur solche) aus Ax herleitbar ist (Gödelscher Vollständigkeitssatz, Beweismethoden).

Ein vollständiges prädikatenlogisches Axiomen-system Ax, das mit den beiden Beweisregeln modus ponens und Generalisierung auskommt, ist durch die folgenden Axiome Ax₁–Ax₁₂ gegeben: \begin{eqnarray}\begin{array}{l}{\text{AX}}_{1} & \varphi \to (\psi \to \varphi ).\\ {\text{AX}}_{2} & [\varphi \to (\psi \to \chi )]\to [(\varphi \to \psi )\to (\varphi \to \chi )].\\ {\text{AX}}_{3} & (\neg \psi \to \neg \varphi )\to (\varphi \to \psi ).\\ {\text{AX}}_{4} & \text{a})\ \ \varphi \wedge \psi \to \varphi,\ \ \ \text{b})\ \ \varphi \wedge \psi \to \psi .\\ {\text{AX}}_{5} & (\chi\to \varphi )\to [(\chi\to \psi )\to (\chi\to (\varphi \wedge \psi ))].\\ {\text{AX}}_{6} & \text{a})\ \ \varphi \to (\varphi \vee \psi),\ \ \ \text{b})\ \ \psi \to \to (\varphi \vee \psi ).\\ {\text{AX}}_{7} & (\varphi \to \chi )\to [(\psi \to \chi )\to [(\varphi \vee \psi )\to \chi]].\end{array}\end{eqnarray}

Offensichtlich sind Ax₁–Ax₇ schon aufgrund ihrer logischen Struktur allgemeingültig; dieses System erweist sich zusammen mit dem modus ponens als vollständiges System für die Aussagenlogik. Für die Prädikatenlogik kommen weitere Axiome über Quantoren hinzu:

Falls das Gleichheitszeichen im PK nicht auftritt, ist das durch Ax₁–Ax₁₀ gegebene System vollständig, anderenfalls kommen noch die folgenden Axiome der Gleichheit hinzu, um ein vollständiges System Ax zu erhalten.

Als wichtiges Hilfsmittel bei prädikatenlogischen Untersuchungen erweist sich der Endlichkeitssatz in seinen verschiedenen Formen (Endlichkeitssatz, Kompaktheitssatz der Modelltheorie).

Läßt man nicht nur die Quantifizierung von Individuenvariablen, sondern auch die der Prädikatenund Funktionenvariablen zu (prinzipiell kommt man in der Prädikatenlogik mit Gleichheit immer ohne Funktionenvariablen aus, da Funktionen mit Hilfe von Relationen definierbar sind), so gelangt man zum Prädikatenkalkül der zweiten Stufe, für den eine „überschaubare“ vollständige Axiomatisierung nicht mehr existiert. Synonym hierfür wird auch der Begriff „Prädikatenlogik der zweiten Stufe“ benutzt.

Werden zu den Grundzeichen des PK noch Variablen für Mengen von Relationen bzw. Relationen von Relationen usw. hinzugenommen, und läßt man die Quantifizierung dieser neuen Variablen ebenfalls zu, dann entstehen Prädikatenkalküle höherer Stufe oder synonym Prädikatenlogiken höherer Stufe. Für sie gelten jedoch alle „schönen“ Eigenschaften der Prädikatenlogik erster Stufe (wo nur Individuenvariablen quantifiziert werden dürfen) nicht mehr, insbesondere gelten der Gödelsche Vollständigkeitssatz und der Endlichkeitssatz nicht.