Eine Semantik, die logische Formeln durch Mengen konstruktiver Zeugen oder rechnerischer Objekte (Realizer) interpretiert, die zeigen, wie eine Formel vorgeführt oder berechnet werden kann, und damit Syntax und Ausführbarkeit verbindet.

Prinzip

Jeder Formel eine Klasse konstruktiver Objekte zuordnen, sodass Konjunktionen, Implikationen und Quantoren durch entsprechende kombinatorische oder rechnerische Operationen widergespiegelt werden; eine Formel gilt genau dann als wahr, wenn sie einen Realizer besitzt.

Demonstration

Kleene-Realizability für die Arithmetik: eine natürliche Zahl (oder der Index einer rekursiven Funktion) dient als Zeuge, der die für eine existenzielle Behauptung benötigte Ausgabe berechnet oder Realizer für Voraussetzungen in Realizer für Konklusionen überführt.

Fehlanwendung

Eine klassische nicht-konstruktive Existenzbeweiserklärung als Realizer zu behandeln, ohne einen expliziten Zeugen zu extrahieren, oder Realisierbarkeit mit modelltheoretischer Wahrheit in Kontexten zu verwechseln, in denen Berechenbarkeit relevant ist.

Konsequenz

Richtig angewendet liefert Realisierbarkeit explizite Algorithmen aus Beweisen, konstruktive Konsistenzaussagen und eine Brücke zwischen Beweistheorie und Berechnung, etwa Programmextraktion im Sinne der Curry–Howard-Korrespondenz.

Umkehrung

Statt Zeugen, die Wahrheit konstruieren, betrachtet man Widerlegungen oder Falsifizierer (Gegen-Realizer), die das Scheitern belegen; der Fokus verschiebt sich von konstruktivem Inhalt zu nachweisbarer Unmöglichkeit.

Abgrenzung

Gilt vornehmlich in konstruktiven oder intuitionistischen Kontexten und für Theorien, in denen rechnerischer Inhalt von Bedeutung ist; sie erfasst nicht ohne weiteres klassische, nicht-konstruktive Semantiken oder rein modelltheoretische Wahrheit ohne Anpassung.

Semantische Spannung

Spannung zur modelltheoretischen Wahrheit: Realisierbarkeit betont, wie eine Formel rekonstruiert bzw. berechnet wird, während die klassische Semantik darauf abzielt, ob eine Formel in einer abstrakten Struktur gilt; beide Perspektiven können feine Unterschiede aufweisen.

Synthese

Realisierbarkeit ordnet Formeln rechnerische Zeugen zu, wodurch Beweise ausführbar werden: sie fasst die logischen Operatoren als Operationen auf Realizern zusammen und ermöglicht so die Gewinnung von Algorithmen und eine konstruktive Interpretation formalen Schließens.