1
2
Thema: Herleitungsspiele
Euklid (ca. 300 v. Chr.)
(1) Standard-Axiomatik für AL
(2) Kalkül des natürlichen Schließens für AL.
Ü i.f. : nach der Ü. von Clemens Thaer
axiuo = „auszeichnen“, „ehren“
Der Traum der Philosophen – mathematische Sicherheit:
Mathematiker können auf den Gebiet ihres Faches Beweise führen;
und wenn sie etwas bewiesen haben, so können sie sich ihrer Sache
sicher sein.
Platon (427 – 347 v. Chr.): Eingangsschild zur Akademie „Kein
Zutritt für Leute ohne Geometriekenntnisse“
Leibniz (1646 – 1716): Plan zur „Characteristica Universalis“
Wenn sich eine Meinungsverschiedenheit erhebt, so wird nicht mehr Diskussion
zwischen zwei Philosophen nötig sein als zwischen zwei Rechen-Spezialisten.
Es reicht dann nämlich, die Stifte in die Hand zu nehmen, sich an die
Rechentische zu setzen, und sich einander (wenn man möchte, nach
Hinzuziehung eines Freundes) zu sagen: Rechnen wir’s doch aus (calculemus)! 1
Hobbes (1588 – 1679):
He was forty years old before he looked on geometry; which happened
accidentally. Being in a gentleman’s library Euclid’s Elements lay open, and
‘twas the forty-seventh proposition in the first book. He read the proposition.
“By G[od]”, said he, “this is impossible!” So he reads the demonstration of it,
which referred him back to such a proof; which referred him back to another,
which he also read. Et sic deinceps [And so on], that at last he was
demonstratively convinced of that truth. This made him in love with geometry. 2
Spinoza (1632 – 1677): “Ethica ordine geometrico demonstrata”
1
übersetzt auch in: Bochenski, Formale Logik, S. 321 nach G.W. Leibniz, Abhandlung ohne Überschrift,
Vorarbeit zur allgemeinen Charakteristik (I), in: Die philosophischen Schriften von G.W.Leibniz, hg. v. C.I.
Gerhardt, Bd. VII, Nachdruck Hildesheim 1978, S.198-205, insbes. S. 200.
2 A brief Life of Thomas Hobbes, 1588 – 1679, by John Aubrey. Im Internet unter:
http://socserv2.socsci.mcmaster.ca/~econ/ugcm/3113/hobbes/life.
Ein Axiom ist ein Satz, der sich dadurch auszeichnet, dass er zur
Begründung anderer Sätze verwendet werden darf, ohne selbst durch
andere Sätze begründet werden zu müssen.
Bei Verwendung der axiomatischen Methode wird also mit Rekurs auf
eine kleine Menge nicht weiter begründeter Sätze, die axiomatische
Basis, ein zunächst begründungsbedürftiger Satz durch eine
lückenlose Folge von zuvor als erlaubt erklärten Begründungsschritten
begründet.
Die ersten drei (metrischen) Axiome Euklids
1. Was demselben gleich ist, ist auch einander gleich
[Wenn A = B und A = C, dann B = C]
2. Wenn Gleichem Gleiches hinzugefügt wird, sind die Ganzen
gleich
[ Wenn A = B und C = D, dann A + B = C + D]
3. Wenn von Gleichem Gleiches weggenommen wird, sind die
Reste gleich
[Wenn A = B und C = D, dann A - B = C - D]
Die ersten drei Postulate Euklids
1. Man kann von jedem Punkt zu jedem Punkt eine Strecke ziehen.
2. Man kann eine [durch Punkte] begrenzte gerade Linie beliebig
weit gerade verlängern.
3. Man kann um jeden Punkt als Mittelpunkt in gegebenem Abstand
einen Kreis ziehen.
3
4
[aus den Definitionen von Buch I]
Euklid I 1 (Anfang)
„[Man kann im Rahmen dieses Systems] über einer beliebigen
gegebenen Strecke ein gleichseitiges Dreieck errichten.
Die gegebene Strecke sei A B. [...]
[Denn man kann laut Postulat 1 von jedem Punkt zu jedem Punkt eine
Strecke zeichnen]
Mit A als Mittelpunkt und A B als Abstand zeichne man
den Kreis B C D
[Dies ist eine nach Postulat 3 mögliche Aktion]
Ebenso zeichne man mit B und Mittelpunkt und B A als Abstand
den Kreis A C E
[Dies ist eine weitere nach Postulat 3 mögliche Aktion]
Ferner ziehe man vom Punkt C, in dem die Kreise einander schneiden,
nach den Punkten A und B die Strecken C A und C B
[dies sind zwei nach Postulat 1 mögliche Aktionen].
C
D
A
B
Def. 1: Ein Punkt ist, was keine Teile hat
Def. 3: Die Enden einer Linie sind Punkte
Def. 4: Eine Strecke ist eine Linie, die zu den Punkten auf ihr
gleichmäßig liegt.
Def. 15: Ein Kreis ist eine ebene, von einer einzigen Linie umfaßte
Figur mit der Eigenschaft, dass alle von einem bestimmten innerhalb
der Figur gelegenen Punkte bis zur Linie laufenden Strecken einander
gleich sind.
Def. 16: Dieser Punkt heißt Mittelpunkt des Kreises.
Def. 20: Von den dreiseitigen Figuren ist ein gleichseitiges Dreieck
jede mit drei gleichen Seiten.
Def. 2: Eine Linie ist breitenlose Länge.
Def. 14: Eine Figur ist, was von einer oder mehreren Grenzen umfasst
wird.
Def. 19: Eine dreiseitige Figur ist eine geradlinige Figur, die von drei
Strecken umfasst wird. [zum Begriff der Strecke vgl. Def. 4!]
E
Def. 13: Eine Grenze ist das, worin etwas endigt.
5
Euklid I 1 (ganz)
„[Man kann im Rahmen dieses Systems] über einer beliebigen
gegebenen Strecke ein gleichseitiges Dreieck errichten.
6
Axiomatische Methode
Die gegebene Strecke sei A B. [...]
[Denn man kann laut Postulat 1 von jedem Punkt zu jedem Punkt eine Strecke zeichnen]
Mit A als Mittelpunkt und A B als Abstand zeichne man den Kreis B C D
[Dies ist eine nach Postulat 3 mögliche Aktion]
Ebenso zeichne man mit B und Mittelpunkt und B A als Abstand den Kreis A C E
[Dies ist eine weitere nach Postulat 3 mögliche Aktion]
Ferner ziehe man vom Punkt C, in dem die Kreise einander schneiden, nach den Punkten A
und B die Strecken C A und C B
[dies sind zwei nach Postulat 1 mögliche Aktionen]. ...
Jede Berufung auf einen bereits zuvor begründeten Satz kann als
Abkürzung für einen Beweis angesehen werden, der nur noch den
Rekurs auf Axiome (i.w.S.) enthält.
In diesem Sinn folgt alles Bewiesene allein aus der axiomatischen
Basis.
Da A Mittelpunkt des Kreises C D B ist, ist A C gleich A B
[Denn nicht nur B, sondern auch C liegt ja auf dem Kreis C D B; und
alle Punkte eines Kreises haben laut Def. 15 und Def. 16 vom
Mittelpunkt denselben Abstand]
Ebenso ist, da B Mittelpunkt des Kreises C A E ist, B C gleich [A B]
[Denn nicht nur A, sondern auch C liegt ja auf dem Kreis C A E; und
alle Punkte eines Kreises haben laut Def. 15 und Def. 16 vom
Mittelpunkt denselben Abstand] [...]
Also sind [A C] und [B C] beide gleich AB.
Was demselben gleich ist, ist [laut Axiom 1] auch einander gleich.
Also ist auch [A C] gleich [B C] .
Also sind [A C], A B und B C einander alle gleich.
Also ist das Dreieck A B C (laut Def. 20) gleichseitig.
Kants These (nicht Euklids):
„[D]er Geometer [ist] immer von der Anschauung geleitet“
KrV B 744
C
D
A
B
E
7
8
Warum ein Herleitungsspiel für AL?
Gottlob Frege
1848 in Wismar, + 1925 in Bad Kleinen
Begriffsschrift,
eine der arithmetischen nachgebildete
Formelsprache des reinen Denkens
(Halle 1879)
Aus dem Vorwort:
„Damit sich nicht [...] unbemerkt etwas Anschauliches eindrängen könnte,
musste Alles auf die Lückenlosigkeit der Schlusskette ankommen. Indem ich
diese Forderung auf das strengste zu erfüllen trachtete, fand ich ein Hindernis in
der Unzulänglichkeit der Sprache, die bei aller entstehenden Schwerfälligkeit
des Ausdruckes doch, je verwickelter die Beziehungen wurden, desto weniger
die Genauigkeit erreichen liess, welche mein Zweck verlangte. Aus diesem
Bedürfnis ging der Gedanke der vorliegenden Begriffsschrift hervor. Sie soll
also zunächst dazu dienen, die Bündigkeit einer Schlusskette auf die sicherste
Weise zu prüfen und jede Voraussetzung, die sich unbemerkt einschleichen will,
anzuzeigen, damit letztere auf ihren Ursprung hin untersucht werden könne.
Deshalb ist auf den Ausdruck alles dessen verzichtet worden, was für die
Schlussfolge nicht von Bedeutung ist.“ (Orig.-S.IV)
Grundgedanke:
Es sollte doch möglich sein, Beweise in stilisierter Form
nachzuspielen. Beweisen sollte ein Herleitungsspiel sein, in dem jeder
Spielzug durch eine Spielregel legitimiert sein muss.
Einwand
Man kann doch mit AL selbst schon Argumente nachspielen, indem man sie in
Ein-Zeilen-Schlüssen entsprechenden Formeln umschreibt und diese mit der
Wahrheitswertanalyse (Turbo-Methode) auf Allgemeingültigkeit überprüft. Wir
können doch mit der Wahrheitswertanalyse bereits die allgemeingültigen von
allen anderen Formeln unterscheiden. Und die Wahrheitswertanalyse ist doch
bereits ein nach strengen Regeln ablaufendes Verfahren zum Aufschreiben von
stilisierten Beweisen! Schließlich kann man doch das Durchführen der
Wahrheitswertanalyse als stilisierte Fallunterscheidung ansehen. Wozu brauchen
wir denn da noch ein extra Herleitungsspiel aus einer axiomatischen Basis?
Antwort:
1. Es ist interessant zu sehen, aus wie sparsamen Grundannahmen man mit
einem vernünftigen Herleitungsspiel alle allgemeingültigen Formeln von
AL herleiten kann. Aus wie wenigen Axiomen folgt eigentlich das
Ganze?
2. Die Beweise mit Hilfe der Wahrheitswertanalyse sind einfach von anderer
Art als Beweise in Form von Herleitungen. In einer Herleitung wird etwas
aus gewissen Voraussetzungen hergeleitet. Dabei ist gar nicht von
„schwarz“ und „weiß“ bzw. „wahr“ und „falsch“ die Rede.
Allgemeingültigkeit ist ein semantischer Begriff, die Grundidee eines
Herleitungsspiels ist es, Beweise rein syntaktisch führen zu können.
3. Eine Herleitung ist evtl. anschaulicher, näher an der Form eines
tatsächlich vorgebrachten Schlusses: wir müssen für eine Herleitung nicht
extra die einzelnen Zeilen in eine Ein-Zeilen-Formel umschreiben,
sondern können tatsächlich Prämissen untereinander notieren.
4. Es ist bei komplizierteren Logiken nicht gesagt, dass man einen so
einfachen Begriff von Allgemeingültigkeit findet wie für AL. Manche
Logiken, z.B. Modallogiken, baut man von der axiomatischen Seite her
auf. Will man in eine solche kompliziertere Logik AL integrieren, so ist es
gut, wenn sich AL axiomatisieren lässt.
9
10
Andernfalls kann Verschiedenes schiefgehen:
Ziel eines Herleitungsspiels
Ein Herleitungsspiel für eine formale Sprache L soll möglichst gerade
die Formeln von L herleitbar machen, die L-allgemeingültig sind, und
diejenigen Formeln nicht herleitbar machen, die nicht Lallgemeingültig sind. Man will die Menge der herleitbaren Formeln
und die der allgemeingültigen Formeln zur "Deckungsgleichheit"
bringen. Genauer gesagt strebt man nach
1. Widerspruchsfreiheit
(soundness – aber nicht in dem Sinn, in dem ein Schluss sound ist!):
Alle herleitbaren Formeln sind allgemeingültig.
Keine Formel soll herleitbar sein, wenn sie nicht allgemeingültig ist.
Keinesfalls darf es passieren (Super-GAU!) dass zwei Formeln beide
herleitbar sind, die einander „widersprechen“, also von denen z.B. die eine
allgemeingültig und die andere widersprüchlich ist.
2. Vollständigkeit
(completeness - Vollständigkeit)
Alle allgemeingültigen Formeln sind herleitbar.
Ist ein Herleitungsspiel für L sowohl widerspruchsfrei als auch vollständig, so
ist das Ziel der "Deckungsgleichheit" von L-allgemeingültigen und herleitbaren
Formeln erreicht.
1. Fall: Weder sound noch complete (ziemlich dämlich). Das Herleitungsspiel
erlaubt die Herleitung einiger, aber nicht aller allgemeingültiger Formeln,
zusätzlich aber die Herleitung einiger nicht allgemeingültiger Formeln.
Krasses Bsp.: Die folgende Axiomatik ist bezüglich AL weder sound noch
complete:
Axiome: (1) p → p
(2) (p ∧ ~ p)
Herleitungsregel: m.p., Subst (s.u.)
Denn man kann zwar (einfach durch Hinschreiben) eine allgemeingültige
Formel herleiten, nämlich (1); aber man kann längst nicht alle allgemeingültigen
Formeln herleiten (z.B. "(p ∨ ~ p)" nicht), und man kann (ebenfalls einfach
durch Hinschreiben) eine nicht allgemeingültige (sondern sogar
widersprüchliche) Formel herleiten. Herleitbare Formeln und allgemeingültige
Formeln überschneiden sich hier also nur teilweise:
herleitbare wffs
allgemeingültige wffs
2. Fall: sound, aber nicht complete (sehr häufig, nicht so schlimm). Alle
herleitbaren Formeln sind allgemeingültig, aber nicht alle allgemeingültigen
Formeln herleitbar.
Krasses Bsp.: (1) p → p als einziges Axiom
herleitbare wffs
allgemeingültige wffs
3. Fall: complete, aber nicht sound (GAU). Es sind zwar alle allgemeingültigen
Formeln herleitbar, obendrein aber noch irgendwelcher Schrott, den man nicht
haben will:
Krasses Bsp.: Standard-Axiomatik (s.u.) + Zusatzaxiom (4) (p ∧ ~ p)
allgemeingültige wffs
herleitbare wffs
11
Axiomatik für AL:3
Axiome
(1) (p → (q → p))
(2) ((p → (q → r)) → ((p → q) → (p → r)))
(3) ((~ p → ~ q) → (q → p)).
Herleitungsregeln
(Subst) p’s, q’s und r’s dürfen durch andere, ggfs. kompliziertere
wffs von AL ersetzt werden (natürlich durch dieselbe für alle p’s,
dieselbe für alle q’s etc.).
(modus ponens) Wenn du in einer Zeile eine wff der Gestalt (α → β)
vor dir hast und in einer anderen Zeile eine wff der Gestalt α, so darfst
du in einer weiteren Zeile β allein hinlegen.
1. „Patiencen-Legen“
2. Axiom: Du darfst diese wff „einfach so hinlegen“.
Herleitungsregel: „Wenn du in einer Zeile dieses hast, darfst du
jenes darunter legen“.
3. modus ponens als Herleitungsregel ≠ modus ponens als wff!
4. Man kann die Regel (Subst) noch einsparen, indem man nicht
Axiome angibt, sondern Axiomenschemata :
Axiome:
Axiome sind alle wffs der folgenden Gestalt
(1) (α → (β → α))
(2) ((α → (β → γ)) → ((α → β) → (α → γ)))
(3) ((~ α → ~ β) → (β → α)).
Herleitungsregel: m.p.
3 nach Kutschera / Breitkopf, Einf. I.d. mod. Logik, München 1971 u.ö., S.58; alternatives System mit 3 Axiomen:
Jan Lukasiewicz (1929), vgl. J.L., Aristotle’s Syllogistic, Oxford 2 1967, S. 80.
12
Zwei Einwände
1. „Kann dieser Vorschlag denn jemals eine vollständige
Axiomatik sein, wenn in keinem der Axiome Hut, Tüte und
Spaghetti vorkommen?“
Antwort: Definitionen für Zusatzkarten!
2.„Ok, jedes der Axiome ist AL-allgemeingültig. Aber sollten
Axiome nicht intuitiv fundamental sein? Aber das stimmt doch
höchstens für das dritte Axiom, weil es eine Richtung des
Kontrapositionsgesetzes ausdrückt. Aber die ersten beiden
Axiome?“
Antwort: Beim Axiomatisieren ist Sparsamkeit Trumpf, nicht die
Suche nach Fundamentalem (darüber einigt man sich sowieso nie).
13
14
Noch besser: Kalkül des natürlichen Schließens
Beispiel für eine Herleitung (vgl. Kutschera / Breitkopf S.60)
[ (α → (
β
→ α))
]
1.(p → ((q → p) → p))
[ ((α → (
β
→ γ )) →
Ax.1
((α →
β
) → (α → γ ))) ]
2.((p → ((q → p) → p)) → ((p → (q → p)) → (p → p))) Ax.2
3.
(p → (q → p)) → (p → p)
[ (α → ( β → α))
4.
Typisch: keine Axiome, nur Herleitungsregeln der Form:
„Wenn du in einer Zeile dieses hast, darfst du jenes darunter legen“.
]
(p → (q → p))
5.
1.,2., m.p.
Jeweils zwei Schlussregeln für jeden Junktor:
- eine Einführungsregel, die mir sagt, wann ich einen Junktor
einsetzen darf
- eine Eliminationsregel, die mir sagt, wie ich ihn wieder
loswerde.
Ax.1
(p → p)
3.,4., m.p.
Vorteil: AL ist mit den angegebenen Axiomen und dem m.p. als
Herleitungsregel widerspruchsfrei und vollständig axiomatisierbar.
Eine wff von AL ist damit herleitbar genau dann, wenn sie
allgemeingültig ist.
Nachteil: gekünstelt und unnatürlich.
Gewisser Ausgleich: Man muss einen Beweis nicht unbedingt führen
und damit kennen, um zu wissen, dass es ihn gibt:
Wenn eine wff allgemeingültig ist, dann gibt es dafür auch eine
Herleitung. Wenn eine wff nicht allgemeingültig ist, dann gibt es
dafür keine Herleitung. Man kann also in einem vollständigen System
mit der Wahrheitswertanalyse ein Gegenbeispiel für die
Allgemeingültigkeit finden und daraus den Schluss ziehen, dass es
auch keine axiomatische Herleitung dafür gibt.
Auf Einführungsregeln wird mit einem „I“ für „introduction“ Bezug
genommen und auf Eliminationsregeln mit einem „E“ für
„elimination“.
15
Kalkül des natürlichen Schließens für AL
nach L.T.F. GAMUT, Logic, Language and Meaning, Bd. 1, Chicago 1991, S. 128-148.
Regel
I ∧ : Wenn du in einer Zeile α hast,
und in einer Zeile β hast,
darfst du ( α ∧ β ) darunter legen.
Motivation
Aus α und β folgt „α und β“
E ∧ : Wenn du in einer Zeile ( α ∧ β ) hast,
dann darfst darunter α legen
und darfst darunter β legen.
Aus „α und β“ folg α und auch β
I ∨ : Wenn du in einer Zeile α hast,
darfst du ( α ∨ β ) darunter legen.
Aus α folgt bereits „α oder β“
E ∨ : Wenn du in einer Zeile ( α ∨ β ) hast,
in einer weiteren Zeile ( α → γ )
und in einer weiteren Zeile ( β → γ ),
dann darfst du γ darunter legen.
Wenn ich weiß, dass α oder β der Fall
ist, aber nicht, was von beidem, obendrein aber weiß, dass beides γ impliziert,
kann ich auf γ schließen.
E → : Wenn du in einer Zeile ( α → β ) hast,
Und in einer weiteren Zeile α,
dann darfst du β darunter legen.
modus ponens
I → : Wenn du in einer Zeile α mit „Hyp“
kommentiert hast und mit dieser Zeile
mit anderen Regeln β gewonnen hast,
so darfst du ( α → β ) darunter legen
und die Hyp-Zeile mit einer eckigen
Klammer verbinden.
Wenn unter der Annahme, dass α, folgt,
dass β, dann gilt „wenn α, dann β“
E ~ : Wenn du in einer Zeile ~ α hast
und in einer weiteren Zeile α,
darfst du die immer weiße Formel
⊥ darunter legen.
Widersprüche sind immer falsch
I ~ : Wenn du in einer Zeile α mit „Hyp“
kommentiert hast, und du, ohne
das „Hyp“ fallen zu lassen, in einer
weiteren Zeile auf ⊥ kommst, so
darfst du ~ α darunter legen.
Wenn im indirekten Beweis aus einer
Annahme ein Widerspruch gefolgert
wird, darf die Annahme negiert werden.
EFQ: Wenn du in einer Zeile ⊥ hast,
darfst du α darunter legen.
Aus einem Widerspruch folgt
Beliebiges (ex falso quodlibet)
DN:
Wenn du in einer Zeile ~ ~ α hast,
darfst du α darunter legen.
Gesetz der doppelten Negation
Vereinfachung: Bereits mit der Wahrheitswertanalyse als allgemeingültig erwiesene Formeln dürfen jederzeit
mit dem Kürzel „AL“ in Beweisgänge eingeführt werden.
16
Beispiel: NWS und DN implizieren den SAD
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
~(p∨~p)
~(p∨~p)→(~p∧~~p)
~p∧~~p
~~p
p
~p
p∧~p
~(p∧~p)
⊥
~~(p∨~p)
(p∨~p)
Hyp
AL (De Morgan mit ~ p für q)
2., E→
(m.p.)
3., E∧
4., DN
3., E∧
5., 6., I∧
AL
(NWS)
7., 8, E~
1., 9., I~
10., DN QED
17
Grenzen der Axiomatisierbarkeit
Die Russell-Paradoxie (Brief an Frege von 1902), sinngemäß:
"Wenn Ihre Logik stimmt, dann muss es so etwas geben wie die
Menge aller Mengen, die sich nicht selbst enthalten. Angenommen,
diese Menge sei in sich selbst enthalten. Dann gehört sie zur Menge
aller Mengen, die sich nicht selbst enthalten, woraus folgt, dass sie
nicht in sich selbst enthalten ist. Angenommen, sie sei nicht in sich
selbst enthalten, so gehört sie zur Menge der Mengen, die nicht in sich
selbst enthalten sind; woraus folgt, dass sie doch in sich selbst
enthalten ist."
Kurz:
Die Logik, die Frege für ausdrucksstark genug gehalten hatte, um
aus ihr die ganze Arithmetik herleiten zu können, war nicht
widerspruchsfrei.
Reparaturversuch: Principia Mathematica (1910) von Whitehead und
Russell
Kein Widerspruch, aber...
Kurt Gödel (1905 - 1978) zeigt 1931
Es ist prinzipiell unmöglich, die gesamte Mathematik als formal
bewiesene logische Formeln zu hinzuschreiben.
Keine formale Logik die intuitiv gesehen ausdrucksstark genug wäre, um aus ihr die ganze
Arithmetik herleiten zu können, ist vollständig axiomatisierbar.