Direkt zum Inhalt

Metzler Lexikon Philosophie: Logik, intuitionistische

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

Lesermeinung

Wenn Sie inhaltliche Anmerkungen zu diesem Artikel haben, können Sie die Redaktion per E-Mail informieren. Wir lesen Ihre Zuschrift, bitten jedoch um Verständnis, dass wir nicht jede beantworten können.

  • Die Autoren
AA Andreas Arndt, Berlin
AB Andreas Bartels, Paderborn
AC Andreas Cremonini, Basel
AD Andreas Disselnkötter, Dortmund
AE Achim Engstler, Münster
AG Alexander Grau, Berlin
AK André Kieserling, Bielefeld
AM Arne Malmsheimer, Bochum
AN Armin Nassehi, München
AR Alexander Riebel, Würzburg
ARE Anne Reichold, Kaiserslautern
AS Annette Sell, Bochum
AT Axel Tschentscher, Würzburg
ATA Angela T. Augustin †
AW Astrid Wagner, Berlin
BA Bernd Amos, Erlangen
BBR Birger Brinkmeier, Münster
BCP Bernadette Collenberg-Plotnikov, Hagen
BD Bernhard Debatin, Berlin
BES Bettina Schmitz, Würzburg
BG Bernward Gesang, Kusterdingen
BI Bernhard Irrgang, Dresden
BK Bernd Kleimann, Tübingen
BKO Boris Kositzke, Tübingen
BL Burkhard Liebsch, Bochum
BR Boris Rähme, Berlin
BS Berthold Suchan, Gießen
BZ Bernhard Zimmermann, Freiburg
CA Claudia Albert, Berlin
CH Cornelia Haas, Würzburg
CHA Christoph Asmuth, Berlin
CHR Christa Runtenberg, Münster
CI Christian Iber, Berlin
CJ Christoph Jäger, Leipzig
CK Christian Kanzian, Innsbruck
CL Cornelia Liesenfeld, Augsburg
CLK Clemens Kauffmann, Lappersdorf
CM Claudius Müller, Nehren
CO Clemens Ottmers, Tübingen
CP Cristina de la Puente, Stuttgart
CS Christian Schröer, Augsburg
CSE Clemens Sedmak, Innsbruck
CT Christian Tewes, Jena
CZ Christian Zeuch, Münster
DG Dorothea Günther, Würzburg
DGR Dorit Grugel, Münster
DH Detlef Horster, Hannover
DHB Daniela Hoff-Bergmann, Bremen
DIK Dietmar Köveker, Frankfurt a.M.
DK Dominic Kaegi, Luzern
DKÖ Dietmar Köhler, Witten
DL Dorothea Lüddeckens, Zürich
DP Dominik Perler, Berlin
DR Dane Ratliff, Würzburg und Austin/Texas
EE Eva Elm, Berlin
EJ Eva Jelden, Berlin
EF Elisabeth Fink, Berlin
EM Ekkehard Martens, Hamburg
ER Eberhard Rüddenklau, Staufenberg
EWG Eckard Wolz-Gottwald, Davensberg
EWL Elisabeth Weisser-Lohmann, Bochum
FBS Franz-Bernhard Stammkötter, Bochum
FG Frank Grunert, Basel
FPB Franz-Peter Burkard, Würzburg
FW Fabian Wittreck, Münster
GK Georg Kneer, Leipzig
GKB Gudrun Kühne-Bertram, Ochtrup
GL Georg Lohmann, Magdeburg
GM Georg Mildenberger, Tübingen
GME Günther Mensching, Hannover
GMO Georg Mohr, Bremen
GN Guido Naschert, Tübingen
GOS Gottfried Schwitzgebel, Mainz
GS Georg Scherer, Oberhausen
GSO Gianfranco Soldati, Tübingen
HB Harald Berger, Graz
HD Horst Dreier, Würzburg
HDH Han-Ding Hong, Düsseldorf
HG Helmut Glück, Bamberg
HGR Horst Gronke, Berlin
HL Hilge Landweer, Berlin
HND Herta Nagl-Docekal, Wien
HPS Helke Pankin-Schappert, Mainz
HS Herbert Schnädelbach, Berlin
IR Ines Riemer, Hamburg
JA Johann S. Ach, Münster
JC Jürgen Court, Köln
JH Jörg Hardy, Münster
JHI Jens Hinkmann, Bad Tölz
JK Jörg Klawitter, Würzburg
JM Jörg F. Maas, Hannover
JOP Jeff Owen Prudhomme, Macon/Georgia
JP Jörg Pannier, Münster
JPB Jens Peter Brune
JQ Josef Quitterer, Innsbruck
JR Josef Rauscher, Mainz
JRO Johannes Rohbeck, Dresden
JS Joachim Söder, Bonn
JSC Jörg Schmidt, München
JV Jürgen Villers, Aachen
KDZ Klaus-Dieter Zacher, Berlin
KE Klaus Eck, Würzburg
KG Kerstin Gevatter, Bochum
KH Kai-Uwe Hellmann, Berlin
KHG Karl-Heinz Gerschmann, Münster
KHL Karl-Heinz Lembeck, Würzburg
KJG Klaus-Jürgen Grün, Frankfurt a.M.
KK Klaus Kahnert, Bochum
KRL Karl-Reinhard Lohmann, Witten
KS Kathrin Schulz, Würzburg
KSH Klaus Sachs-Hombach, Magdeburg
LG Lutz Geldsetzer, Düsseldorf
LR Leonhard Richter, Würzburg
MA Mauro Antonelli, Graz
MB Martin Beisler, Gerbrunn
MBI Marcus Birke, Münster
MBO Marco Bonato, Tübingen
MD Max Deeg, Cardiff
MDB Matthias Bloch, Bochum
ME Michael Esfeld, Münster
MFM Martin F. Meyer, Koblenz/Landau
MK Matthias Kunz, München
MKL Martin Kleinsorge, Aachen
MKO Mathias Koßler, Mainz
ML Mark Lekarew, Berlin
MLE Michael Leibold, Würzburg
MM Matthias Maring, Karlsruhe
MN Marcel Niquet, Frankfurt a.M.
MQ Michael Quante, Köln
MR Mathias Richter, Berlin
MRM Marie-Luise Raters-Mohr, Potsdam
MS Manfred Stöckler, Bremen
MSI Mark Siebel, Hamburg
MSP Michael Spang, Ellwangen
MSU Martin Suhr, Hamburg
MW Markus Willaschek, Münster
MWÖ Matthias Wörther, München
NM Norbert Meuter, Berlin
OB Oliver Baum, Bochum
OFS Orrin F. Summerell, Bochum
PE Peter Eisenhardt, Frankfurt a.M.
PCL Peter Ch. Lang, Frankfurt a.M.
PK Peter Kunzmann, Jena
PN Peter Nitschke, Vechta
PP Peter Prechtl †
RD Ruth Dommaschk, Würzburg
RDÜ Renate Dürr, Karlsruhe
RE Rolf Elberfeld, Hildesheim
REW Ruth Ewertowski, Stuttgart
RH Reiner Hedrich, Gießen
RHI Reinhard Hiltscher, Stegaurach
RK Reinhard Kottmann, Münster
RL Rudolf Lüthe, Koblenz
RLA Rolf-Jürgen Lachmann, Berlin
RM Reinhard Mehring, Berlin
RP Roland Popp, Bremen
RS Regina Srowig, Würzburg
RTH Robert Theis, Strassen
RW Raymund Weyers, Köln
SD Steffen Dietzsch, Berlin
SIK Simone Koch, Bochum
SP Stephan Pohl, Dresden
SZ Snjezana Zoric, Würzburg
TB Thomas Bausch, Berlin
TBL Thomas Blume, Dresden
TF Thomas Friedrich, Mannheim
TG Thomas Grundmann, Köln
TH Thomas Hammer, Frankfurt a.M.
TK Thomas Kisser, München
TM Thomas Mormann, Unterhaching
TN Thomas Noetzel, Marburg
TP Tony Pacyna, Jena
TW Thomas Welt, Bochum
UB Ulrich Baltzer, München
UT Udo Tietz, Berlin
UM Ulrich Metschl, München/Leonberg
VG Volker Gerhardt, Berlin
VM Verena Mayer, München
VP Veit Pittioni, Innsbruck
VR Virginie Riant, Vechta
WAM Walter Mesch, Heidelberg
WB Wilhelm Baumgartner, Würzburg
WH Wolfram Hinzen, Bern
WJ Werner Jung, Duisburg
WK Wulf Kellerwessel, Aachen
WL Winfried Löffler, Innsbruck
WM Wolfgang Meckel, Butzbach
WN Wolfgang Neuser, Kaiserslautern
WP Wolfgang Pleger, Cochem/Dohr
WS Werner Schüßler, Trier
WST Wolfgang Struck, Erfurt
WSU Wolfgang Schulz, Tübingen
WvH Wolfram von Heynitz, Weiburg

Herausgegeben von Peter Prechtl (†) und Franz-Peter Burkard.

Partnerinhalte