Intuitionistische Mathematik < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Status: |
(Umfrage) Beendete Umfrage  | | Datum: | 16:52 Di 18.04.2017 | | Autor: | tobit09 |
Hallo zusammen!
Obwohl ich in meinem Studium viel mit mathematischer Logik zu tun hatte, war intuitionistische Logik kein Thema. Vor ein paar Tagen bin ich nun (im Rahmen des Computer-Programms "Coq Proof Assistant") auf sie gestoßen. Mich würde interessieren, was andere Matheraum-User über diese Mathematik denken.
(Einen groben Überblick für diejenigen, die auch zum ersten Mal ernsthaft damit in Berührung kommen, gibt ![[]](/images/popup.gif) Wikipedia.)
Als "Einstiegspunkt" möchte ich meine Meinung dazu präsentieren:
Unstrittig ist wohl, dass sowohl intuitionistische Logik als auch die (den meisten Mathematikern intuitiv vertraute) klassische Logik sich formal präzisieren lassen, so dass das Arbeiten in beiden jeweils als "Spiel mit wohldefinierten Spielregeln" aufgefasst werden kann. Nach den Spielregeln der klassischen Logik ist z.B. [mm] $A\vee\neg [/mm] A$ für jede "Aussage" A beweisbar, während in der intuitionistischen Logik folgende "Proposition" nicht beweisbar ist: "Für alle Propositionen A gilt [mm] $A\vee\neg [/mm] A$".
Strittig ist hingegen offenbar die Frage, welche Spielregeln "sinnvoller" sind. Schließlich arbeiten wir ja nicht in Logiken als "zufällig zusammengewürfelten" Spielregeln, sondern verbinden mit ihnen gewisse Vorstellungen ihrer Bedeutung.
Während klassische Logik die Vorstellung von Wahrheit und Falschheit ausdrückt, drückt die intuitionistische Logik in diesem Sinne die Vorstellung von Beweisbarkeit aus.
Beispiel: Ich bezeichne eine Menge M als "gut", wenn sie mindestens ein Element enthält. In der klassischen Logik bedeutet "M ist gut" intuitiv: "Die Aussage 'M ist gut' ist wahr", wobei die Vorstellung dahinter steht: "Für jede Menge M gilt: M ist gut oder M ist nicht gut". In der intuitionistischen Logik steht "M ist gut" hingegen intuitiv für "es gibt einen Beweis für 'M ist gut' ". Da es durchaus möglich ist, dass es weder für "M ist gut" noch für "M ist nicht gut" einen Beweis gibt, können wir intuitiv nicht einfach sagen, dass "M ist gut oder M ist nicht gut" beweisbar ist.
Entsprechend ist "M ist gut oder M ist nicht gut" nach klassischen "Spielregeln" beweisbar, nach intuitionistischen Spielregeln jedoch nicht.
Aus meiner Sicht drücken sowohl klassische Logik als auch intuitionistische Logik in diesem Sinne sinnvolle Vorstellungen in sinnvoller Weise aus. Es handelt sich also bei beiden Logiken nicht um "zufällig zusammengewürfelte" Spielregeln.
Nun frage ich mich: Warum polarisiert die intuitionistische Logik so? Kann man nicht sinnvoll mit beiden Logiken arbeiten, ohne die jeweils andere Logik für "minderwertig/unangemessen" zu erklären?
Ich möchte daher auf die Argumente sowohl von
a) "Gegnern" der intuitionistischen Logik als auch von
b) "Gegnern" der klassischen Logik
eingehen.
a) Mir fallen spontan zwei wesentliche Argumente ein, die gegen die intuitionistische Logik angeführt werden:
i) "Die intuitionistische Logik beschränkt zu sehr die Argumentationsmöglichkeiten der Mathematiker."
ii) "Die Resultate sind unintuitiv."
Zu i): Stellen wir uns vor, jemand argumentiert wie folgt: "Wenn wir statt mit dem Körper der rationalen Zahlen mit beliebigen Körpern arbeiten, schränkt das zu sehr die Argumentationsmöglichkeiten ein, denn dann können wir nicht einmal [mm] $1+1\not=0$ [/mm] beweisen." Ich würde antworten: Sowohl die rationalen Zahlen als auch beliebige Körper sind interessant, sie müssen nicht gegeneinander ausgespielt werden. Zwar können wir in beliebigen Körpern nicht [mm] $1+1\not=0$ [/mm] beweisen, aber dafür erhalten wir durch schwächere Annahmen an den Zahlbereich, in dem wir arbeiten, zwar weniger, aber allgemeinere Aussagen, als wenn wir nur über rationale Zahlen nachdenken. Entsprechend liefert Beschränkung auf intuitionistische Logik zwar weniger, aber allgemeinere Aussagen der Art "dieses Theorem ist auch in intuitionistischer Logik beweisbar". Das ist ähnlich zu Aussagen der Art "dieses Theorem ist auch ohne Auswahlaxiom beweisbar", deren Sinngehalt weniger umstritten ist.
Zu ii): Wenn man nur im Rahmen der intuitionistische Logik beweisbare Resultate zugrunde legt, sind alle diese Resultate erst Recht in der klassischen Logik beweisbar! Was unintuitiv erscheint, sind eher die "Nichtbeweisbarkeiten" gewisser in klassischer Logik beweisbarer Aussagen (z.B. es gibt Funktionen [mm] $\IR\to\IR$, [/mm] die nicht stetig sind). Aber diese "Nichtbeweisbarkeiten" scheinen mir sinnvoll, wenn man die oben geschilderte Vorstellung hinter der intuitionitischen Logik ("Propositionen sprechen über Beweisbarkeit statt Wahrheit") zugrunde legt.
(Leider beschränken sich manche Verfechter der intuitionistischen Ideen nicht auf die "normale" intuitionistische Logik und führen, ohne dies hinreichend deutlich zu machen, weitere Annahmen ein und kommen so zu Statements wie "Theorem: Alle Funktionen [mm] $\IR\to\IR$ [/mm] sind stetig", die sich eben offensichtlich NICHT mithilfe "normaler" intuitionistischer Logik beweisen lassen.)
b) Nun an die "Gegner" der klassischen Logik, die argumentieren, die "definitive Wahrheit oder Falschheit" von Propositionen gebe es i.A. nicht. Das mag aus philosophischer Sicht richtig sein. Dennoch spricht einiges für die Vorstellung von "Wahrheit oder Falschheit" jeder Proposition als MODELL-Vorstellung. D.h. ich sage nicht, dass es objektive Wahrheit oder Falschheit in der Wirklichkeit "gibt", sondern nur, dass die entsprechende Vorstellung sinnvoll ist. Ich weiß z.B. auch nicht ob die Vorstellung einer Gesamtheit aller unendlich vielen natürlicher Zahlen in der physikalischen Wirklichkeit eine Entsprechung hat; trotzdem bin ich vom Sinngehalt der Vorstellung einer Gesamtheit aller natürlichen Zahlen überzeugt. Ich gehe davon aus, dass die Vorstellung einer unendlichen Abfolge von Würfelwürfen, wie sie häufig in der mathematischen Stochastik betrachtet werden, keine Entsprechung in der physikalischen Realität haben. Dennoch erscheint mir die mathematische Vorstellung unendlich vieler Würfelwürfe als Modell-Vorstellung sinnvoll.
Mein Fazit: Ich finde beide Logiken spannend und sinnvoll. Schade, dass fast nur die klassische Logik gelehrt wird. Auch weitere Logiken (z.B. Modallogik, mit der ich mich noch nicht beschäftigt habe), scheinen spannend und sinnvoll zu sein...
Nun bin ich gespannt auf eure Meinungen! 
Viele Grüße
Tobias
|
|
| |
|
Lieber Tobias
Herzlichen Dank für diesen erhellenden Aufsatz ! Selber habe
ich mich zwar mit intuitionistischer Logik und Mengenlehre nur
vor langer Zeit mal etwas beschäftigt, aber mit deinen Zeilen
motivierst du mich jedenfalls, mich dem Thema wieder einmal
zuzuwenden und einiges vielleicht mit einer neuen inneren Haltung
neu zu betrachten.
Dein Hauptgedanke, dass das übliche Denken über Wahr/Falsch-
Entscheidungen auch in Logik und Mathematik durchaus hinterfragbar
ist und auch hinterfragt werden soll, scheint mir sehr wertvoll.
Vielleicht könnte ein solcher Aufruf zu einem weiter gefassten
Denken und Urteilen auch in anderen ("lebensnäheren (?)")
Bereichen, also etwa in gesellschaftlichen Fragen, nützlich werden ...
Bei Diskussionen über kosmologische Fragen im Rahmen eines
Forums stelle ich fest, dass Fragen über Endlichkeit / Unendlichkeit
offenbar doch mehr Menschen fesseln, als man zunächst erwarten
würde. Da gibt es etwa die Meinung, das Universum müsse aus
"rein logischen" Gründen endlich sein und z.B. eine endliche
Gesamtmasse haben. Es findet sich aber auch die exakt
entgegengesetzte Ansicht, ebenfalls "rein logisch" begründet ...
Das Nachdenken über Logik und das, was wir oft ungesagt
als Voraussetzungen des Denkens betrachten (oder nichtmal
"betrachten", sondern vielmehr unbewusst einbringen) ist
demnach durchaus auch wichtig im Zusammenhang der
Gestaltung unseres Weltbildes im Rahmen der ungeheuren
Dimensionen, welche uns Astrophysik und Kosmologie im
Lauf der letzten Jahrzehnte eröffnet haben !
LG , Al-Chwaruedi
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 23:08 Sa 22.04.2017 | | Autor: | tobit09 |
Hallo Al-Chwaruedi!
Danke für deine freundliche Antwort. Ich bin positiv überrascht, dass die intuitionistische Logik (zumindest bei dir) nicht auf grundsätzliche Ablehnung zu stoßen scheint...
Viele Grüße
Tobias
|
|
|
| |
|
Hallo tobit09,
was aus deinen Ausführungen nicht ganz hervorgeht, ist, dass das Schließen in intuitionistischer Logik auch Relevanz für die klassische Mathematik hat. Hierzu sollte man anmerken, dass Kategorien immer mit einer internen Logik ausgestattet kommen. In normalen Kategorien ist diese Logik ziemlich primitiv, aber wenn man mit einem Topos startet, bekommt man ziemlich genau die intuitionistische Logik heraus. Das heißt, dass man Sätze, die man konstruktiv beweisen kann, geeignet so interpretieren kann, dass sie Gültigkeit in jedem Topos haben. Da bieten sich zum Beispiel verschiedene Topoi, die in der algebraischen Geometrie aufkommen, an, zum Beispiel der Zariski-Topos oder der einfach Topos der Garben auf einem Raum. Jemand der dieses Spiel sehr gut spielt, ist Ingo Blechschmidt; du kannst dir ja mal die Einleitung hierzu durchlesen. Ein klassischer (und leichter lesbarer) Zugang ist "Sheaves in Geometry and Logic" von Mac Lane und Moerdejk. Dort findest du auch Anwendungen auf rein logische Probleme, z.B. einen Beweis zur Unabhängigkeit der Kontinuumshypothese. Was dich ganz sicher interessiert (gerade, da du mit Coq zu tun hattest) dürfte das Homotopie-Typentheorie-Buch sein, das du frei hier findest. Es setz keinerlei Vorwissen voraus. Lies da unbedingt mal rein!
Liebe Grüße,
UniversellesObjekt
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig | | Datum: | 12:56 Mo 24.04.2017 | | Autor: | tobit09 |
Hallo UniversellesObjekt!
Vielen Dank für deine Anregungen!
Die Frage nach einer befriedigenden Grundlegung der Mathematik finde ich ungleich wichtiger, als wenn (überspitzt formuliert) zusätzlich zu den schon bewiesenen 425233 Theoremen das 425234. Theorem bewiesen wird...
Typentheorie scheint mir diesbezüglich besser zu gefallen als Mengenlehre.
Ob auf Typentheorie aufbauende Kategorien-theoretische Grundlegung auch für eigentlich nicht Kategorien-Theorie-affine Mathematiker wie mich einen weiteren Vorteil bringt, kann ich (noch?) nicht beurteilen.
Eine Befürchtung habe ich jedoch: Schon Typentheorie hat eine gewisse Komplexität. Wenn wir jetzt auch noch Kategorien-Theorie zur Grundlegung brauchen, könnte diese Mathematik für Studienanfänger unvermittelbar werden, so dass die Lehre an der Uni wohl nach wie vor mit naiver Mengenlehre begonnen werden müsste, um dann später gegebenenfalls "umzusteigen"...
Viele Grüße
Tobias
|
|
|
| |
|
> Hallo UniversellesObjekt!
>
>
> Vielen Dank für deine Anregungen!
>
> Die Frage nach einer befriedigenden Grundlegung der
> Mathematik finde ich ungleich wichtiger, als wenn
> (überspitzt formuliert) zusätzlich zu den schon
> bewiesenen 425233 Theoremen das 425234. Theorem bewiesen
> wird...
Naja, so wie ich das sehe, ist das der Job eines (reinen) Mathematikers...
> Typentheorie scheint mir diesbezüglich besser zu gefallen
> als Mengenlehre.
> Ob auf Typentheorie aufbauende Kategorien-theoretische
> Grundlegung auch für eigentlich nicht
> Kategorien-Theorie-affine Mathematiker wie mich einen
> weiteren Vorteil bringt, kann ich (noch?) nicht
> beurteilen.
> Eine Befürchtung habe ich jedoch: Schon Typentheorie hat
> eine gewisse Komplexität. Wenn wir jetzt auch noch
> Kategorien-Theorie zur Grundlegung brauchen, könnte diese
> Mathematik für Studienanfänger unvermittelbar werden, so
> dass die Lehre an der Uni wohl nach wie vor mit naiver
> Mengenlehre begonnen werden müsste, um dann später
> gegebenenfalls "umzusteigen"...
Die Homotopie-Typentheorie wird zwar von einigen Kategorientheoretikern (Awodey, Voevodsky (naja, seine Fields-Medaille hat er für Algebra gewonnen)) vorangetrieben, aber sie baut nicht darauf auf und hat auch sonst nicht direkt viel mit KT zu tun. Hast du dir die ersten Seiten mal angesehen? Es ist vielleicht etwas gewöhnungsbedürftig, diesen (vermutlich) neuen Begriff eines "Typs" zu akzeptieren, aber andererseits vermutlich nicht schwieriger als das Konzept einer abstrakten Menge, wenn man sie das erste mal sieht.
Und eines der Hauptziele ist ja, die Mathematik zugänglicher für Beweis-Assistenten wie Coq von Coquand (der auch bei HoTT mitwirkt) zu machen. Das wird also Auswirkungen für alle Bereiche der reinen Mathematik haben. (Ich habe neulich mit einem Homotopietheoretiker darüber gesprochen, und der hat vorausgesat, HoTT würde die Mathematik revolutionieren. Das liest man von allen Leuten, die darin involviert sind. Ich selbst kann das nicht einschätzen; mehr als das erste Kapitel des Buches habe ich dazu nicht gelesen.)
> Viele Grüße
> Tobias
Liebe Grüße,
UniversellesObjekt
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig | | Datum: | 01:15 So 30.04.2017 | | Autor: | tobit09 |
> Die Homotopie-Typentheorie wird zwar von einigen
> Kategorientheoretikern (Awodey, Voevodsky (naja, seine
> Fields-Medaille hat er für Algebra gewonnen))
> vorangetrieben, aber sie baut nicht darauf auf und hat auch
> sonst nicht direkt viel mit KT zu tun.
Danke für den Hinweis. Dann habe ich mich diesbezüglich vertan.
> Hast du dir die
> ersten Seiten mal angesehen?
Grob gelesen habe ich bisher die (ziemlich lange) Einleitung, die ich noch nicht so erhellend fand.
Vermutlich wird Einiges klarer, wenn man den eigentlichen Text studiert.
> Es ist vielleicht etwas
> gewöhnungsbedürftig, diesen (vermutlich) neuen Begriff
> eines "Typs" zu akzeptieren, aber andererseits vermutlich
> nicht schwieriger als das Konzept einer abstrakten Menge,
> wenn man sie das erste mal sieht.
Mit Prädikatenlogik und Mengen lässt sich ganz gut naiv umgehen.
Ich weiß nicht, ob ein entsprechender naiver Zugang zu Typentheorie praktikabel ist.
> Und eines der Hauptziele ist ja, die Mathematik
> zugänglicher für Beweis-Assistenten wie Coq von Coquand
> (der auch bei HoTT mitwirkt) zu machen.
Dieses Ziel begrüße ich ausdrücklich. (Vielleicht trägt es auch zu einer genaueren und weniger grob skizzierenden Mathematik bei, die die Verantwortung für die Details vom Leser auf den Urheber überträgt?)
Weißt du, welche(n) Vorteil(e) HoTT z.B. gegenüber der in Coq ohnehin eingebauten Typentheorie hat?
> Das wird also
> Auswirkungen für alle Bereiche der reinen Mathematik
> haben.
(Siehst du eine Beschränkung der Auswirkungen ausschließlich auf REINE Mathematik?)
> (Ich habe neulich mit einem Homotopietheoretiker
> darüber gesprochen, und der hat vorausgesat, HoTT würde
> die Mathematik revolutionieren. Das liest man von allen
> Leuten, die darin involviert sind. Ich selbst kann das
> nicht einschätzen; mehr als das erste Kapitel des Buches
> habe ich dazu nicht gelesen.)
Um so mehr frage ich mich, was HoTT hat, was Coq nicht hat...
Dass eine neue Grundlegung der Mathematik grundsätzlich eher die Mathematik revolutionieren kann als das 425234. bewiesene mathematische Theorem, erscheint mir jedenfalls klar. 
|
|
|
|
