"Logische Systeme der Informatik 001.ps.gz" - читать интересную книгу автора

Theoretische Stammvorlesung Logische Systeme der Informatik

Helmut Thiele Universit"at Dortmund Fachbereich Informatik

Lehrstuhl I

Inhaltsverzeichnis 1 Einf"uhrung in die Pr"adikatenlogik der ersten Stufe 3

1.1 Die Syntax mehrsortiger Pr"adikatenkalk"ule der ersten Stufe (Syntax I) : : : : : : 3

1.1.1 Vorbemerkungen : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 1.1.2 Signaturen : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 4 1.1.3 Individuenvariablen und Terme : : : : : : : : : : : : : : : : : : : : : : : : 8 1.1.4 Ausdr"ucke : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 12 1.2 Interpretation der Terme und Ausdr"ucke (Semantik I) : : : : : : : : : : : : : : : 20

1.2.1 Algebraische Systeme : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 20 1.2.2 Zust"ande (Belegungen) der Individuenvariablen, Interpretation der Terme 23 1.2.3 Interpretation der Ausdr"ucke; die Erf"ullungsdefinition : : : : : : : : : : : 25 1.2.4 Allgemeing"ultigkeit und Erf"ullbarkeit von Ausdr"ucken : : : : : : : : : : : 27 1.2.5 Die semantische "Aquivalenz von Termen und Ausdr"ucken : : : : : : : : : 28 1.2.6 Pr"anexe Normalformen : : : : : : : : : : : : : : : : : : : : : : : : : : : : 38 1.2.7 Das Verhalten von Allgemeing"ultigkeit und Erf"ullbarkeit gegen"uber Bildung von Teilstrukturen sowie bei homomorphen bzw. isomorphen Abbildungen von Interpretationen : : : : : : : : : : : : : : : : : : : : : : : : : 49

1.3 Der Modellbegriff. Semantisches Folgern. Modell-basiertes Schliessen (Semantik II) 65

1.3.1 Der Modellbegriff : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 65 1.3.2 Das semantische Folgern : : : : : : : : : : : : : : : : : : : : : : : : : : : : 75 1.3.3 Zwei allgemeine Charakterisierungss"atze f"ur logische Operatoren : : : : : 85 1.3.4 Semantisches Folgern durch alleinige Verwendung minimaler Modelle : : : 89 1.4 Formales Ableiten und Beweisen. Regelbasiertes Schliessen (Syntax II) : : : : : : 99

1.4.1 Motivationen. Vorbemerkungen : : : : : : : : : : : : : : : : : : : : : : : : 99 1.4.2 Das verwendete logische Axiomensystem : : : : : : : : : : : : : : : : : : : 100 1.4.3 Der auf dem Modus Ponens allein beruhende Ableitungsbegriff : : : : : : 102 1.4.4 Ein pr"adikatenlogischer Ableitungsbegriff : : : : : : : : : : : : : : : : : : 110 1.4.5 Der Beweisbarkeitsbegriff : : : : : : : : : : : : : : : : : : : : : : : : : : : 115

1

2 INHALTSVERZEICHNIS

1.5 Eine syntaktische Charakterisierung des semantischen Folgerns. Der Hauptsatz

der Pr"adikatenlogik der ersten Stufe. Folgerungen aus dem Hauptsatz : : : : : : 118

1.5.1 Eine syntaktische Charakterisierung des semantischen Folgerns : : : : : : 118 1.5.2 Vorbereitungen f"ur den Beweis der semantischen Vollst"andigkeit : : : : : 124 1.5.3 Beendigung des Vollst"andigkeitsbeweises in den F"allen ohne bzw. mit Identit"at : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 137

1.5.4 Folgerungen aus dem Hauptsatz : : : : : : : : : : : : : : : : : : : : : : : 148 1.6 Das Entscheidungsproblem. L"osbare F"alle. Das Unentscheidbarkeitstheorem von

Church : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 151

1.6.1 Vorbemerkungen, "Uberblick : : : : : : : : : : : : : : : : : : : : : : : : : : 151 1.6.2 L"osbare F"alle : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 155 1.6.3 Das Unentscheidbarkeitstheorem von Church : : : : : : : : : : : : : : : 158

Literaturverzeichnis 165