Einführung in die mathematische Logik - ub-net · 2012. 1. 22. · Logik-1 Einführung in die...

27
Logik-1 Einführung in die mathematische Logik Ein Crashkurs über die Grundlagen wichtiger Logiken und Beweiskalküle Uwe Bubeck 13. Juli 2000 Proseminar „Maschinelles Beweisen“ SS 2000

Transcript of Einführung in die mathematische Logik - ub-net · 2012. 1. 22. · Logik-1 Einführung in die...

  • Logik-1

    Einführung in diemathematische Logik

    Ein Crashkurs über die Grundlagenwichtiger Logiken und Beweiskalküle

    Uwe Bubeck13. Juli 2000

    Proseminar „Maschinelles Beweisen“ SS 2000

  • Logik-2

    Einleitung und Motivation

    Einführung in die mathematische Logik

  • Logik-3

    Motivation

    „Logik ist der Anfang aller Weisheit“Mr. Spock

    • Umgangssprache: Unschärfen, Mehrdeutigkeiten→ ungeeignet zur exakten Wissensrepräsentation

    • Korrektheit logischer Ableitungen führt zuglaubwürdigen neuen Erkenntnissen→ Problem der korrekten Modellierung

  • Logik-4

    Einschränkungen

    „Logik ist die Hygiene, deren sich der Mathematikerbedient, um seine Gedanken gesund und kräftig zuerhalten“Hermann Weyl

    • Hilfsmittel der Mathematik versus praktisches Werkzeug– Notation nicht für automatische Beweissysteme konzipiert

    – Tatsächliche Beweisführung häufig schwierig

    • Einschränkungen für maschinelle Handhabbarkeit

    → Unentscheidbarkeit und Unvollständigkeit

  • Logik-5

    Historischer Überblick• Aristoteles (384 - 322 v. Chr.): Syllogismus

    „Jeder Grieche ist ein Mensch Jeder Mensch ist sterblich-> Jeder Grieche ist sterblich“

    • Boole (1815-1864): Aussagenlogik als Algebra• Frege (1848-1929): Prädikatenlogik• Russel (1872-1970): Antinomien, Typisierung• Church (1903-1995): Lambda-Kalkül• Gödel (1906-1978): Unentscheidbarkeit• Gentzen (1909-1945): Sequenzenkalkül• 1954-58: Erste maschinelle Beweise• 1963ff: Unifikation und Resolution• 1970ff: Prolog• 1985ff: Beweisen in nichtklassischen Logiken

  • Logik-6

    Logische Grundlagen

    Einführung in die mathematische Logik

  • Logik-7

    Syntax formaler Systeme

    • Besonderheit der Implikationfalsch � wahr und falsch � falsch per Definition

    • Strukturelle InduktionBeispiel: sind φ und ψ Formeln, dann auch (φ ∧ ψ)

    Phase abgelaufen Keine Autos mehr Fußgängertaste

    Umschalten

    ¬

    Disjunktion

    Konjunktion

    Negation

    Implikation

    • Beispiel: Syntaxbaum

  • Logik-8

    Axiome und Inferenzregeln• Axiome: Menge grundlegender Sätze als wahr vorgegeben

    • Angabe über AxiomschemataBeispiel: Gesetz der ausgeschlossenen Mitte

    φ ∨ ¬φ

    Für φ kann eine beliebige Formel eingesetzt werden→ Metasprache ≠ Objektsprache

    • Schemata auch für Inferenz- und AbleitungsregelnBekanntes Beispiel: Modus Ponens

    ψψφφ �,

  • Logik-9

    Beweise und Modelle

    Einführung in die mathematische Logik

  • Logik-10

    Beweise

    • Beweise sind syntaktischeUmformungen → Mechanisierbarkeit

    • Problem: Auswahl derBeweisschritte

    Beweis: Eine Folge von Formeln φ1.. φn mit der zubeweisenden Zielformel φn = ψ und einer Menge Γ vonVoraussetzungen. Für jedes φi muß gelten:•φi ist ein Axiom oder•φi ist in den Annahmen Γ enthalten oder•φi ist eine Ableitung aus vorangegangenen Beweisschritten.

    Axiom Axiom

    Inferenz

    Annahme

    Inferenz

    Zielformel

    Beweisbaum

  • Logik-11

    Interpretationen und Modelle

    • Interpretationen häufig induktiv festgelegt

    • Interpretation A ist Modell von φ, wenn φ in A wahr ist

    • Interpretation als Beziehung zwischen Syntax und Semantik

    • Interpretation als Zuordnung eines Wahrheitsgehaltes

    Interpretation∀x:(∃y:(x+1=y)) „Natürliche Zahlen

    sind unbeschränkt“

    ∀x:(∃y:(x+1=y))Grundmenge M

    wahr

    falsch

    natürliche Zahlen

    Primzahlen

  • Logik-12

    Wichtige Systemeigenschaften• Entscheidbarkeit: algorithmisch entscheidbar,

    ob eine beliebige Formel ein Satz ist→ Optimalsituation für automatisches Beweisen

    • Semi-Entscheidbarkeit: Entscheidungsalgorithmusterminiert i. a. nur für Sätze oder unerfüllbare Formeln→ Reine Erfüllbarkeit nicht maschinell nachweisbar!

    • Vollständigkeit: jede wahre Formel ist beweisbar• Korrektheit: jede beweisbare Formel ist wahr

    Sätze unerfüllbareFormelnerfüllbareFormeln

  • Logik-13

    Schematische Darstellung

    Beschreibung innatürlicher Sprache

    SyntaxFormale Sprache

    Wahre Formeln Beweisbare Formeln

    SemantikWahrheitsgehalt

    KalkülAbleitung

    Formalisierung

    Vollständigkeit

    Korrektheit

    (Automatisches) Beweisen

    Modellierung

  • Logik-14

    Aussagenlogik

    Einführung in die mathematische Logik

  • Logik-15

    Aussagenlogik

    • Verknüpfungen: Negation und ImplikationWeitere durch Makros (Abkürzungen) oder AbleitungsregelnBeispiel Disjunktion:

    • Induktive Syntaxdefinition– Jedes Atom ist eine aussagenlogische Formel– Sind φ und ψ Formeln, dann auch (¬φ) und (φ�ψ)

    • Ableitungsregel: Modus Ponens

    • Axiomschemata: Hilbert-Kalkül– φ � (ψ�φ)– (φ�(ψ�ρ)) � ((φ�ψ)�(φ�ρ))– (¬(¬φ)) � φ

    ψφψφ

    ψφψφ

    ∨�¬

    �¬∨ )()(

  • Logik-16

    Aussagenlogische Beweise

    • Interpretation über Wahrheitswerte� Vollständigkeit und Korrektheit� Entscheidbarkeit (betrachte Wahrheitstafeln)

    • Möglichkeiten für (automatisches) Beweisen– beweistheoretisch (syntaktisch):

    • Hilbert-Kalkül: Auswahl der Schritte schwierig• Sequenzenkalkül: gut mechanisierbar

    – modelltheoretisch:• Wahrheitstafeln: nur für einfache Formeln• Resolution: oft sehr effizient; Vorverarbeitung

    -+

    +

  • Logik-17

    Sequenzenkalkül

    • Gentzen 1943. Ziel: intuitive Beweise→ verwendet vor allem Ableitungsregeln

    • Beweis eines Satzes φ Sequenzenbaum mit Wurzel →φ

    • Ableitungsregeln erzeugen Baum von der Wurzel aus.Blatt Γ→∆ wird Verzweigung mit n neuen Blättern Γi→∆i

    • Beweis erfolgreich, wenn alle Äste abgeschlossen durchdas „aussagenlogische Axiom“:

    Sequenzen: Ausdrücke Γ→∆ mit Bedeutung: VorbedingungenΓ ={Γ1∧...∧Γn} implizieren Nachbedingungen ∆={∆1∨... ∨ ∆n}

    ....11 Nnn

    ∆→Γ∆→Γ∆→Γ

    .,,

    Ax∆→Γ φφ

  • Logik-18

    Sequenzenkalkül: Beispiel

    • Folgeschritte oft vorausbestimmt oder wenige Alternativen→ Beweiser muß weniger Möglichkeiten durchprobieren

    • Erweiterung auf Prädikatenlogik möglich

    )()()()(RQPRQP

    RQPRQP�∧���→�∧→��

    )()(,),(

    RQPRQPRQPRQP�∧→��

    →��

    RQPRQRQPR→�

    →,),(

    ,,RQPRQ

    RQQP→�

    →,),(

    ,,

    RQPRQPRQPRQ→��

    →�,),(

    ,),(RQPRQP

    RPQP→��

    →,),(

    ,,

  • Logik-19

    Prädikatenlogik

    Einführung in die mathematische Logik

  • Logik-20

    Prädikatenlogik• Prädikatenlogik ausdrucksstärker als Aussagenlogik

    Beispiel: „wenn n ungerade ist, dann ist 2n gerade“– Unzureichend: Ausdruck der Form n_ungerade�2n_gerade– Mit Quantifizierung:∀n:(ungerade(n)�gerade(verdopple(n))

    • Erweiterung der Aussagenlogik um– Quantifizierungen „für alle“ (∀) bzw. „es existiert ein“ (∃)– Konstanten (a,b,...)– Variable (x,y,...)– Funktionssymbole (f,g,...)– Prädikatsymbole (P,Q,...)

    • Quantifizierungen erlaubt über– Variable (Prädikatenlogik erster Stufe)– Funktionen und Prädikate (zweite Stufe)

  • Logik-21

    Prädikatenlogik: Syntax, Interpretation

    • Induktive Definition wohlgeformter Formeln– Jede Variable ist ein Term– Ist f ein k-stelliges Funktionensymbol, und sind τ1,..., τk Terme,

    dann ist auch f(τ1,..., τk) ein Term– Ist P ein k-stelliges Prädikatsymbol, und sind τ1,..., τk Terme,

    dann ist P(τ1,..., τk) eine (atomare) Formel– Sei x Variable, und seien F und G Formeln. Dann sind auch ¬F,

    (F∧G) und (F∨G) sowie ∃x:F und ∀x:F Formeln

    • Interpretation prädikatenlogischer Formeln:– Grundmenge und passende Funktionen und Prädikate festlegen– Interpretationsprozeß verläuft gemäß Schachtelung der Formel– Quantoren: Elemente der Grundmenge überprüfen

  • Logik-22

    Prädikatenlogik: Axiome, Inferenz

    • Unterscheidung: gebundene und freie Variablen

    • Zwei zusätzliche Axiome– (∀x:φ(x)) � φ[x/t]– φ[x/t] � (∃x: φ(x))

    • Vorsicht: freie Variable dürfen dabei nicht gebunden werden

    Beispiel „jede natürliche Zahl besitzt einen Nachfolger“:∀x:(∃y:(x+1=y)) wird zu der falschen Aussage ∃y:(y+1=y)„eine natürliche Zahl ist gleich ihrem Nachfolger“

    • Außerdem Generalisierung als weitere Inferenzregel

    ψφψφ

    φψφψ

    �∃�

    ∀��

    ))(:()(

    ))(:()(

    xxv

    xxv

  • Logik-23

    AusblickZusammenfassung

    Einführung in die mathematische Logik

  • Logik-24

    Ausblick• Typisierte Prädikatenlogik

    Beispiel:∀x:String(∃y:Integer(Länge(x)=y))→ vermeide sinnlose Einsetzungen: Effizienz

    • Mehrwertige LogikEinführung zusätzlicher WahrheitswerteBeispiel: {falsch, undefiniert, wahr}

    • Modale Aussagenlogik „notwendigerweise“, � „möglicherweise“Beispiel: Beschreibung intelligenter Agenten

    • Temporale Aussagenlogik „immer“, � „irgendwann“Beispiel: Kommunikationsprotokolle

  • Logik-25

    Zusammenfassung

    • Logiken unterschiedlicher Ausdrucksstärke

    • Mächtigkeit versus maschinelle Handhabbarkeit→ Sorgfältige Auswahl. Standard: Prädikatenlogik

    • Prinzipielle Grenzen→ Entscheidbarkeit

    • Verschiedene Beweisverfahren→ Zusammenhang Syntax und Interpretation

  • Logik-26

    Definitionen-1

    Formales System: System, welches über eine formaleSprache mit der Möglichkeit zur Deduktion (logischeFolgerung) verfügt. Logische und nichtlogische Komponente.

    Axiome: Potentiell unendliche Menge grundlegender Sätze,die zu Beginn als wahr vorgegeben und in Beweisen oderDeduktionen benutzt werden.

  • Logik-27

    Definitionen-2

    Interpretation: Stellt die Beziehung zwischen Syntax derformalen Sprache und Semantik bezüglich der nichtlogischenSystemkomponente her. Syntaktisch korrekten Formeln wirddabei eine Aussage über ihren Wahrheitsgehalt zugeordnet(z.B. ein Wahrheitswert).

    Modell: Sind sowohl die System-Axiome als auch dieFormel φ innerhalb einer Interpretation A wahr, so ist A einModell für φ, in Zeichen A|=φ.