Quelltext der Seite Intuitionismus (Logik und Mathematik)

Der '''Intuitionismus''' ist eine von [[Luitzen Egbertus Jan Brouwer|L. E. J. Brouwer]] begründete Richtung der [[Philosophie der Mathematik]], bei der die Mathematik als Tätigkeit des exakten Denkens angesehen wird, die ihre eigenen Objekte hervorbringt und nicht voraussetzt. Die Wahrheit mathematischer Aussagen wird reduziert auf ihre Konstruierbarkeit, womit der Intuitionismus als eine Art des [[Konstruktive Mathematik|Konstruktivismus]] gelten kann. Der Intuitionismus ist eine der Grundpositionen im [[Grundlagenstreit der Mathematik]].

== Grundgedanke ==
Die Wahrheit eines mathematischen Zusammenhangs wird in der intuitionistischen Mathematik erst anerkannt, wenn ein entsprechender Beweis formuliert wird. Wahre Aussagen oder von ihnen beschriebene Objekte haben keine Gültigkeit unabhängig von tatsächlichen Denkprozessen. Dies steht im Kontrast unter anderem zum sog. [[Platonismus]] in der Philosophie der Mathematik.

== Geschichte ==
Die Geschichte des Intuitionismus beginnt im Jahr 1912, als [[Luitzen Egbertus Jan Brouwer]] mit seiner Kritik am [[Satz vom ausgeschlossenen Dritten|Gesetz des ausgeschlossenen Dritten]] seine philosophischen Grundlagen formuliert. In den 1920er Jahren kam es zwischen der formalistischen Hilbert-Schule und Brouwer, der vom Hilbert-Schüler [[Hermann Weyl]] unterstützt wurde, zur in der Einleitung erwähnten Grundlagenkrise der Mathematik. Die erste vollständige [[Formalisierung]] intuitionistischer [[Aussagenlogik|Aussagen-]] und [[Prädikatenlogik]] stellt [[Arend Heyting]] im Jahr 1930 vor. 1933 zeigte [[Kurt Gödel]] eine Übersetzungsmöglichkeit von klassischer in intuitionistische Logik auf. Eine [[Modelltheorie|Semantik]] für die intuitionistische Logik präsentierte als erster [[Saul Kripke]]. Weitere Logiker und Mathematiker, die zum Intuitionismus beigetragen haben, sind [[Andrei Kolmogorow]], [[Stephen Kleene]] und in Deutschland [[Paul Lorenzen]].

=== Verhältnis zum mathematischen Konstruktivismus ===
Beweise nach intuitionistischen Paradigmen, die über die reine Logik hinausgehen und die Eigenschaften mathematischer Objekte untersuchen, führen zu einer [[Konstruktive Mathematik|konstruktiven Mathematik]]. Dies ergibt sich, weil ohne den Satz vom ausgeschlossenen Dritten keine [[Indirekter Beweis|Widerspruchsbeweise]] möglich sind, mit denen bei klassischer Logik die Existenz eines mathematischen Objektes bewiesen werden kann, indem die Nichtexistenz widerlegt wird. Der Intuitionismus gelangt insofern zu den gleichen Ergebnissen wie der Konstruktivismus, obwohl die dahinterliegenden philosophischen Betrachtungen unterschiedlich sind: Der Intuitionismus begründet sich auf einem nicht-klassischen Wahrheitsbegriff, der Konstruktivismus auf einem nicht-klassischen Existenzbegriff.

== Intuitionistische Logik ==
Die Gleichsetzung von Wahrheit und Beweisbarkeit erfordert eine damit kompatible Interpretation von mathematischen Aussagen und damit eine nichtklassische Logik. Während in der klassischen Logik die Aussage ''A''&nbsp;∨&nbsp;''B'' wahrheitsfunktional (siehe [[Wahrheitswert]]) interpretiert wird als „''A'' trifft zu, oder ''B'' trifft zu“, wird dieselbe Aussage in der intuitionistischen Logik interpretiert als: „Es gibt einen Beweis für ''A,'' oder es gibt einen Beweis für ''B,'' und man erkennt an ihm, ob er ''A'' oder ''B'' beweist.“

Aus dieser unterschiedlichen Interpretation der [[Junktor|logischen Verknüpfungen]] ergibt sich, dass bestimmte Theoreme der klassischen Logik in der intuitionistischen nicht gültig sind. Ein Beispiel ist der [[Satz vom ausgeschlossenen Dritten]], ''A''&nbsp;∨&nbsp;¬''A.'' Die klassische Interpretation lautet „''A'' trifft zu, oder ''A'' trifft nicht zu“ und ist leicht als gültig erkennbar. Die intuitionistische Interpretation lautet „''A'' ist beweisbar, oder ''A'' ist widerlegbar“ (wiederum mit der Forderung an den potentiellen Beweis, dass erkennbar sein muss, welche Teilaussage bewiesen worden ist). Wäre der Satz vom ausgeschlossenen Dritten in dieser Interpretation wahr, würde er die Vollständigkeit des Kalküls behaupten.

[[Kalkül]]e für die intuitionistische Logik müssen daher so beschaffen sein, dass in ihnen der Satz vom ausgeschlossenen Dritten nicht herleitbar ist. In einem Regelkalkül erreicht man das, indem man auf die Beseitigungsregel für die doppelte Negation verzichtet – für die Negation bleibt dann nur der [[Satz vom Widerspruch]] als Axiom oder als Regel. Auf diese Weise erhält man die intuitionistische Logik, welche den philosophischen Standpunkt in rein formaler Weise widerspiegelt.

=== Verhältnis des Intuitionismus zur klassischen Logik ===
Der Intuitionismus als [[Philosophie|philosophische]] bzw. metamathematische Richtung kritisiert nicht die [[klassische Logik]] als formales System, sondern stellt deren Anwendbarkeit auf wissenschaftliche, vor allem mathematische Fragestellungen in Frage bzw. vertritt die Meinung, dass andere logische Systeme diesen Fragestellungen angemessener sind.

Für den Intuitionismus als eine philosophische Position, die das Konzept der Beweisbarkeit in die Mitte ihrer Überlegungen stellt, ist  die klassische Logik, die logische Verknüpfungen als Wahrheitsfunktionen (siehe [[Wahrheitswert]]) interpretiert, schlechthin nicht von Interesse, weil Beweisbarkeit nicht als Wahrheitsfunktion darstellbar ist.

=== Satz vom ausgeschlossenen Dritten ===
Der [[Satz vom ausgeschlossenen Dritten]] wird problematisch, wenn er sich auf unendliche Mengen bezieht. Als Beispiel diene hier der Satz

''P'': ''Jede gerade Zahl, die größer als 2 ist, lässt sich als Summe zweier Primzahlen darstellen.''

Das Gegenteil dieses Satzes wird, nach der klassischen Logik, ausgedrückt durch den Satz

¬''P'': ''Es gibt eine gerade Zahl, die größer als 2 ist und sich nicht als Summe zweier Primzahlen darstellen lässt.''

Weder der Satz ''P'' noch der Satz ¬''P'' konnten bis heute bewiesen werden, siehe [[Goldbachsche Vermutung]].

Die Aufzählungsmethode ist kein geeigneter Ansatz, um ''P'' oder ¬''P'' zu beweisen: Zum einen kann ''P'' nicht in der Weise bewiesen werden, dass für jede gerade Zahl ''n'' zwei Primzahlen ''p'' und ''q'' aufgeschrieben werden, deren Summe ''p''&nbsp;+&nbsp;''q''&nbsp;=&nbsp;''n'' ergibt, denn es gibt unendlich viele gerade Zahlen. Um dagegen ¬''P'' zu beweisen, müsste eine gerade Zahl angegeben werden, für die die Zerlegung in zwei Primzahlen unmöglich ist. Falls ¬''P'' gilt, würde man zwar nach endlicher Zeit eine solche Zahl finden; falls aber ¬''P'' nicht gilt, würde man unendlich lange suchen.

Aus Sicht der Intuitionisten besagt der Satz vom ausgeschlossenen Dritten nun, dass eine der beiden oben dargestellten Aufgaben, also der Beweis von ''P'' oder der Beweis von ¬''P,'' durchführbar sein muss. Dies ist in der Tat nicht für alle Sätze ''P'' der Fall: Sollte eines Tages nun doch die Goldbachsche Vermutung bewiesen oder widerlegt werden, so gibt es dennoch viele andere Aussagen über unendliche Mengen, für die das gleiche Problem besteht (zum Beispiel die [[Kontinuumshypothese]]); der [[Gödelscher Unvollständigkeitssatz|Gödelsche Unvollständigkeitssatz]] zeigt zudem, dass solche Beispiele aus prinzipiellen Gründen existieren.

Der Satz vom ausgeschlossenen Dritten wird deshalb zwar in der [[Klassische Logik|klassischen Logik]] akzeptiert, nicht jedoch im Intuitionismus und der [[Gotthard Günther|Güntherlogik]].

== Inspiration für Informatiker ==
Informatiker entdeckten den Intuitionismus als Inspirationsquelle<ref>Bengt Nordström, Kent Petersson, Jan M. Smith: ''Programming in Martin-Löf’s Type Theory – An Introduction,'' 1990 ([https://www.cse.chalmers.se/research/group/logic/book/book.pdf PDF])</ref> und darauf aufbauend entstanden Beweisunterstützungssysteme wie [[Coq (Software)|Coq]], [[Epigram]] und [[Agda]], die für ihre Konstruktion und zur effektiven Benutzung die konstruktive Perspektive verlangen und beispielsweise den Satz vom ausgeschlossenen Dritten bestenfalls als [[Hack]] enthalten. Die tiefgreifende Beziehung liegt hier im [[Curry-Howard-Isomorphismus]], der Aussagen mit [[Datentyp|Typen]] und [[Beweis (Mathematik)|Beweise]] mit ([[Computerprogramm|Programmen]] zur Berechnung von) Werten des der zu beweisenden Aussage entsprechenden Typs gleichsetzt.

== Literatur ==
* [[Luitzen Egbertus Jan Brouwer|L. E. J. Brouwer]], Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten, in: ders., Collected Works, pp. 150–190, North-Holland Publishing Company, Amsterdam, Oxford 1975.
* L. E. J. Brouwer (Hrsg.), ''Intuitionismus,'' eingeleitet und kommentiert von Dirk van Dalen Mannheim, Leipzig, Wien, Zürich BI 1992, ISBN 3-411-15371-7.
== Einzelnachweise ==
<references />

== Weblinks ==
* {{SEP|https://plato.stanford.edu/entries/brouwer/|Luitzen Egbertus Jan Brouwer|Mark van Atten}}
* {{SEP|https://plato.stanford.edu/entries/intuitionistic-logic-development/|The Development of Intuitionistic Logic|Mark van Atten}}
* {{SEP|https://plato.stanford.edu/entries/intuitionism/|Intuitionism in the Philosophy of Mathematics|Rosalie Iemhoff}}
* {{SEP|https://plato.stanford.edu/entries/logic-intuitionistic/|Intuitionistic Logic|Joan Moschovakis}}
* {{SEP|https://plato.stanford.edu/entries/mathematics-constructive/|Constructive Mathematics|Douglas Bridges}}, insb. 3.1 ''Intuitionistic Mathematics''

[[Kategorie:Nichtklassische Logik]]
[[Kategorie:Konstruktivismus (Geistes- und Sozialwissenschaft)]]
[[Kategorie:Philosophie der Mathematik]]

[[pms:Antuissionism]]