Ein Ansatz, der logischen Junktoren und Formeln Bedeutung durch ihre Rolle in Inferenzen — Einführungs- und Eliminationsregeln — zuschreibt, statt durch modelltheoretische Wahrheitsbedingungen.

Prinzip

Bedeutung wird durch kanonische Inferenzmuster bestimmt: Junktoren werden durch die inferenziellen Schritte charakterisiert, die sie in Beweisen einführen und eliminieren; Beweisumformungen stehen im Zentrum der Semantik.

Demonstration

In der natürlichen Deduktion erhält die Konjunktion ihre Bedeutung durch die Einführungsregel (aus A und B folgere A∧B) und durch die Eliminationsregeln (aus A∧B folgere A oder B); zusammen bestimmen diese Regeln funktional das semantische Verhalten des Junktors in Beweiskontexten.

Fehlanwendung

Beliebige Beweissysteme als semantisch interpretierend zu betrachten, ohne Harmonie oder Normalisierung sicherzustellen, kann zu inkonsistenten Bedeutungen führen; syntaktische Inferenzregeln als Bedeutung zu nehmen, ohne ihre Stabilität unter Beweisumformungen zu prüfen, ist fehlerhaft.

Konsequenz

Junktoren und Formeln erhalten Bedeutungen, die an inferenziellen Gebrauch gebunden sind; dies verbindet Beweistheorie und Semantik eng, stützt normative Auffassungen von Assertion und Schluss sowie konstruktive Interpretationen logischer Konstanten.

Umkehrung

Die modelltheoretische Semantik kehrt den Fokus um, indem sie Bedeutung über Wahrheitsbedingungen in Strukturen definiert und dann Beweisregeln daraus ableitet, statt von inferenziellen Rollen auszugehen.

Abgrenzung

Gilt vornehmlich für Systeme, deren Beweisregeln wohlverhalten sind (kanonisch, harmonisch und normalisierungsfähig); sie stößt an Grenzen bei rein extensionale, modellbasierten Eigenschaften oder bei Logiken ohne geeignete Beweissysteme.

Semantische Spannung

Spannung zwischen inferenzieller (gebrauchsbasierter) und modelltheoretischer (wahrheitsbasierter) Bedeutung: Manche Phänomene werden natürlich durch Beweise erfasst (konstruktiver Gehalt), andere verlangen extensional Modelle (Wahrheitsbedingungen über Strukturen).

Synthese

Die beweistheoretische Semantik sieht logische Bedeutung als Resultat kanonischer Beweisoperationen: Durch Explikation von Einführungs- und Eliminationsverhalten und deren Harmonie entsteht eine Semantik, die normative Inferenzschemata mit der Interpretation logischer Konstanten verbindet.