"Beweise als Programme 001.ps.gz" - читать интересную книгу автора

Beweise als Programme

Helmut Schwichtenberg

Mathematisches Institut der Ludwig-Maximilians-Universit"at M"unchen

Sommersemester 1996

Inhaltsverzeichnis 1 Einf"uhrung 2

1.1 Ein Existenzbeweis ohne Beispielsangabe : : : : : : : : : : : : : : : : : : : : : 2 1.2 Formale Systeme : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 1.3 Die Sprache der Logik erster Stufe : : : : : : : : : : : : : : : : : : : : : : : : : 3 1.4 Terme und Formeln : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7

2 Nat"urliche Herleitungen 10

2.1 Einf"uhrungs- und Beseitigungsregeln : : : : : : : : : : : : : : : : : : : : : : : : 10 2.2 Herleitungen als Terme : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 13 2.3 Klassische und intuitionistische Logik : : : : : : : : : : : : : : : : : : : : : : : 16

3 Arithmetik 20

3.1 Sprachen der Arithmetik : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 20 3.2 Arithmetische Herleitungen : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 21 3.3 Beispiel: Obere Schranke von + und \Delta : : : : : : : : : : : : : : : : : : : : : : : 23 3.4 Beispiel: Das Wall Street Problem : : : : : : : : : : : : : : : : : : : : : : : : : 25

4 Beweise als Programme 29

4.1 Existenz einer Normalform : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 29 4.2 Folgerungen aus der Normalisierung : : : : : : : : : : : : : : : : : : : : : : : : 34 4.3 Interpretation von Beweisen : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 36 4.4 Programmentwicklung durch Beweistransformation : : : : : : : : : : : : : : : : 38 4.5 Ausblick : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 40

Index 41 Literatur 44

1

Kapitel 1 Einf"uhrung

fEinfg 1.1 Ein Existenzbeweis ohne Beispielsangabe f

Sqrt2g

Untersuchungsgegenstand dieser Vorlesung sind mathematische Beweise. Bei diesen Untersuchungen werden einige interessante Aspekte von Beweisen zum Vorschein kommen. So ist es zum Beispiel m"oglich und sinnvoll, zwischen Existenzbeweisen zu unterscheiden, die das als existent nachgewiesene Objekt tats"achlich liefern, und solchen, die dies nicht tun. Als Beispiel betrachten wir die folgende Aussage.

Es gibt irrationale Zahlen a; b mit ab rational. Einen Beweis erh"alt man wie folgt durch Fallunterscheidung.