Eine Gruppe mathematischer Auffassungen, die explizite Konstruktionen oder Algorithmen verlangen, um Existenzaussagen zu bezeugen, und die typischerweise nichtkonstruktive Prinzipien wie das uneingeschränkte Ausschlussprinzip zurückweisen; Beweise sollen rechnerischen Gehalt liefern.

Prinzip

Existenz bedeutet die Fähigkeit, ein Zeugenobjekt oder einen Algorithmus zu liefern; logische Prinzipien und mengentheoretische Axiome werden nur insoweit akzeptiert, als sie eine rechnerische oder konstruktive Interpretation zulassen (intuitionistische Logik, Typentheorie, konstruktive Mengentheorie).

Demonstration

Ein konstruktiver Existenzbeweis des größten gemeinsamen Teilers durch Angabe des euklidischen Algorithmus liefert ein explizites Zeugnis und ein terminierendes Verfahren, während ein klassischer nichtkonstruktiver Widerspruchsbeweis abgelehnt würde.

Fehlanwendung

Eine klassische nichtkonstruktive Beweisführung ohne algorithmischen Zeugen fälschlich als konstruktiv zu bezeichnen oder anzunehmen, jedes klassische Theorem lasse sich ohne Weiteres konstruktiv übersetzen, ohne Definitionen zu ändern oder Annahmen zu stärken.

Konsequenz

Führt zu beweisen mit algorithmischem Gehalt, ermöglicht Programmextraktion und verifizierte Berechnung aus Beweisen und verfeinert oft klassische Aussagen zu rechnerisch interpretierbaren Formen.

Umkehrung

In der klassischen Mathematik wird Wahrheit großzügiger behandelt (Zulassung des ausgeschlossenen Dritten und nichtkonstruktiver Existenzbeweise) und man legt mehr Gewicht auf Theoremformulierungen als auf konstruktive Zeugen, was kürzere oder allgemeinere Existenzbehauptungen zulässt.

Abgrenzung

Umfasst verschiedene formale Systeme (Bishop'sche konstruktive Analysis, intuitionistische Typentheorie, konstruktive Mengentheorie) mit unterschiedlichen Axiomen; schließt klassische Mathematik nicht ein, es sei denn sie wird zur Bereitstellung von Konstruktionen umformuliert.

Semantische Spannung

Spannung zwischen dem Wunsch nach konstruktiven Zeugen und der klassischen Bequemlichkeit nichtkonstruktiver Prinzipien; zwischen verschiedenen konstruktiven Schulen hinsichtlich akzeptabler Axiome (Auswahlaxiom, abzählbares Auswahlaxiom, Markov-Prinzip).

Synthese

Konstruktive Mathematik verlangt konsistent, dass Existenzbehauptungen expliziten Konstruktionen oder Algorithmen entsprechen, und ordnet Logik und Grundlagen neu, um rechnerischen Gehalt und verifizierbare Zeugnisse in Analysis, Algebra und Logik zu priorisieren.