Ein halb-konstruktives Prinzip, das aussagt, dass für ein entscheidbares Prädikat P über den natürlichen Zahlen, wenn es unmöglich ist, dass kein n P(n) erfüllt (¬¬∃n P(n)), dann ein n existiert mit P(n); informell fällt für entscheidbare Prädikate über die Naturzahlen die Doppelnegation von Existenz zur Existenz zusammen.

Prinzip

Doppelnegations-Elimination eingeschränkt auf entscheidbare arithmetische Existenziale: Wenn jede Instanz P(n) entscheidbar ist, dann führt die Nicht-Unmöglichkeit der Existenz zu einem tatsächlichen Zeugen durch ein effektives Suchargument oder eine endliche Widerlegung des universellen Scheiterns.

Demonstration

Betrachte ein entscheidbares Prädikat P(n) mit der metatheoretischen Tatsache ¬¬∃n P(n). Das Markow-Prinzip erlaubt, ∃n P(n) zu behaupten; rechnerisch entspricht dies einer effektiven Suche, die anhält, sobald ein n gefunden wurde, für das P(n) gilt, da für jedes n P(n) entscheidbar ist.

Fehlanwendung

Das Markow-Prinzip auf nicht entscheidbare Prädikate anzuwenden oder es als in allen konstruktiven Systemen beweisbar zu betrachten (es ist unabhängig von der intuitionistischen Arithmetik); außerdem darf es nicht mit dem allgemeinen Gesetz vom ausgeschlossenen Dritten oder uneingeschränkter Doppelnegations-Elimination verwechselt werden.

Konsequenz

Die Annahme des Markow-Prinzips erlaubt die Extraktion von Zeugen aus doppelt verneinten Existenzbehauptungen, wenn Prädikate entscheidbar sind, ermöglicht bestimmte konstruktive Suchprozeduren und stärkt berechenbare Interpretationen, ohne die volle klassische Logik zu übernehmen.

Umkehrung

Verwirft man das Markow-Prinzip, bleibt das Verhalten strikt konstruktiv: ¬¬∃n P(n) impliziert nicht notwendigerweise ∃n P(n), selbst wenn jedes P(n) entscheidbar ist; dies betont den Unterschied zwischen dem Wissen, dass universelles Scheitern unmöglich ist, und der Produktion eines Zeugen.

Abgrenzung

Gilt speziell für Prädikate über die natürlichen Zahlen, deren Instanzen jeweils entscheidbar sind; es ist keine allgemeine Doppelnegations-Elimination und gilt nicht für beliebige Formeln oder in jedem konstruktiven System ohne Annahme des Prinzips.

Semantische Spannung

Spannung zum Gesetz vom ausgeschlossenen Dritten und klassischem Denken: Das Markow-Prinzip ist schwächer als die volle klassische Logik, aber stärker als reiner Intuitionismus in der Art, wie es meta-level Nicht-Unmöglichkeit in Existenz für entscheidbare Prädikate umwandelt.

Synthese

Das Markow-Prinzip ist eine gezielte konstruktive Ergänzung: Wenn die Eigenschaft für jedes natürliche n entscheidbar ist, genügt die Unmöglichkeit eines universellen Scheiterns, um einen tatsächlichen Zeugen zu garantieren, wodurch eine endliche Suchrechtfertigung der Existenz möglich wird, ohne uneingeschränkte klassische Prinzipien anzunehmen.