Ein konstruktives logisches System, das logische Junktoren in Begriffen von Beweisbarkeit oder Konstruktionen interpretiert, das das uneingeschränkte Gesetz vom ausgeschlossenen Dritten zurückweist und häufig über natürliche Deduktion, Sequenzenkalküle, Heyting-Algebren oder Kripke-Semantik für konstruktive Wahrheit formalisiert wird.

Prinzip

Wahrheit ist an die Existenz eines Beweises oder einer Konstruktion gebunden: Ein Beweis von A∨B ist entweder ein Beweis von A oder ein Beweis von B mit Indikator; ein Beweis von A→B ist eine Methode, die jeden A-Beweis in einen B-Beweis überführt; ¬A bedeutet, dass A zu einem Widerspruch führt, statt absolute Falschheit von A zu behaupten.

Demonstration

In der konstruktiven Mathematik muss man zur Behauptung der Existenz eines Objekts mit Eigenschaft P eine Methode angeben, dieses Objekt zu konstruieren; ein konstruktiver Beweis von 'es existiert n mit P(n)' muss ein konkretes n und die Verifikation von P(n) liefern.

Fehlanwendung

Klassisches Schließen anzuwenden, wie Beweis durch Widerspruch, um Existenz ohne Zeugen zu folgern (d. h. ∃x P(x) allein aus ¬∀x¬P(x) abzuleiten), verletzt intuitionistische Standards und erzeugt nicht-konstruktive Existenzbehauptungen.

Konsequenz

Die Annahme intuitionistischer Logik sorgt dafür, dass Beweise mit Algorithmen oder Konstruktionen korrespondieren, was für Programmauszug, Typentheorie und konstruktive Mathematik vorteilhaft ist, aber klassische Schlüsse einschränkt und explizitere Konstruktionen verlangt.

Umkehrung

Der Umkehrfall ist die klassische Logik, welche das Gesetz vom ausgeschlossenen Dritten (A∨¬A) akzeptiert und nicht-konstruktive Existenzbeweise mittels Doppelnegationsbeseitigung und anderer klassischer Prinzipien erlaubt, die in der intuitionistischen Logik fehlen.

Abgrenzung

Intuitionistische Logik regelt konstruktives Schließen bezüglich Wahrheit und Beweisbarkeit; sie legt nicht zwangsläufig die berechenbare Komplexität der Konstruktionen fest und verhindert nicht alle Anwendungen der Doppelnegationslogik dort, wo zusätzliche konstruktive Prinzipien sie rechtfertigen.

Semantische Spannung

Es besteht Spannung zur klassischen Logik: Manche klassisch gültigen Sätze besitzen keine intuitionistische Beweise, wodurch ein Trade-off zwischen konstruktivem Inhalt (Algorithmen, Zeugen) und der größeren deduktiven Macht klassischer Logik entsteht.

Synthese

Intuitionistische Logik fasst Deduktion als Produktion von Konstruktionen auf: Junktoren und Quantoren werden als Vorschriften zum Aufbau von Beweisen oder Zeugen gelesen, wodurch eine beweistheoretische Grundlage entsteht, in der Existenz und Implikation eine algorithmische Bedeutung tragen statt bloßer Wahrheitswerte.