die im Rahmen des Intuitionismus entwickelte formale Logik. Der Intuitionismus ist eine, vornehmlich von Brouwer begründete, konstruktivistische Position in der Philosophie der Mathematik, die Anfang des 20. Jh. als Reaktion auf die durch die logischen Antinomien ausgelöste Grundlagenkrise der Mathematik entstand. Er ist gekennzeichnet durch die Auffassung von Mathematik als schöpferischer, geistiger Tätigkeit, die auf einer ›Ur-Intuition‹ beruht, der etwa die natürlichen Zahlen entspringen, und durch die mathematische Objekte und Sachverhalte erst konstruiert werden. Diese bestehen also nicht unabhängig vom menschlichen Denken und Erkennen. Daraus ergibt sich eine Ablehnung des Aktual-Unendlichen. Unendlichkeit besteht in unbegrenzter Fortsetzbarkeit und ist damit potentielle Unendlichkeit. Diesen finitistischen Standpunkt teilt der Intuitionismus mit dem Formalismus der Hilbert’schen Schule, als dessen Gegenposition er sich verstand. Im Unterschied zu Letzterem sieht der Intuitionismus das Wesen der Mathematik nicht im kalkülmäßigen Operieren mit ansonsten bedeutungslosen Zeichenfolgen. Für die i. L. bedeutet die Kritik am Aktual-Unendlichen eine Änderung des Wahrheits- wie des Existenzbegriffs gegenüber der klassischen Logik. Intuitionistisch wird Wahrheit als Beweisbarkeit und Existenz als effektive Konstruierbarkeit verstanden. Dies führt zu der, für die i. L. charakteristischen, Preisgabe des tertium non datur, A∨¬A. Damit ist die klassische Tautologie ¬¬A → A intuitionistisch ebenfalls nicht beweisbar. Umgekehrt ergibt sich die klassische Logik aus der intuitionistischen durch Hinzunahme des tertium non datur. Ebenso werden indirekte Existenzbeweise, wie etwa die Ableitung eines Widerspruchs aus der Annahme der Nichtexistenz, intuitionistisch nicht anerkannt. Die i. L. ist somit (echt) enthalten in der klassischen Logik, d.h. jede intuitionistisch beweisbare Formel ist auch klassisch beweisbar, aber nicht umgekehrt. Allerdings gilt, dass, wenn A klassisch beweisbar ist, dann ¬¬A in der i.n L. beweisbar ist.

Die erste vollständige Formalisierung der i.n L. stammt von Heyting (1930). Eine nur geringfügig schwächere Axiomatisierung wurde jedoch bereits 1925 von Kolmogorow vorgeschlagen. Nach diesen Darstellungen in Form axiomatischer Hilberttypkalküle gelang Gentzen 1934 eine Formalisierung der i.n L. durch einen Sequenzenkalkül und einen Kalkül des Natürlichen Schließens, die dem epistemischen Charakter der i.n L. angemessener erscheinen. Bemerkenswert ist die Tatsache, dass der intuitionistische Sequenzenkalkül aus dem klassischen gewonnen werden kann, indem nur Sequenzen zugelassen werden, die im hinteren Teil, dem Sukzedens, aus höchstens einer Formel bestehen.

Der semantische Aufbau der i.n L. gestaltete sich schwieriger. Einem Ergebnis von Gödel zufolge (1932) ist es nicht möglich, die i. Aussagen-L. durch Bewertungen mit endlich vielen Wahrheitswerten zu charakterisieren. Zudem sind (nach einem Resultat von McKinsey, 1939) die Junktoren der i.n L. voneinander unabhängig, also nicht wechselseitig auseinander definierbar. Die in den dreißiger Jahren entwickelte algebraische Semantik der i.n L. legte jedoch eine topologische Interpretation für die i.L. nahe. Formal ergibt sich diese aus dem Umstand, dass die offenen Punkte eines topologischen Raumes das klassische Beispiel sog. Heytingalgebren sind, mit denen die algebraische Struktur der i.n L. dargestellt wird. Da gewisse modallogische Systeme ebenfalls eine topologische Deutung erlauben, ergibt sich daraus die interessante Möglichkeit der Übersetzung der i.n L. in die Modallogik. Die naheliegendste Übertragung gelingt hierbei in das modallogische System S4, für dessen Modalitäten dadurch gleichzeitig eine Beweisbarkeitsinterpretation gegeben wird (Notwendigkeit wird dann verstanden als »beweisbar mit korrekten logischen Mitteln«). Eine solche Übertragung wurde 1932 von Gödel formuliert und 1948 von McKinsey und Tarski streng bewiesen. Indirekt resultiert aus dem Zusammenhang von i.r L. und Modallogik auch ein semantischer Aufbau der i.n L. Die durch Kripke Mitte der sechziger Jahre entwickelte Semantik für die i.L. ist im Wesentlichen eine Semantik der möglichen Welten, wie sie, ebenfalls v.a. von Kripke, zuerst für die Modallogik vorgeschlagen wurde. Formal weitgehend ähnliche Ansätze wurden einige Jahre zuvor von Beth und, etwa zeitgleich mit Kripke, von Grzegorczyk vorgeschlagen. Grundsätzlich soll dabei, wie Grzegorczyk meint, die i.L. als die Logik wissenschaftlicher Forschung betrachtet werden, die klassische Logik dagegen als die Logik eines ontologischen Standpunktes. Inwieweit die Kripke-Semantik der epistemischen Motivation der i.n L. allerdings gerecht wird, ist eine noch offene Frage. Anschaulich wird der klassische Wahrheitsbegriff dabei ersetzt durch die ›Wissenszustände‹ oder ›Informationsstadien‹ eines idealen Forschers, der sich weder mit dem Erwerb neuen Wissens irrt, noch früheres Wissen vergisst (und damit eine gewisse Monotonie-Eigenschaft besitzt). Dies führt formal (für den aussagenlogischen Fall) zu sog. Kripke-Modellen M = , bestehend aus einer nicht-leeren Menge W (anschaulich die genannten Informationsstadien), einer Halbordnung ≤ auf W und einer Funktion V, die jedem Element w von W eine Menge der in w ›gewussten‹ oder ›ermittelten‹ Elementaraussagen (also Atomformeln) zuordnet derart, dass für w≤w' V(w) eine Teilmenge von V(w') ist. Die semantische Grundrelation M ⊨_w A – lies: w erzwingt A (in M) –, die die klassische Erfüllungsrelation ersetzt, wird induktiv definiert durch:

(1) für eine Atomformel p: M ⊨_w p genau dann, wenn p ∈ V(w)

(2) M ⊨_w A ∧ B gdw M ⊨_w A und M ⊨_w B

(3) M ⊨_w A ∨ B gdw M ⊨_w A oder M ⊨_w B

(4) M ⊨_w A B → gdw für alle w' mit w≤w': wenn M ⊨_w' A, dann M ⊨_w' B

(5) M ⊨_w ¬A gdw für kein w' mit w≤w': M ⊨_w' A.

Für die Prädikatenlogik müssen zusätzliche Regeln für die in dem durch die Informationsstadien dargestellten Forschungsprozess ›konstruierten‹ Objekte formuliert werden, die garantieren, dass einmal konstruierte Objekte auch auf allen späteren Stufen zur Verfügung stehen.

Relativ zu der skizzierten Semantik lässt sich die Vollständigkeit ebenso wie Korrektheit der i.n L. beweisen. Dabei ist allerdings zu bemerken, dass die Vollständigkeitsbeweise für die i. Prädikaten-L. ursprünglich selbst nicht konstruktiv bzw. intuitionistisch formuliert waren. Dies liegt an der generell nicht konstruktiven Natur von Vollständigkeitsbeweisen, die zeigen, dass es für jede semantisch gültige Formel einen Beweis gibt, ohne eine solchen auch tatsächlich immer zu konstruieren, wie es für den intuitionistischen Existenzbegriff erforderlich wäre. Erst 1974 gelang durch Veldman ein intuitionistisch annehmbarer Vollständigkeitsbeweis für die i.L. mit Hilfe einer modifizierten Kripke-Semantik. – Die i. Aussagen-L. ist ebenso wie die klassische entscheidbar. Anders als im klassischen Fall ist allerdings bereits die monadische i. Prädikaten-L. nicht mehr entscheidbar.

Neben ihrer ausgeprägten epistemischen Motivation ist die i. L. philosophisch auch deshalb von Bedeutung, weil sie einen naheliegenden Ausgangspunkt für die Untersuchung der verschiedenen strukturellen Eigenschaften logischer Systeme darstellt. So liegen etwa zwischen der intuitionistischen und der klassischen Aussagenlogik überabzählbar viele sog. intermediäre Logiken, die als distributiver Verband angeordnet werden können. – Die i.L. ihrerseits ist eine echte Erweiterung des sog. Minimalkalküls von Johansson, aus dem sich die i. L. durch Hinzunahme des Axioms ¬p →(p → q) ergibt. In jüngster Zeit wird ein wachsendes Interesse der theoretischen Informatik an der i.n L. sichtbar, die sich, entsprechend ihrer epistemischen Motivation, als eine Logik der Informationsstrukturen verstehen lässt. So versteht sich die in den letzten Jahren von J. Girard vorgeschlagene lineare Logik als eine das konstruktivistische Element der i.n L. noch verstärkende Logik. – Auf der Grundlage der i.n L. wurde eine formale Darstellung der intuitionistischen Mathematik bis hin zur Analysis gegeben. Diese sieht sich allerdings der Schwierigkeit gegenüber, zahlreiche, für die klassische Mathematik konstitutive Begriffe wegen ihres nicht-konstruktivistischen Charakters nicht benützen zu können. Hierzu zählt u. a. der übliche Mengenbegriff, der faktisch eine Etablierung des Aktual-Unendlichen bewirkt.

Literatur:

• M. Dummett: Elements of Intuitionism. Oxford 1977
• M. Fitting: Intuitionistic Logic, Model Theory and Forcing. Amsterdam 1969
• A. Troelstra/D. van Dalen: Constructivism in Mathematics. Amsterdam 1988.

UM