WEBVTT

00:06.880 --> 00:09.560
Ja, ich begrüße Sie zur Vorlesung.

00:10.780 --> 00:19.520
Wir sind noch im Kapitel 3 und wollen heute noch ganz kurz eine

00:19.520 --> 00:24.960
Ergänzung machen hier zu dieser unten angegebenen Aussage.

00:25.960 --> 00:29.140
Wir haben es ja beim letzten Mal Ende von der letzten Stunde mit

00:29.140 --> 00:31.080
Berechnungsschemata auseinandergesetzt.

00:31.080 --> 00:37.420
Ich beachte Sie nochmal, dass wir hier sozusagen zwei Ausprägungen

00:37.420 --> 00:37.700
haben.

00:37.840 --> 00:42.980
Nämlich die eine, wenn wir an dieser Stelle hier oben Variablen oder

00:42.980 --> 00:44.960
Identifikatoren zu besetzen haben.

00:45.180 --> 00:48.080
Oder wenn wir Grundtherma haben, das war also auf einer der

00:48.080 --> 00:52.640
vorhergehenden Folien, dann war die Situation die, dass wir hier in

00:52.640 --> 00:56.520
diesen obersten Kästchen, die sozusagen die Blätter dieses Baumes

00:56.520 --> 01:00.760
sind, schon unmittelbar die Konstanten haben einfügen können.

01:01.320 --> 01:04.920
Jetzt kommen wir aber nochmal zu dem Satz hier unten.

01:06.280 --> 01:09.900
Das Berechnungsschema hat die Form eines zyklenfreien gerichteten

01:09.900 --> 01:14.060
Graphen, falls gewisse Identifikatoren mehrfach auftreten.

01:15.260 --> 01:18.780
Das muss man sich jetzt nochmal genauer analysieren.

01:18.780 --> 01:25.820
Die erste Sache ist die, dass wir eigentlich sinnvollerweise uns hier

01:25.820 --> 01:29.360
mit diesen Kanten eine Richtung geben.

01:30.240 --> 01:34.560
Also diese Berechnungsschemata sind eigentlich von der Semantik her

01:34.560 --> 01:38.320
geeignet, das als gerichtete Graphen anzusehen.

01:38.980 --> 01:41.980
Das heißt, Sie können hier überall eigentlich die Pfeile ergänzen.

01:43.200 --> 01:49.260
Zweite Sache, die wir feststellen, ist, dass wir es in dem Falle, wo

01:49.260 --> 01:53.080
wir keine mehrfachen Auftreten von Identifikatoren haben, also die

01:53.080 --> 01:58.040
Identifikatoren treten also maximal einmal auf, haben wir es mit

01:58.040 --> 01:58.860
Bäumen zu tun.

01:59.780 --> 02:03.140
Das ist also hier typischerweise, was wir an dem Beispiel sehen, ist

02:03.140 --> 02:03.600
ein Baum.

02:04.360 --> 02:08.260
Und jetzt machen wir einfach mal ein Beispiel, wo wir eben zeigen,

02:08.420 --> 02:15.560
dass das nicht mehr ein Baum darstellt, sobald die Identifikatoren

02:15.560 --> 02:17.440
mehr als einmal auftreten.

02:18.420 --> 02:20.960
Und das ist natürlich gegeben bei dem folgenden Beispiel.

02:22.020 --> 02:26.620
x-y mal x plus y, hier ist es sogar so, dass beide Identifikatoren, x

02:26.620 --> 02:28.480
und y, zweimal auftreten.

02:28.480 --> 02:32.980
Und dann schauen wir uns mal das Berechnungsformular an.

02:34.240 --> 02:40.740
Wir fangen immer oben an mit den Blättern, haben hier das x, hier das

02:40.740 --> 02:41.000
y.

02:41.200 --> 02:45.500
Wir wissen nicht, welche Werte diese annehmen, deswegen bleibt das

02:45.500 --> 02:46.040
erstmal leer.

02:47.000 --> 02:50.780
Und dann sieht eben das Berechnungsschema so aus, dass wir auf der

02:50.780 --> 02:55.060
einen Seite das Minus berechnen.

02:55.060 --> 03:00.440
Da brauchen wir x und y, hier schreiben wir dann wieder das Minus hin,

03:00.500 --> 03:01.380
das Minuszeichen.

03:01.980 --> 03:06.460
Und genauso müssen wir das Plus berechnen, das schreiben wir jetzt so

03:06.460 --> 03:07.880
hin, hier das Plus.

03:09.060 --> 03:12.840
Und dann kommen wir eben durch den letzten Schritt zu der

03:12.840 --> 03:13.060
Multiplikation.

03:13.900 --> 03:15.980
Also das ist so ein Berechnungsschema.

03:16.100 --> 03:20.120
Sie sehen, wir haben nicht mehr die Baumeigenschaft.

03:20.120 --> 03:23.840
Sie können sich also auch im Zusammenhang mit den Grafengrundlagen

03:23.840 --> 03:25.460
nochmal überlegen, nochmal wiederholen.

03:25.520 --> 03:30.140
Was war da ein Baum, was ist ein Zyklus in dem Zusammenhang.

03:30.340 --> 03:33.580
Und wir stellen eben fest, das ist zyklenfrei, das muss zyklenfrei

03:33.580 --> 03:33.920
sein.

03:34.540 --> 03:38.160
Und das ist genau die Aussage, die wir jetzt eben hier getroffen

03:38.160 --> 03:38.400
haben.

03:39.760 --> 03:43.080
Zyklenfreier gerichteter Graf, eben kein, das muss man auch eben

03:43.080 --> 03:46.220
dazuschreiben, das ist eigentlich die wesentliche Aussage.

03:46.220 --> 03:50.640
Wenn wir also ein mehrfaches Auftreten haben, haben wir eben keinen

03:50.640 --> 03:52.140
Baum.

03:53.280 --> 03:56.940
Das ist hier eigentlich die Aussage, die wir hier treffen.

03:58.700 --> 04:01.900
Gut, das war also nochmal ein Nachtrag zu den Rechenstrukturen.

04:03.120 --> 04:06.380
Und jetzt kommen wir also zu dem Abschnitt 3.3.

04:06.520 --> 04:09.680
Und da wollen wir uns mit Thermasetzungssystemen beschäftigen.

04:09.680 --> 04:15.820
Und ich habe ja schon am Anfang von diesem Kapitel so ein bisschen die

04:15.820 --> 04:19.540
Roadmap des gesamten Kapitels aufgezeigt.

04:20.260 --> 04:22.740
Die sah also folgendermaßen aus, die möchte ich noch ein bisschen

04:22.740 --> 04:24.920
ergänzen, deswegen möchte ich nochmal aufgreifen.

04:25.380 --> 04:29.840
Weil das eigentlich das Zentrale ist, um sozusagen zu verstehen, warum

04:29.840 --> 04:32.500
wir diese Themen hier bearbeiten und wie die zusammenhängen.

04:32.500 --> 04:41.000
Nämlich wir sind ja gestartet mit der Textersetzung und den

04:41.000 --> 04:42.500
Textersetzungssystemen.

04:45.080 --> 04:50.380
Dann haben wir auf der anderen Seite die Rechenstrukturen.

04:52.440 --> 04:54.760
Die Rechenstrukturen, mit denen haben wir uns jetzt gerade

04:54.760 --> 04:55.440
beschäftigt.

04:56.160 --> 05:01.180
Und eigentlich sieht es so aus, dass wir uns auf dieser Seite ganz

05:01.180 --> 05:04.400
stark mit Syntax beschäftigt haben.

05:07.380 --> 05:14.120
Weil wir eigentlich noch gar nicht so richtig mitbekommen, was die

05:14.120 --> 05:15.260
Texte denn darstellen.

05:15.340 --> 05:19.640
Wir haben dann das so mal am Ende von diesem Multiplikationsbeispiel

05:19.640 --> 05:20.320
aufgezeigt.

05:20.320 --> 05:24.000
Man kann diese Strichdarstellung, die könnte man als natürliche Zahlen

05:24.000 --> 05:24.740
interpretieren.

05:25.280 --> 05:29.160
Dafür sind aber diese Textersetzungssysteme überhaupt nicht geeignet,

05:29.260 --> 05:33.500
um sich hier mit semantischen Fragestellungen auseinanderzusetzen.

05:33.580 --> 05:37.120
Das ist eher zufällig, kann man sagen, wie man sich also hier dieser

05:37.120 --> 05:37.960
Sache nähert.

05:38.200 --> 05:44.440
Ganz im Gegensatz zu den Rechenstrukturen, da haben wir eigentlich das

05:44.440 --> 05:47.940
richtig schön schon mal in den Griff bekommen.

05:47.940 --> 05:50.020
Diese Frage, was heißt das denn?

05:50.640 --> 05:56.360
Welche mathematische Funktion weise ich denn diesen Rechenstrukturen

05:56.360 --> 06:00.000
zu den Operationen, zu den Termen, die hier drin vorkommen?

06:00.100 --> 06:05.780
Nämlich das ist genau das, was uns hier an der Stelle interessiert,

06:05.860 --> 06:07.060
nämlich die Terme.

06:07.140 --> 06:11.820
Aus Texten, die ursprünglich nur aus irgendwelchen Zeichen bestehen,

06:11.900 --> 06:14.340
aus einem Zeichenvorrat, werden Terme.

06:14.340 --> 06:18.760
Weil in den Termen kommen Operationen der Rechenstruktur vor und von

06:18.760 --> 06:21.940
denen wissen wir zumindest mal einiges, die Funktionalität.

06:22.040 --> 06:26.220
Wir wissen sogar eine Abbildung zu mathematischen Funktionen.

06:26.700 --> 06:30.280
Und das ist eigentlich jetzt genau die Sache, die wir hier

06:30.280 --> 06:34.020
zusammenbringen im Sinne der Termersetzung.

06:34.720 --> 06:38.740
Wir nehmen nämlich von oben sozusagen die Vorgabe des

06:38.740 --> 06:40.700
Textersetzungssystems.

06:40.700 --> 06:49.360
Das wird also ganz ähnlich sein, wie man einen Algorithmus definiert,

06:49.460 --> 06:54.480
wie die Regeln aussehen, wie man mit diesen Regeln sukzessive arbeitet

06:54.480 --> 06:56.920
und von einem Term in den nächsten kommt.

06:57.240 --> 07:00.920
Das bleibt also von dieser Seite her, aber was wir jetzt eben dazu

07:00.920 --> 07:04.880
bekommen, und das ist das Interessante, das ist die Semantik.

07:04.880 --> 07:11.640
Wir können sehr viel mehr über diese Termherleitung und die Schritte

07:11.640 --> 07:15.460
von einem Term in den nächsten, können wir sehr viel mehr Aussagen

07:15.460 --> 07:16.000
darüber treffen.

07:16.080 --> 07:22.840
Das ist also nochmal hier diese beiden Aspekte Rechenstrukturen und

07:22.840 --> 07:25.220
Textersetzung gegenübergestellt.

07:25.220 --> 07:28.800
Und was wir hier dann noch bekommen, auf dieser Seite, wenn wir hier

07:28.800 --> 07:30.540
Syntax und Semantik uns betrachten.

07:31.000 --> 07:35.400
Und das ist schon mal ein Vorgriff auf das, was wir dann im letzten

07:35.400 --> 07:36.640
Abschnitt hier behandeln.

07:37.200 --> 07:40.680
Das führt letztendlich zu dem Bereich der Logik.

07:42.140 --> 07:44.880
Das werden wir also in der Logik nochmal vertiefen.

07:45.460 --> 07:51.660
Nämlich, das ist sozusagen die mathematische Theorie, wie man mit

07:51.660 --> 07:54.520
Syntax und Semantik vernünftig arbeiten kann.

07:54.520 --> 08:00.120
Und diese beiden Themen, Termersetzung, Logik, die schalten wir dann

08:00.120 --> 08:00.540
zusammen.

08:00.960 --> 08:02.520
Das machen wir aber dann nach Weihnachten.

08:02.980 --> 08:07.000
Das führt uns dann nämlich letztendlich zu dem Lambda-Kalkül.

08:08.040 --> 08:09.260
Da brauchen wir also Logik.

08:10.080 --> 08:12.700
Lambda-Kalkül ist ein Termersetzungssystem.

08:14.380 --> 08:19.020
Und wir brauchen noch Logikgrundlagen, um dieses Lambda-Kalkül zu

08:19.020 --> 08:19.420
verstehen.

08:19.420 --> 08:25.240
Und das führt uns dann letztendlich zu der funktionalen

08:25.240 --> 08:25.920
Programmierung.

08:29.200 --> 08:31.080
Und das machen wir am Beispiel von Gopher.

08:31.700 --> 08:37.020
Also eine Programmiersprache, in der man auch rein auf der Basis vom

08:37.020 --> 08:38.560
Lambda -Kalkül programmieren kann.

08:38.660 --> 08:40.400
Wo man sich allerdings noch ein bisschen Richtung höhere

08:40.400 --> 08:43.000
Programmiersprachen auch behelfen kann.

08:43.140 --> 08:46.420
Damit es nicht ganz primitiv wird, diese Art der Programmierung.

08:46.520 --> 08:47.480
Oder mathematisch wird.

08:48.560 --> 08:52.000
Gut, das ist also sozusagen nochmal die ergänzte Roadmap, die wir hier

08:52.000 --> 08:52.300
haben.

08:52.740 --> 08:57.820
Und jetzt kommen wir zu den Algorithmen als Termersetzungssystemen.

08:59.200 --> 09:02.240
Wir haben, wie gesagt, die Textersetzungssysteme.

09:02.340 --> 09:06.340
Das ist unsere Vorgabe, mit denen fangen wir an.

09:06.420 --> 09:11.080
Das ist sozusagen die Basis, mit denen wir Algorithmen zumindest schon

09:11.080 --> 09:12.040
mal beschreiben können.

09:12.040 --> 09:17.240
Und jetzt kommen diese Terme hier dazu.

09:17.960 --> 09:22.760
Und wir werden sehen, dass wir uns sehr viel leichter tun werden,

09:23.260 --> 09:25.500
solche Systeme aufzubauen.

09:25.600 --> 09:27.920
Das ist immer noch nicht der Weisheit letzter Schluss zum

09:27.920 --> 09:28.500
Programmieren.

09:28.660 --> 09:30.040
Aber es ist schon mal eine Verbesserung.

09:31.100 --> 09:36.000
Und was wir insbesondere hier erreichen, ist, dass wir diese

09:36.000 --> 09:37.400
Signaturen mit ins Spiel bringen.

09:37.400 --> 09:41.160
Also die Algebren hier mit ins Spiel bringen, algebraische Strukturen

09:41.160 --> 09:44.960
mit einsetzen können, um solche Algorithmen beschreiben zu können.

09:45.860 --> 09:51.220
Und was wir dann an der Stelle eben erreichen, ist, dass wir diese

09:51.220 --> 09:55.760
Interpretationen mit in die Waagschale werfen.

09:56.300 --> 10:00.880
Wir nehmen also den Anteil von der Rechenstruktur.

10:00.880 --> 10:07.480
Diese Interpretationen, die ich hier angegeben habe, die sind genau an

10:07.480 --> 10:09.040
dieser Stelle hier gegeben.

10:09.140 --> 10:09.900
Das ist Semantik.

10:11.000 --> 10:14.800
Das sind genau die Interpretationen, die wir hier eingeführt haben.

10:15.460 --> 10:18.880
Die Interpretationen i, das ist ja genau die Semantik.

10:20.360 --> 10:21.460
Interpretationen i soll das heißen.

10:21.500 --> 10:22.860
Das ist vielleicht ein bisschen schlecht gelungen.

10:22.860 --> 10:25.380
Schreibe ich es nochmal so hin.

10:25.480 --> 10:31.800
Also diese Abbildungsfunktion, die aus einem Symbol eine mathematische

10:31.800 --> 10:34.900
Operation zuordnet.

10:35.060 --> 10:39.580
Das ist genau das, was wir hier jetzt an der Stelle eben verwenden.

10:40.220 --> 10:45.720
Wir können die Interpretationen über eine Rechenstruktur hier angeben.

10:45.720 --> 10:50.780
Und was wir letztendlich dann erreichen, ist, dass wir schon mal über

10:50.780 --> 10:54.020
die semantische Äquivalenz eine Aussage treffen können.

10:54.100 --> 10:58.880
Wir können nämlich Äquivalenzklassen bilden, aufgrund von gleicher

10:58.880 --> 11:00.080
semantischer Bedeutung.

11:00.560 --> 11:05.800
Und das führt letztendlich dazu, dass diese Regeln hier, dass wir von

11:05.800 --> 11:08.600
denen fordern, dass die Semantik erhalten sind.

11:09.600 --> 11:12.580
Die sollen Semantik erhalten sein.

11:15.000 --> 11:18.120
Das heißt, man soll also hier nicht irgendwie aus einem Term

11:18.120 --> 11:21.800
irgendeinen beliebigen anderen Term bilden können oder ableiten

11:21.800 --> 11:26.140
können, sondern die Interpretationsfunktion soll für diese Terme

11:26.140 --> 11:28.500
letztendlich das gleiche Ergebnis liefern.

11:28.500 --> 11:32.680
Das ist also, wie wir Semantik erhaltende Regeln definieren können.

11:32.820 --> 11:37.620
Also auf der Semantikseite unter Zuhilfenahme dieser

11:37.620 --> 11:38.900
Interpretationsfunktion.

11:39.380 --> 11:44.480
Was wir hier dann brauchen oder was wir suchen, sind

11:44.480 --> 11:50.740
Termersetzungsregeln, die diese Semantik Erhaltung, diese semantische

11:50.740 --> 11:53.000
Äquivalenz auf Termen ermöglicht.

11:53.000 --> 11:58.200
Und wir nutzen hier selbstverständlich die spezielle Struktur der

11:58.200 --> 11:59.420
Terme aus.

11:59.700 --> 12:04.220
Also die ist ja genau durch diesen induktiven Termaufbau gegeben.

12:04.960 --> 12:11.500
Und durch die Axiome, die in der Rechenstruktur oder in der Algebra

12:11.500 --> 12:14.660
enthalten ist, das wird hier sozusagen mit einbezogen.

12:15.180 --> 12:17.140
Das ist also die Überlegung.

12:17.140 --> 12:20.880
Und jetzt geht es zu den Termersetzungsregeln.

12:22.100 --> 12:27.620
Und hier auch wieder als Vorabinformation, wir müssen uns mit den

12:27.620 --> 12:31.380
Identifikatoren jetzt dann auch wieder etwas auseinandersetzen an der

12:31.380 --> 12:31.660
Stelle.

12:31.800 --> 12:37.140
Das wird also eine zweistufige Angelegenheit.

12:38.320 --> 12:42.080
Das werde ich Ihnen also gleich zeigen, wenn wir eben von den Regeln

12:42.080 --> 12:43.840
reden und von Instanzen von Regeln.

12:43.840 --> 12:48.800
Gehen wir mal von den Termersetzungsregeln aus.

12:49.940 --> 12:53.420
Das ist wieder ein Paar, das ist eine linke und eine rechte Seite,

12:53.560 --> 12:56.940
also der Term, von dem wir ausgehen und der Term, den wir eben

12:56.940 --> 12:57.480
ableiten.

12:58.560 --> 13:01.880
Wir haben wieder hier diese Schreibweise, die wir also von den

13:01.880 --> 13:06.340
Textersetzungsregeln kennen, von Textersetzungssystemen kennen.

13:06.760 --> 13:08.100
Also nehmen wir auch wieder den Pfeil.

13:08.780 --> 13:13.360
Und jetzt müssen wir hier an der Stelle schon eine Sache

13:13.360 --> 13:17.080
berücksichtigen, nämlich wir haben ja jetzt an der Stelle eine

13:17.080 --> 13:18.540
Signatur.

13:20.100 --> 13:26.560
Und wir müssen hier die Sorte miteinbeziehen, das ist wie Typen in

13:26.560 --> 13:27.560
Programmiersprachen.

13:27.700 --> 13:33.060
Ich habe das ja schon mehrfach, diese Analogie, Ihnen auf den Weg

13:33.060 --> 13:33.440
gegeben.

13:33.440 --> 13:38.080
Wir müssen hier sozusagen gleiche Typen von Termen haben, gleiche

13:38.080 --> 13:38.920
Sorten.

13:39.060 --> 13:43.040
Und da steht genau in der Signatur drin, das heißt hier sehen Sie,

13:43.160 --> 13:48.880
dass Sie also immer auf der einen Seite diese Textersetzung oder jetzt

13:48.880 --> 13:51.520
in dem Fall Termersetzung haben und Sie müssen immer die Signatur noch

13:51.520 --> 13:55.060
mit berücksichtigen, also das, was sozusagen von der Rechenstruktur,

13:55.180 --> 13:56.180
von der Algebra kommt.

13:56.180 --> 14:00.340
Und jetzt haben wir an der Stelle freie Identifikatoren.

14:02.020 --> 14:06.520
Der Begriff frei, der wird hier schon mal vorab verwendet, haben wir

14:06.520 --> 14:08.580
schon an einer anderen Stelle auch vorab verwendet.

14:09.120 --> 14:13.260
Das muss man dann im Zusammenhang mit Logik sehen, nämlich also frei

14:13.260 --> 14:15.280
im Sinne von wir können da was einsetzen.

14:15.580 --> 14:19.040
Das ist nicht gebunden, wir können da also Ersetzungen vornehmen, das

14:19.040 --> 14:20.580
soll hier an der Stelle frei bedeuten.

14:20.580 --> 14:26.140
Und da sind halt Identifikatoren enthalten und die sind aus der Menge

14:26.140 --> 14:29.460
X, die Menge X haben wir ja auch schon früher mal eingeführt von

14:29.460 --> 14:33.640
irgendwelchen Identifikatoren und die treten hier frei auf, sind freie

14:33.640 --> 14:35.060
Vorkommnisse, wie wir auch sagen.

14:36.400 --> 14:43.120
Und diese Identifikatoren, zu denen gibt es auch eine Forderung, die

14:43.120 --> 14:44.580
sieht also folgendermaßen aus.

14:44.580 --> 14:52.820
Wir fordern, dass wir bei der Herleitung von Termen, also wenn wir von

14:52.820 --> 14:59.020
einem Term T zu einem Term R kommen im Termersetzungssystem, dass wir

14:59.020 --> 15:01.520
nicht mehr Identifikatoren auf der rechten Seite bekommen.

15:01.860 --> 15:05.300
Oder andersherum ausgedrückt, wie es auf der Folie hier steht, wir

15:05.300 --> 15:10.300
fordern, dass die Identifikatoren, die im Term R auftreten, müssen

15:10.300 --> 15:11.500
auch im Term T auftreten.

15:11.500 --> 15:14.540
Das heißt, wir können da nicht einfach neue Identifikatoren dazu

15:14.540 --> 15:15.020
zaubern.

15:15.640 --> 15:20.560
Die müssen also aus dem Satz der Identifikatoren, die in R in T

15:20.560 --> 15:26.160
auftreten, müssen die in R auch enthalten sein.

15:27.040 --> 15:30.280
Das ist eine Anforderung, die nicht jedes Termersetzungssystem

15:30.280 --> 15:35.700
notwendigerweise enthält, aber das macht das Ganze sicherlich

15:35.700 --> 15:38.860
einfacher nochmal und macht auch Sinn, diese Forderung

15:38.860 --> 15:39.860
aufrechtzuerhalten.

15:39.860 --> 15:46.660
So, und jetzt kommen wir zu diesem Schritt von der Regel zu einer

15:46.660 --> 15:47.780
Instanz der Regel.

15:48.420 --> 15:53.340
Das ist eine Sache, die wir eben dadurch hier reinbekommen, dass wir

15:53.340 --> 15:58.280
freie Identifikatoren in solchen Termen haben.

15:59.120 --> 16:04.080
Und eigentlich ist eine Termersetzungsregel, dahinter stecken ganz

16:04.080 --> 16:07.340
viele Instanzen von solchen Regeln.

16:07.820 --> 16:10.700
Und das können wir mal an einem Beispiel, kann ich das mal

16:10.700 --> 16:12.020
verdeutlichen.

16:13.260 --> 16:17.260
Wir gehen mal aus, und dann verstehen Sie auch diese Schreibweise ohne

16:17.260 --> 16:17.440
Schwierigkeiten.

16:17.980 --> 16:21.020
Wir gehen mal von einer folgenden Regel aus, also eine

16:21.020 --> 16:22.700
Termersetzungsregel ist das natürlich.

16:22.700 --> 16:34.120
Von folgender Regel, das Predecessor von Successor von X, und das ist

16:34.120 --> 16:42.000
eben dieser, dieses X ist der frei vorkommende Identifikator in dem T,

16:43.100 --> 16:45.600
und der geht über nach X.

16:45.600 --> 16:51.180
Das ist dieser Term, Predecessor von Successor von X, der geht über

16:51.180 --> 16:53.500
nach X.

16:54.140 --> 17:00.620
Und jetzt haben wir Instanzen, die sich jetzt einfach dadurch ergeben,

17:01.320 --> 17:04.180
dass wir das X besetzen.

17:04.180 --> 17:15.740
Also eine Instanz könnte sein, Predecessor von Successor von 0, geht

17:15.740 --> 17:16.580
über nach 0.

17:17.820 --> 17:21.200
Oder eine andere Instanz könnte sein, das ist also ein erstes

17:21.200 --> 17:27.220
Beispiel, eine andere Instanz könnte sein, Predecessor von Successor

17:27.220 --> 17:38.840
von Y, da brauchen wir drei schließende Klammern, geht über zu

17:38.840 --> 17:42.460
Successor von Y.

17:44.860 --> 17:48.400
So, und da haben wir, sehen Sie, das sind nur Beispiele.

17:49.000 --> 17:53.080
Was wir hier letztendlich gemacht haben ist, das schreibe ich jetzt

17:53.080 --> 17:59.180
nochmal formal hin, wenn wir jetzt sagen, das ist eine Regel, die von

17:59.180 --> 18:08.160
T, wenn das T nach R ist, in der allgemeinen Schreibweise, also T ist

18:08.160 --> 18:13.960
dieser Teil hier und das R besteht nur aus dem X, dann haben wir hier

18:13.960 --> 18:27.700
gebildet, T setze 0 für X ein und dann entsprechend R setze 0 für X

18:27.700 --> 18:28.020
ein.

18:29.020 --> 18:35.840
Und genauso hier haben wir eine andere Ersetzung durchgeführt, nämlich

18:35.840 --> 18:45.480
wir haben Successor von Y für X eingesetzt und auf der rechten Seite

18:45.480 --> 18:52.080
haben wir ebenfalls Successor von Y für X eingesetzt.

18:52.080 --> 18:57.860
So, das sind jetzt zwei Beispiele, zwei Instanzen und Sie können sich

18:57.860 --> 19:01.440
vorstellen, dass Sie eben hier beliebig viele abzählbar und endlich

19:01.440 --> 19:04.340
viele Instanzen sich hinter dieser Regel verbirgt.

19:05.220 --> 19:09.140
Der Grund ist der, dass wir hier eben freie Identifikatoren in der

19:09.140 --> 19:13.060
Regel zulassen, das ist hier an der Stelle dieses X gewesen, es können

19:13.060 --> 19:17.440
auch mehr sein, es ist nicht begrenzt.

19:18.280 --> 19:22.300
Wir haben nur diese Begrenzung, dass bitte hier auf der rechten Seite

19:22.300 --> 19:26.020
keine neuen Identifikatoren auftreten, die nicht auf der linken

19:26.020 --> 19:27.380
auftreten, das war diese Forderung.

19:27.940 --> 19:32.860
Und jetzt können Sie hier an der Stelle eben verschiedenste Terme

19:32.860 --> 19:38.320
einsetzen und hier waren eben zwei Beispiele, einmal der Term 0 und

19:38.320 --> 19:45.200
einmal der Term Successor von Y und das ist dann eine Beobachtung, die

19:45.200 --> 19:50.980
man hier an der Stelle machen kann, dass man also hier auch wieder

19:50.980 --> 19:55.120
Identifikatoren, neue Identifikatoren mit ins Spiel bringen kann.

19:56.120 --> 19:59.060
Das heißt also, was Sie hier ansehen ist, dass Sie durch die

19:59.060 --> 20:03.120
Instanzen, die Sie hier bilden, dass Sie dadurch nicht etwa die

20:03.120 --> 20:05.680
Identifikatoren versuchen wegzubekommen.

20:06.300 --> 20:11.020
Also erstens wird nicht ausgesagt, dass man jetzt alle Identifikatoren

20:11.020 --> 20:17.940
ersetzen muss, das bleibt einem selbst zu überlassen, wie viele von

20:17.940 --> 20:22.420
diesen Identifikatoren Sie ersetzen wollen und zum zweiten können Sie

20:22.420 --> 20:26.020
also neue Identifikatoren mit ins Spiel bringen, indem Sie eben in

20:26.020 --> 20:29.020
diesen Termen, die Sie hier einsetzen, auch wieder ganz neue

20:29.020 --> 20:32.100
Identifikatoren mit übernehmen.

20:32.100 --> 20:36.120
Das ist also wichtig, dass Sie das erkennen, dass man hier diese

20:36.120 --> 20:41.080
Instanzenbildung nicht etwa macht, um sich von diesen Identifikatoren

20:41.080 --> 20:43.900
zu befreien, das hat damit nichts zu tun, das ist nur eine

20:43.900 --> 20:47.660
Variantenbildung, die Sie hier eben vornehmen können, auf der Basis

20:47.660 --> 20:53.400
einer Termersetzungsregel hier entsprechende Instanzen zu bilden.

20:54.640 --> 20:57.560
Formal sieht das also dann so aus, wir haben wieder diese

20:57.560 --> 21:05.020
Schreibweise, dass wir hier mehrere von den Identifikatoren simultan

21:05.020 --> 21:07.820
substituieren können, das ist ja hier die Schreibweise für

21:07.820 --> 21:12.640
Substitution, und das heißt nichts anderes, als dass wir an der Stelle

21:12.640 --> 21:21.200
diese Identifikatoren raussuchen, in dem Term, in dem T, und gegen die

21:21.200 --> 21:24.000
XI ersetzen, und das eben simultan.

21:24.200 --> 21:29.280
Das heißt also, Sie können mehrere dieser Identifikatoren gleichzeitig

21:29.280 --> 21:34.120
ersetzen, hier steht nicht drin, das möchte ich nochmal deutlich

21:34.120 --> 21:37.320
machen, hier steht gewisse Identifikatoren, hier steht nicht alle

21:37.320 --> 21:41.800
Identifikatoren, die in T auftreten, und insbesondere ist hier auch

21:41.800 --> 21:50.820
noch zu sehen gewesen, dass durch diese TIs, die TIs können, ich sag

21:50.820 --> 22:00.200
mal, neue Identifikatoren enthalten.

22:03.340 --> 22:08.740
Das ist also hier die Konstruktionsprinzipien, die Sie aus dem

22:08.740 --> 22:13.100
Beispiel heraus auch nochmal nachvollziehen können, und das heißt, wir

22:13.100 --> 22:21.020
haben also hier von einer Thamersetzungsregel viele Instanzen, die wir

22:21.020 --> 22:21.880
daraus bilden können.

22:22.100 --> 22:26.140
Mit diesen Instanzen arbeiten wir jetzt auch dann im nächsten Schritt,

22:27.060 --> 22:32.980
das ist jetzt diese Folie, wir wenden jetzt eine Regel an, wie geht

22:32.980 --> 22:33.260
das?

22:34.360 --> 22:40.060
Man geht eben aus von einem Term C, das ist jetzt schon wieder neuer

22:40.060 --> 22:46.900
Term, und was man bildet ist, dass man also hier an der Stelle jetzt

22:46.900 --> 22:53.220
einen Identifikator sucht, den nennen wir auch wieder X, können wir

22:53.220 --> 23:02.080
auch anders nennen, und wir ersetzen dieses X, wir setzen einmal das T

23:02.080 --> 23:06.500
für das X ein und setzen dann das R für das X ein.

23:08.680 --> 23:12.580
Und an der Stelle möchte ich Sie ganz explizit darauf aufmerksam

23:12.580 --> 23:17.380
machen, dass wir hier nicht von einer allgemeinen Thamersetzungsregel

23:17.380 --> 23:24.820
ausgehen, sondern an der Stelle ist T Pfeil R eine Instanz der Regel.

23:25.100 --> 23:29.120
Das heißt, wir haben schon diese Ersetzung durchgeführt, diese

23:29.120 --> 23:29.820
Substitution.

23:30.800 --> 23:37.520
Das macht an der Stelle, ist das formal eigentlich gar nicht so

23:37.520 --> 23:42.000
relevant, nämlich Sie können sich hier auch überlegen, dass Sie an

23:42.000 --> 23:46.440
dieser Stelle gar keine Substitution durchführen.

23:46.440 --> 23:49.140
Wer sagt Ihnen denn, dass Sie hier eine Substitution durchführen

23:49.140 --> 23:49.400
müssen?

23:50.260 --> 23:56.420
Sie können sozusagen auch die Thamersetzungsregel als eine Instanz

23:56.420 --> 23:57.940
derselbigen ansehen.

23:58.280 --> 23:59.800
Das ist ja nicht verboten an der Stelle.

24:00.320 --> 24:04.880
Insofern ist das also jetzt hier mal formal keine schwerwiegende

24:04.880 --> 24:05.340
Einschränkung.

24:05.460 --> 24:07.100
Vielmehr, Sie kriegen hier diese Vielfalt.

24:07.820 --> 24:12.940
Hier kommt letztendlich die Vielfalt der Regelanwendungen, die kommt

24:12.940 --> 24:14.020
hier eigentlich zum Tragen.

24:14.020 --> 24:18.580
Dass Sie aus einer Thamersetzungsregel eine Vielzahl von Instanzen

24:18.580 --> 24:19.780
herausbekommen.

24:21.460 --> 24:26.040
Und C ist jetzt ein Term, der Identifikator X muss wieder frei

24:26.040 --> 24:26.540
vorkommen.

24:27.500 --> 24:29.880
Da haben wir kein Problem mit, weil wir noch gar keine Möglichkeiten

24:29.880 --> 24:32.720
haben bisher, den zu binden.

24:32.900 --> 24:35.520
Da brauchen wir nämlich Quantoren, mit denen haben wir ja bisher noch

24:35.520 --> 24:36.600
gar nichts zu tun.

24:37.000 --> 24:39.420
Insofern kommen unsere Identifikatoren alle frei vor.

24:39.420 --> 24:44.960
T heißt Redex und dieses Auftreten von X in C heißt Anwendungsstelle.

24:46.460 --> 24:49.520
Das können Sie auch eigentlich, brauchen Sie sich nicht merken.

24:50.220 --> 24:53.060
Das werden wir von Ihnen nicht abverlangen, diese Begriffe.

24:54.160 --> 24:54.880
So, Beispiel.

24:55.780 --> 25:01.060
Jetzt können wir wieder unser gerade schon angefangenes Beispiel hier

25:01.060 --> 25:02.160
übernehmen.

25:03.100 --> 25:07.940
Wir haben diese Regelinstanz ja hier produziert.

25:09.100 --> 25:12.340
Erinnern Sie sich dann einfach nochmal, wie wir dazu gekommen sind mit

25:12.340 --> 25:13.880
dieser Substitution von dem Zero.

25:14.240 --> 25:18.280
Das ist halt nur eine von vielen Instanzen, die wir hier bilden.

25:18.800 --> 25:23.020
Und wir haben eben diesen Term C, das ist jetzt hier Successor von

25:23.020 --> 25:24.040
Successor von X.

25:24.040 --> 25:29.200
Und jetzt können wir, kann man schon sagen, ganz mechanisch diese

25:29.200 --> 25:33.220
Regelinstanz auf den Term anwenden.

25:33.780 --> 25:37.280
Wir suchen uns also hier, was wir letztendlich bilden, ist genau diese

25:37.280 --> 25:40.640
hier oben angegebene Substitution.

25:41.500 --> 25:46.360
Wir suchen das Auftreten, also die Anwendungsstelle, wie es hier

25:46.360 --> 25:49.920
heißt, von dem X in den Term C raus.

25:49.920 --> 25:53.120
Das ist hier, das an dieser Stelle.

25:53.880 --> 25:59.440
Und da setzen wir jetzt entsprechend auf der einen Seite das T ein.

25:59.780 --> 26:04.600
Das heißt, was wir hier letztendlich bilden, ist der, ich schreibe es

26:04.600 --> 26:12.740
mal ausführlich hin, Successor von Successor von X.

26:15.590 --> 26:17.900
Und hier kommt jetzt die Substitution.

26:19.140 --> 26:26.320
Und zwar, das ist der Predecessor von dem Successor von Zero.

26:29.780 --> 26:32.860
Und den setzen wir für X ein.

26:33.500 --> 26:40.140
Also solche Schreibweisen sollten Sie schon sich so weit

26:40.140 --> 26:44.240
eintrainieren, dass das Ihnen keine Probleme macht, mit diesen

26:44.240 --> 26:45.620
Substitutionen umzugehen.

26:46.340 --> 26:50.300
Sowohl auf dieser Ebene der Thermalsetzungssysteme wird das von Ihnen

26:50.300 --> 26:55.560
abverlangt, als auch dann insbesondere im Lambda-Kalkül, wo wir also

26:55.560 --> 26:59.100
hin zu der Programmierung dann kommen, wo wir also auf der Basis genau

26:59.100 --> 27:03.300
von diesen Substitutionen, Programmierungen, Algorithmen hinschreiben.

27:03.660 --> 27:06.940
Und da müssen Sie mit diesen Konstruktionen gut umgehen können.

27:07.240 --> 27:10.000
Das ist aber soweit sehr schnell einsehbar.

27:10.100 --> 27:13.640
Man muss sich nicht nur mit diesen Terminologien, mit Notationen ein

27:13.640 --> 27:14.420
wenig beschäftigen.

27:14.780 --> 27:18.300
Dann kommt man da also sehr schnell auf die Wirkungsweise raus.

27:18.980 --> 27:21.960
So, und jetzt kommen wir zu dem Übergang, zu dem

27:21.960 --> 27:23.760
Thermalsetzungsalgorithmus.

27:23.760 --> 27:26.560
Und das habe ich schon Ihnen anfangs gesagt.

27:26.920 --> 27:30.300
Da können wir also die Dinge, die wir aus den Textversetzungssystemen

27:30.300 --> 27:33.620
kennen, die können wir hier ohne Schwierigkeiten adaptieren.

27:34.300 --> 27:36.740
Und was ist also ein Thermalsetzungssystem?

27:37.080 --> 27:40.240
Immer hier bitte berücksichtigen, das ist neu.

27:40.300 --> 27:44.100
Wir haben hier eine Signatur Sigma, weil wir diese Rechenstrukturen

27:44.100 --> 27:45.680
hier mit einbeziehen.

27:46.220 --> 27:51.200
Aber ansonsten ist das eben eine im Allgemeinen endliche Menge R von

27:51.200 --> 27:52.320
Thermalsetzungsregeln.

27:54.160 --> 27:58.840
Im allgemeinen Fall, also im pragmatischen, sinnvollen Fall können Sie

27:58.840 --> 28:04.160
hier auch sagen, wir wollen ja irgendwie mit den Systemen

28:04.160 --> 28:08.920
programmieren und da wollen wir also auch eine endliche Menge von

28:08.920 --> 28:11.460
Operationen sozusagen haben, die wir anwenden.

28:11.820 --> 28:15.140
Bei den Instanzen, da kommen wir ja eh schon zu den abzählbar

28:15.140 --> 28:18.220
unendlich vielen, dann sollen wenigstens die Thermalsetzungsregeln

28:18.220 --> 28:19.280
endlich sein.

28:19.280 --> 28:22.980
Also wir haben nichts davon, wenn das unendlich viele wären.

28:23.140 --> 28:27.540
Das ist deswegen diese im Allgemeinen endliche Anzahl von

28:27.540 --> 28:28.480
Thermalsetzungsregeln.

28:29.080 --> 28:34.340
So, die Berechnung, die können Sie eigentlich eins zu eins aus den

28:34.340 --> 28:36.000
Textversetzungssystemen übernehmen.

28:36.080 --> 28:41.140
Wir haben auch wieder eine Berechnungsfolge und wir haben hier die

28:41.140 --> 28:47.120
Eingabe, mit dem wir starten, wir haben hier die Ausgabe und wir

28:47.120 --> 28:51.620
kommen letztendlich von einem Term zum nächsten, indem wir die

28:51.620 --> 28:56.580
verschiedenen Thermalsetzungsregeln anwenden, beziehungsweise die

28:56.580 --> 29:04.200
Instanzen anwenden und Ti nach Ti plus 1 ist Anwendung einer Regel.

29:05.500 --> 29:12.400
Hier sollte man vielleicht hinschreiben, Regel Instanz aus dem

29:12.400 --> 29:17.340
Thermalsetzungssystem R und wir haben wieder diese Eigenschaft des

29:17.340 --> 29:27.440
Terminalseins, indem wir eben sagen, wir finden kein Term R mehr,

29:27.840 --> 29:28.940
sodass Ti nach R gilt.

29:29.040 --> 29:34.660
Das heißt, wir finden keine Regel mehr, die uns ermöglicht, Ti in R zu

29:34.660 --> 29:35.220
überführen.

29:36.300 --> 29:39.960
Genauso haben wir Normalformen, die haben wir auch schon kennengelernt

29:39.960 --> 29:46.580
und die definieren wir über diese Eigenschaft des Terminalseins in der

29:46.580 --> 29:53.160
Form, dass wir hier sagen, dass wir von terminalen Grundthermen

29:53.160 --> 29:55.160
ausgehen zu einem Thermalsetzungssystem.

29:55.620 --> 29:59.100
Ich kann da relativ schnell das behandeln, weil wir das schon an

29:59.100 --> 30:03.380
anderer Stelle bei den Textversetzungssystemen sehr genau behandelt

30:03.380 --> 30:03.700
haben.

30:03.700 --> 30:11.800
Und wir sagen jetzt, dass wir jedem Term versuchen, einen solchen

30:11.800 --> 30:14.000
terminalen Grundtherm zuzuordnen.

30:14.100 --> 30:19.680
Wir haben nur folgendes Problem, zwei Probleme oder zwei

30:19.680 --> 30:24.340
Eigenschaften, die unschön sind, die wir aber hier klar erkennen

30:24.340 --> 30:24.660
müssen.

30:24.660 --> 30:28.520
Wir haben also Eigenschaften der Normalform, die können wir mal hier

30:28.520 --> 30:29.140
aufschreiben.

30:30.080 --> 30:34.660
Eigenschaften der Normalform.

30:37.920 --> 30:44.320
Die erste ist, dass sie nicht vollständig ist.

30:45.800 --> 30:47.240
Nicht vollständig?

30:49.420 --> 30:55.220
Das würden wir schon gerne haben, aber warum ist das nicht

30:55.220 --> 30:55.940
vollständig?

30:55.940 --> 31:13.860
Weil die Therme für die nur nichtterminierende

31:18.300 --> 31:27.480
Berechnungen existieren,

31:31.340 --> 31:32.720
keine Normalform haben.

31:38.210 --> 31:43.290
Das heißt also, wir können nicht jedem Term so etwas zuordnen.

31:43.550 --> 31:51.290
Wichtig ist, wir erben hier diese ganzen unschönen Eigenschaften der

31:51.290 --> 31:52.110
Nichtterminierung.

31:52.390 --> 31:53.750
Da müssen wir uns also auch ein paar Gedanken machen.

31:54.450 --> 31:58.090
Das wird ja durch die Thermersetzung, dadurch, dass wir jetzt

31:58.090 --> 32:01.870
Algebren, Rechenstrukturen mit einbeziehen, wird das ja nicht besser,

32:02.410 --> 32:03.790
diese Eigenschaft bleibt uns erhalten.

32:04.610 --> 32:09.650
Und das zweite ist, diese Zuordnung ist auch nicht eindeutig, das

32:09.650 --> 32:13.570
hatten wir schon ausführlicher bei den Textversetzungssystemen

32:13.570 --> 32:39.930
behandelt, weil für gewisse Therme Berechnungen mit unterschiedlichen

32:42.360 --> 32:47.420
Resultaten existieren,

32:52.160 --> 32:53.120
existieren können.

32:57.070 --> 33:03.090
So, da haben wir also auch das Problem, dass die Sache nicht zwingend

33:03.090 --> 33:04.850
deterministisch ist.

33:05.390 --> 33:09.830
Wir können also auch wieder hier unterschiedliche Resultate,

33:09.950 --> 33:13.390
unterschiedliche Wege beschreiten in der Berechnung, in der Ableitung.

33:13.850 --> 33:18.990
Das sind also Eigenschaften, die wir einfach zur Kenntnis nehmen, die

33:18.990 --> 33:23.630
sich ergeben aufgrund dieser Eigenschaften, die wir bei

33:23.630 --> 33:24.870
Thermersetzungssystemen haben.

33:24.970 --> 33:33.170
Den Algorithmus schauen wir uns jetzt auch nochmal im Detail an.

33:36.690 --> 33:39.570
Eigentlich kann man von den Textversetzungsalgorithmen abschreiben,

33:40.310 --> 33:44.810
was sich also tatsächlich hier bei den Thermersetzungssystemen von der

33:44.810 --> 33:48.010
mechanischen Seite ergibt.

33:48.010 --> 33:51.330
Wir kommen gleich noch zu der Semantikseite, das ist das eigentliche

33:51.330 --> 33:51.870
Interessante.

33:52.470 --> 33:55.670
Von der mechanischen, also von der Einsetzungsseite ergibt es

33:55.670 --> 33:59.530
eigentlich diese Instanzen, die wir hier haben und dass wir eben diese

33:59.530 --> 34:00.830
Sorten berücksichtigen müssen.

34:00.930 --> 34:04.450
Das sind die zwei Dinge, die wir hier noch dazu bekommen.

34:04.970 --> 34:09.070
Und jetzt kommen wir noch zu dem Algorithmus, da können wir also sehr

34:09.070 --> 34:09.890
schnell drüber gehen.

34:10.350 --> 34:14.570
Das ist genau die Eigenschaft, die auch ein Textversetzungsalgorithmus

34:14.570 --> 34:15.390
hat.

34:15.390 --> 34:20.170
Wir müssen also einen Algorithmus hier formulieren mit diesen

34:20.170 --> 34:20.450
Eigenschaften.

34:21.050 --> 34:23.750
Hier ist wieder der Bezug zu den Eigenschaften, die ein Algorithmus

34:23.750 --> 34:25.170
aufweisen soll.

34:25.650 --> 34:29.850
Nämlich, dass er endlich in der Aufschreibung effektiv durchführbar

34:29.850 --> 34:31.330
sein soll und so weiter.

34:31.990 --> 34:36.790
Und das kriegen wir dadurch hin, dass wir eben diese Ersetzungsregel

34:36.790 --> 34:37.970
hier in den Mittelpunkt stellen.

34:38.050 --> 34:40.370
Das ist wieder unsere einzige Operation, die wir haben.

34:40.370 --> 34:49.430
Und die wenden wir eben in der Form an, dass wir eine Anwendung

34:49.430 --> 34:51.170
durchführen von T nach R.

34:52.150 --> 34:57.950
Und was wir dann erreichen ist, dass wir dieses R als Eingabe für den

34:57.950 --> 34:59.830
nächsten Algorithmenschritt verwenden.

34:59.930 --> 35:01.390
Das ist sozusagen unsere Operation.

35:01.390 --> 35:11.410
Und wir kommen dann zu dem Ende, zu dem Terminalen Term, wenn wir

35:11.410 --> 35:13.550
keine weitere Regel finden.

35:14.290 --> 35:16.410
Dann ist also der Algorithmus ans Ende gekommen.

35:16.930 --> 35:22.530
Sie haben aus den vorhergehenden Eigenschaften der Normalform schon

35:22.530 --> 35:22.930
entnommen.

35:23.330 --> 35:26.390
Wir haben hier noch nichts darüber ausgesagt oder wir können auch

35:26.390 --> 35:28.910
keine weitere Aussage treffen, ob das terminiert oder nicht

35:28.910 --> 35:33.310
terminiert, ob das deterministisch ist, ob das nicht deterministisch

35:33.310 --> 35:37.190
ist, ob das Resultat determiniert ist oder nicht determiniert ist.

35:37.550 --> 35:40.910
Also da haben wir eigentlich nichts dazu beigetragen, dass das jetzt

35:40.910 --> 35:42.490
besser werden könnte.

35:43.070 --> 35:45.030
Das müssen Sie also einfach zur Kenntnis nehmen.

35:45.090 --> 35:48.990
Wir haben ja da auch nichts geändert an dem Mechanismus an sich.

35:50.230 --> 35:54.650
Wir haben allerdings die Signatur mit reingebracht und hier nochmal

35:54.650 --> 35:58.270
ein Beispiel, ein Thermersetzungssystem zur Signatur der

35:58.270 --> 35:59.070
Rechenstruktur NAT.

35:59.170 --> 36:04.850
Das ist einfach diese Beispiele, die ich Ihnen vorher aufgezeigt habe,

36:04.890 --> 36:07.670
jetzt hier als Thermersetzungssystem dargestellt.

36:08.230 --> 36:13.190
Wir brauchen also hier Sorten, das ist mal das eine, was wir haben.

36:13.190 --> 36:16.690
Wir brauchen die Funktionen, da haben wir also an der Stelle dann

36:16.690 --> 36:20.470
sozusagen diesen Rechenstrukturanteil hier erbracht.

36:21.010 --> 36:25.250
Wir haben dann entsprechend diese Normalformen, die haben wir ja

36:25.250 --> 36:26.290
vorher auch schon behandelt.

36:26.930 --> 36:33.130
Die sind also im Rahmen der Textversetzungssysteme auch definiert und

36:33.130 --> 36:35.190
jetzt im Thermersetzungssystem einfach übernommen.

36:35.190 --> 36:38.650
Und entsprechend haben wir dann eben diese schon behandelte

36:38.650 --> 36:44.030
Reduktionsregel, die wir jetzt hier einführen können und übernehmen

36:44.030 --> 36:44.410
können.

36:44.910 --> 36:50.390
Und entsprechend können wir diese hier auf solche Thermer anwenden,

36:50.530 --> 36:51.690
der Rechenstruktur.

36:52.210 --> 36:56.730
Und wir kriegen hier eine Wirkung raus, dass wir eben das

36:56.730 --> 37:00.190
Funktionssymbol Predecessor in den Grundthermen eliminieren.

37:01.030 --> 37:04.770
Sie müssen hier an der Stelle nochmal überlegen, ob das wirklich mit

37:04.770 --> 37:07.650
dieser Formel alleine getan ist.

37:08.770 --> 37:14.210
Da ist es also sinnvoll, dass Sie sich noch eine zweite sich auch hier

37:14.210 --> 37:16.470
gönnen, nämlich den genau andersrum.

37:16.470 --> 37:22.530
Wenn Sie den Successor vom Predecessor von X auch noch hier dazunehmen

37:22.530 --> 37:27.890
und das nach X überführen, dann kriegen Sie tatsächlich eine

37:27.890 --> 37:34.870
vollständige Eliminierung dieser Predecessor-Operation raus aus den

37:34.870 --> 37:36.570
Grundthermen, von denen wir hier ausgehen.

37:37.330 --> 37:38.530
Das ist also das Beispiel.

37:39.330 --> 37:48.290
Und jetzt machen wir eigentlich genau den Übergang von diesem

37:48.290 --> 37:50.370
Thermersetzungssystem hin zur Logik.

37:51.290 --> 37:56.650
Und diese Problematik, die hier jetzt angerissen ist in den

37:56.650 --> 38:00.910
Thermersetzungssystemen, die werden wir in der Logik noch etwas weiter

38:00.910 --> 38:05.690
vertiefen, weil wir brauchen Logikgrundlagen, um das wirklich

38:05.690 --> 38:06.870
vernünftig machen zu können.

38:07.430 --> 38:12.750
Aber wir können schon mal sozusagen eine erste Motivation geben, die

38:12.750 --> 38:17.750
in diese Richtung geht, nämlich wir reden hier über Korrektheit.

38:19.750 --> 38:26.970
Und an der Stelle machen wir genau den Übergang zur Semantik, wenn wir

38:26.970 --> 38:31.590
uns über Korrektheit Gedanken machen, sowohl wenn wir über partielle

38:31.590 --> 38:35.730
Korrektheit als auch über vollständige Korrektheit uns Gedanken

38:35.730 --> 38:36.070
machen.

38:36.910 --> 38:38.890
Fangen wir mit der partiellen Korrektheit an.

38:38.990 --> 38:42.150
Erstmal muss man verstehen, was es ungefähr bedeutet, was dahinter

38:42.150 --> 38:44.810
steckt, was da die Aussage ist.

38:45.410 --> 38:50.510
Und dann können wir das nochmal vertiefen und die Vertiefung geht dann

38:50.510 --> 38:51.450
in Richtung der Logik.

38:51.450 --> 38:56.010
Also, wir gehen aus von so einem Thermersetzungssystem und einer

38:56.010 --> 38:56.650
Rechenstruktur.

38:57.230 --> 39:00.250
Das sind die beiden Dinge, also eigentlich brauchen wir die

39:00.250 --> 39:03.390
Rechenstruktur und wir bauen darauf das Thermersetzungssystem auf.

39:03.430 --> 39:05.710
Wir brauchen immer eine Rechenstruktur mit einer Signatur.

39:06.950 --> 39:14.350
So, und was heißt jetzt, dass unser Thermersetzungs... na, nicht das

39:14.350 --> 39:15.450
System, sondern eine Regel.

39:15.730 --> 39:18.950
Das ist schonmal das Erste, worauf Sie Ihre Aufmerksamkeit lenken

39:18.950 --> 39:19.290
sollten.

39:19.790 --> 39:25.790
Diese partielle Korrektheit, das ist eine Aussage zu einer Regel.

39:27.830 --> 39:30.930
Währenddessen die vollständige Korrektheit, das bezieht sich auf das

39:30.930 --> 39:31.270
System.

39:32.250 --> 39:36.110
Das ist erstmal schonmal ein sehr großer Unterschied.

39:37.490 --> 39:43.910
So, wir beleuchten also eine Regel, die schreiben wir hin T-Pfeil R.

39:45.210 --> 39:47.310
Und wann heißt die jetzt partiell korrekt?

39:49.050 --> 39:52.170
Die heißt partiell korrekt bezüglich der Rechenstruktur A.

39:53.690 --> 39:58.210
Und jetzt kommen wir zu einer Sache, die wir schon früher im

39:58.210 --> 40:02.250
Zusammenhang mit der Semantik eingeführt haben.

40:03.710 --> 40:04.310
Semantikbetrachtung.

40:05.390 --> 40:10.110
Falls für jede Belegung Beta in A gilt, dass die

40:10.110 --> 40:15.230
Interpretationsfunktion bezüglich dieser Belegung Beta...

40:15.830 --> 40:16.590
Was war das Beta?

40:16.670 --> 40:18.890
Das Beta hat uns die Identifikatoren belegt.

40:18.890 --> 40:21.230
Also mit Werten belegt.

40:22.370 --> 40:28.490
Dass dieses I-Beta zur Rechenstruktur A bezogen auf das T das gleiche

40:28.490 --> 40:32.010
Ergebnis ergibt, wenn wir die Interpretationsfunktion auf das R

40:32.010 --> 40:35.630
anwenden oder für das R ausrechnen.

40:36.650 --> 40:42.610
Das heißt also an der Stelle, dass wir genau diesen Übergang machen.

40:43.610 --> 40:48.670
Das ist eine Syntax.

40:49.830 --> 40:55.670
Das ist mechanisches Ersetzen von einem Termin einen anderen nach

40:55.670 --> 40:58.610
irgendeiner Vorgabe.

40:59.370 --> 41:02.970
Und dieser Algorithmus, der arbeitet genau nach dieser Vorgabe.

41:03.870 --> 41:09.590
Das ist eigentlich eine Semantikaussage.

41:10.490 --> 41:17.410
Was das jetzt hier bedeutet, was hinter dieser Aussage steckt, ist,

41:18.310 --> 41:25.570
dass wir mit dieser rein syntaktischen Umformung, dass wir damit

41:25.570 --> 41:29.390
semantisch korrekt arbeiten.

41:29.390 --> 41:37.590
Dass wir hier nicht irgendwie eine ungültige oder nicht zulässige

41:37.590 --> 41:40.070
Transformation durchführen, das heißt das.

41:40.390 --> 41:44.930
Und eine nicht gültige, eine unzulässige Transformation, also diese

41:44.930 --> 41:49.050
Adjektive, das bezieht sich genau auf den semantischen Inhalt, auf den

41:49.050 --> 41:53.130
semantischen Wert dieser beiden Terme.

41:53.130 --> 41:57.350
Und der semantische Wert dieser Terme wird genau durch die

41:57.350 --> 42:00.230
Interpretationsfunktion hier angegeben.

42:00.330 --> 42:04.190
Durch das I mit der Belegung Beta zu einer Rechenstruktur A.

42:04.870 --> 42:05.950
Das drückt das aus.

42:07.790 --> 42:13.330
Gut, und wir können jetzt diese auf eine Regel bezogene Eigenschaft,

42:13.870 --> 42:17.690
können wir jetzt auf das System beziehen, indem wir sagen, wenn alle

42:17.690 --> 42:22.490
Regeln diese Eigenschaft der partiellen Korrektheit erfüllen, dann

42:22.490 --> 42:25.050
nennen wir auch dieses System partiell korrekt.

42:25.570 --> 42:29.490
Nichtsdestotrotz ist hier wichtig, dass die von der Konstruktion her

42:29.490 --> 42:32.190
diese partielle Korrektheit, dass wir uns wirklich auf einzelne Regeln

42:32.190 --> 42:32.990
konzentrieren können.

42:32.990 --> 42:36.890
Das gilt dann nicht mehr bei der vollständigen Korrektheit.

42:38.390 --> 42:41.630
Da setzen wir zwar auf ein partiell korrektes Thermasetzungssystem

42:41.630 --> 42:49.430
auf, aber wir machen zwei zusätzliche Eigenschaften, die jetzt das

42:49.430 --> 42:53.490
ganze System betreffen, weil wir jetzt über Terme hinweg das

42:53.490 --> 42:54.050
betrachten.

42:54.690 --> 43:01.610
Und zwar das eine, was wir jetzt hier mit einbeziehen, sind die

43:01.610 --> 43:03.510
nichtterminierenden Berechnungen.

43:03.590 --> 43:04.990
Die muss man ja auch mit berücksichtigen.

43:06.870 --> 43:10.230
Beim Thermasetzungssystem haben wir ja eben die Eigenschaft, dass wir

43:10.230 --> 43:12.730
nichtterminierende Berechnungen erzeugen können.

43:13.230 --> 43:25.130
Und die Eigenschaft ist hier, dass für Grundtherme, die sozusagen

43:25.130 --> 43:35.610
nicht mit dem Bottom-Symbol bewertet werden können, hier ist ja die

43:35.610 --> 43:36.970
Interpretation enthalten.

43:36.970 --> 43:40.390
Also da ist wieder das I mit enthalten, das ist ja die

43:40.390 --> 43:47.470
Kurzschreibweise für I zur Rechenstruktur A bezogen für das T.

43:48.070 --> 43:51.290
Das ist ja hier diese Kurzschreibweise, das ist die Semantik, die wir

43:51.290 --> 43:51.630
haben.

43:53.090 --> 43:58.250
Wenn die semantische Seite besagt, das ist nicht Bottom.

43:58.630 --> 44:03.550
Bottom hatten wir ja immer dann benutzt, wenn wir sozusagen in eine

44:03.550 --> 44:05.250
Nichtterminierung gekommen sind.

44:07.610 --> 44:10.410
Aber wir schließen hier aus, dass das Bottom ist.

44:10.490 --> 44:11.330
Das ist eben nicht Bottom.

44:11.410 --> 44:17.530
Wir wissen, das ist sozusagen nicht mit diesem Spezialwert belegt.

44:17.530 --> 44:20.950
Sie erinnern sich, diesen Spezialwert Bottom hatten wir dazu gehabt,

44:21.270 --> 44:24.650
dass wir trotzdem noch gültig bleiben oder irgendwie einen Wert

44:24.650 --> 44:28.910
zuordnen können, auch wenn wir in eine Nichtterminierung geraten.

44:29.010 --> 44:32.590
Aber hier ist durch das Ungleich gesagt, wir wissen von der

44:32.590 --> 44:34.210
semantischen Seite her, das ist nicht Bottom.

44:34.210 --> 44:44.090
Das ist ein anderer Wert, ein definierter, ein Wert, der wirklich eine

44:44.090 --> 44:47.590
Bedeutung hat, nicht nur dieses Bottom, was so ein Ersatzelement ist.

44:48.890 --> 44:52.530
Und dann müssen wir erwarten, dass von der syntaktischen Seite her,

44:52.570 --> 44:58.030
also von der mechanischen Durchführung der Umsetzung, dass wir dann

44:58.030 --> 45:01.130
auch keine nichtterminierendere Berechnung erhalten.

45:01.130 --> 45:05.670
Das heißt, hier gehen wir also weiter, dass wir also noch eine Aussage

45:05.670 --> 45:08.090
zur Terminierung treffen.

45:09.310 --> 45:11.650
Wenn Sie sich das da oben mal angucken, deswegen partielle

45:11.650 --> 45:15.410
Korrektheit, da haben wir über diesen Fall überhaupt keine Aussage

45:15.410 --> 45:15.750
gemacht.

45:16.190 --> 45:21.350
Hier setzen wir sozusagen noch an und wollen diese partiellen Fälle an

45:21.350 --> 45:24.550
der Stelle da noch eine Forderung stellen.

45:24.550 --> 45:30.010
Und das zweite ist, dass wir in Richtung Determinierung auch eine

45:30.010 --> 45:39.810
Aussage machen, indem wir nämlich sagen, dass wieder für Grundtherme,

45:40.310 --> 45:53.050
die eben von denen wir wissen, dass diese verschieden sind und dass

45:53.050 --> 45:56.430
diese auf der anderen Seite auch nicht Bottom sind.

45:58.510 --> 46:04.350
Dass wenn wir die beiden Sachen wissen, dass wir dann auch fordern

46:04.350 --> 46:11.790
können oder dass wir dann wissen, dass deren Interpretationen, also

46:11.790 --> 46:14.710
das ist wieder hier die Interpretation, die dahinter steckt, wieder

46:14.710 --> 46:22.970
diese Kurzschreibweise, also die Semantik dieser Therme, dass sie eben

46:22.970 --> 46:23.990
auch unterschiedlich ist.

46:24.270 --> 46:28.710
Das geht in Richtung Determinierung, das geht in Richtung

46:28.710 --> 46:29.250
Terminierung.

46:29.330 --> 46:33.370
Das ist nicht genau Terminierung, Determinierung, aber mit diesen

46:33.370 --> 46:36.650
Eigenschaften des Algorithmus und mit diesen Eigenschaften auf der

46:36.650 --> 46:39.210
Semantikseite wird eben entsprechend gearbeitet.

46:39.210 --> 46:44.710
Gut, jetzt kommen wir dann zu dem Abschnitt 3-4 und ich glaube, das

46:44.710 --> 46:46.810
ist ganz geeignet, um fünf Minuten Pause zu machen.

51:32.020 --> 51:33.400
So, ich würde gerne weitermachen.

51:41.520 --> 51:42.480
Mathematische Logik.

51:46.810 --> 51:53.050
Versuchen wir nochmal zu motivieren, warum wir uns mit mathematischer

51:53.050 --> 51:55.390
Logik beschäftigen und was wir eigentlich hier tun.

51:55.390 --> 52:00.610
Da werden Sie sehen, dass wir letztendlich dieses Spiel zwischen

52:00.610 --> 52:05.370
Syntax, Semantik und stimmt das eine mit dem anderen überein, ist das,

52:05.430 --> 52:11.450
was wir da syntaktisch betreiben, stimmt das mit der Semantik überein

52:11.450 --> 52:15.090
oder ist das semantisch zu vertreten sozusagen.

52:15.610 --> 52:19.650
Das ist genau das, was wir eigentlich in der mathematischen Logik uns

52:19.650 --> 52:20.150
vornehmen.

52:20.150 --> 52:28.830
Und wir haben hier zwei Bereiche oder zwei Arten von Aussagen.

52:32.480 --> 52:37.460
Wir haben eine Menge, die werden wir nennen herleitbare oder

52:37.460 --> 52:38.840
ableitbare Aussagen.

52:42.000 --> 52:50.720
Und da werden wir so ein Symbol verwenden, das eben so eine, also

52:50.720 --> 52:55.780
nicht ein Pfeil, sondern ein Ableitungssymbol, das eben genau diese

52:55.780 --> 52:57.960
Eigenschaft hier oder dieses Aussehen hat.

53:00.220 --> 53:06.020
So und dann haben wir eine zweite Menge von Aussagen, das sind die

53:06.020 --> 53:07.020
wahren Aussagen.

53:08.920 --> 53:10.480
Die wahren Aussagen.

53:13.820 --> 53:21.360
Und das ist genau hier dieser Zusammenhang zwischen das, was wir hier

53:21.360 --> 53:30.220
als Syntax begreifen, dieses Herleitungs- oder Ableitungssymbol, das

53:30.220 --> 53:33.780
übernimmt die Rolle unseres Pfeils in den Text- und

53:33.780 --> 53:35.440
Thermalsetzungssystemen.

53:35.440 --> 53:42.860
Allerdings werden wir hier sozusagen noch ein Kalkül dazu angeben.

53:42.960 --> 53:45.480
Gut, die Text- und Thermalsetzungssysteme sind eigentlich auch nichts

53:45.480 --> 53:49.840
anderes als Kalküle, aber ein spezielles Kalkül, nämlich ein

53:49.840 --> 53:51.960
Logikkalkül steckt hier eben dahinter.

53:53.660 --> 53:54.620
Ein Logikkalkül.

53:55.120 --> 53:59.720
Und das gibt es eben ein Logikkalkül für die Aussagenlogik und ein

53:59.720 --> 54:01.460
Logikkalkül für die Prädikatenlogik.

54:01.460 --> 54:06.720
Die werden wir eben hier herleiten, den werden wir uns hier

54:06.720 --> 54:07.500
auseinandersetzen.

54:08.160 --> 54:10.200
Dann haben wir auf der anderen Seite aber noch die Semantik.

54:12.180 --> 54:15.680
Das sind genau diese Fragen, ist das eine wahre Aussage?

54:16.980 --> 54:20.200
Das ist nicht mehr reines Syntax, sondern das ist der Wahrheitsgehalt,

54:20.400 --> 54:23.420
der Bedeutungsgehalt der Aussage.

54:24.400 --> 54:27.320
Die wollen wir hier untersuchen.

54:27.440 --> 54:29.540
Es gibt wahre Aussagen, es gibt falsche Aussagen.

54:29.540 --> 54:34.620
Das können wir also nicht mehr syntaktisch irgendwie abprüfen, sondern

54:34.620 --> 54:37.400
da brauchen wir ein semantisches Modell dahinter.

54:38.180 --> 54:41.300
Und jetzt gibt es eben zwei Zusammenhänge.

54:43.060 --> 54:46.700
Der eine Zusammenhang geht in die Richtung von den herleitbaren

54:46.700 --> 54:48.540
Aussagen zu den wahren Aussagen.

54:49.380 --> 54:58.540
Und falls wir zeigen können, dass jede herleitbare Aussage eine wahre

54:58.540 --> 55:01.820
Aussage ist, dann reden wir von Korrektheit.

55:01.820 --> 55:05.480
Also Korrektheit, das haben wir gerade schon kennengelernt im Begriff.

55:06.460 --> 55:11.920
Wo wir geschaut haben, ist das partiell oder total korrekt, oder

55:11.920 --> 55:15.960
vollständig korrekt, diese Thermersetzungssysteme.

55:15.960 --> 55:28.620
Korrektheit bedeutet hier, jede herleitbare Aussage, das ist der linke

55:28.620 --> 55:30.920
Teil, ist wahr.

55:33.720 --> 55:36.700
Das bedeutet, wenn wir hier von dem Logikkalkül ausgehen, wir wollen

55:36.700 --> 55:41.820
ja diese Herleitung oder Ableitung, wo wir über ein Kalkül

55:41.820 --> 55:45.720
beschreiben, der tut das, was wir uns so vorstellen, er produziert

55:45.720 --> 55:46.900
keine falschen Aussagen.

55:47.200 --> 55:50.500
Das ist also jetzt hier in der Richtung die Korrektheit.

55:54.640 --> 56:00.100
Genauso ist aber andersrum interessant zu fragen, jetzt habe ich eine

56:00.100 --> 56:03.340
wahre Aussage, ist die denn auch ableitbar, ist die herleitbar?

56:03.920 --> 56:07.000
Und das ist genau die Vollständigkeit,

56:10.860 --> 56:24.240
die besagt, jede wahre Aussage ist herleitbar.

56:27.560 --> 56:34.240
Ist klar, dass das zwei verschiedene Dinge sind, die jetzt nicht

56:34.240 --> 56:38.260
unmittelbar für jedes Kalkül zutreffen.

56:38.420 --> 56:41.680
Wir müssen also ganz klar hier erstmal die eine Richtung überlegen,

56:42.420 --> 56:43.980
das ist noch relativ einfach.

56:45.040 --> 56:49.300
Die Korrektheit ist, da gehe ich einfach wieder irgendwie über die

56:49.300 --> 56:54.120
Therme und zeige, dass ich sozusagen immer, wenn ich mal wahre

56:54.120 --> 56:59.340
Aussagen habe und ich wende diese Regeln des Kalküls an, dann bleiben

56:59.340 --> 56:59.760
die wahr.

57:00.480 --> 57:06.180
Die andere Richtung ist schon erheblich schwieriger von den wahren

57:06.180 --> 57:11.540
Aussagen auszugehen und zu fragen, sind die denn alle da enthalten in

57:11.540 --> 57:12.140
dem Kalkül.

57:12.140 --> 57:17.740
Aber die beiden Begriffe Korrektheit und Vollständigkeit sind

57:17.740 --> 57:21.700
unmittelbar mit der mathematischen Logik, so wie sie der Informatiker

57:21.700 --> 57:23.480
benötigt, unmittelbar verknüpft.

57:23.540 --> 57:27.220
Da geht es eigentlich immer um diese Fragen und damit einhergehend

57:27.220 --> 57:30.380
auch, wie gesagt, um diese Fragen der Syntax und der Semantik.

57:30.380 --> 57:33.460
Da ist das eigentlich in dieser mathematischen Logik, ist diese

57:33.460 --> 57:38.200
Fragestellung und diese mathematischen Grundlagen, die wir brauchen,

57:38.340 --> 57:42.660
um solche Fragen zu behandeln, sind hier eben enthalten und deswegen

57:42.660 --> 57:45.420
beschäftigen wir uns mit dieser Logik.

57:45.880 --> 57:48.820
Und da haben wir zwei Ausprägungen, die Aussagen-Logik und die

57:48.820 --> 57:49.800
Prädikaten -Logik.

57:49.800 --> 57:55.780
Und die Prädikaten-Logik, das ist hier schon mal angegeben, da kommen

57:55.780 --> 58:05.560
also noch neben der Sorte Buhl und der dazugehörigen Rechenstruktur

58:05.560 --> 58:09.740
weitere Signaturen und Rechenstrukturen mit ins Spiel.

58:10.300 --> 58:14.280
Nämlich, wenn wir diese Identifikatoren mit reinbringen und da die

58:14.280 --> 58:17.580
Quantifizierung, die es gibt, für alle durchführen, dann kommen hier

58:17.580 --> 58:21.700
also noch weitere Rechenstrukturen mit rein, die liefern aber alle,

58:21.960 --> 58:24.480
eben enden alle in der Sorte Buhl.

58:25.100 --> 58:28.780
Das sind also sozusagen logische Prädikaten, logische Aussagen.

58:28.780 --> 58:33.280
Dann eine Sache, die wir hier an der Stelle schon mal vorwegnehmen

58:33.280 --> 58:37.540
müssen, weil sie für die Rechenstrukturen, die wir bislang behandelt

58:37.540 --> 58:40.060
haben, eben nicht gilt.

58:40.640 --> 58:42.800
Das Prinzip des Tertium non datur.

58:43.580 --> 58:50.160
Bedeutet ganz einfach, dass wir so ein Bottom-Element, so ein drittes

58:50.160 --> 58:53.780
Element, neben wahr und falsch, haben wir hier nicht.

58:53.780 --> 58:59.940
Das heißt, wir haben sozusagen eine zweiwertige Logik, die wir hier

58:59.940 --> 59:08.340
zugrunde legen und wir haben also hier sogenannte starke Terme, auf

59:08.340 --> 59:10.720
die wir uns zurückziehen.

59:11.220 --> 59:18.600
Das heißt, diese undefinierte Problematik, die ja dadurch entsteht in

59:18.600 --> 59:21.380
Programmen, dass wir nichtterminierende Programme haben und dann haben

59:21.380 --> 59:29.100
wir eben sozusagen diese Lücke, dadurch halbwegs uns behelfen können,

59:29.200 --> 59:31.580
dass wir eben hier dieses Bottom-Element eingeführt haben, das

59:31.580 --> 59:32.760
brauchen wir an der Stelle gar nicht.

59:32.760 --> 59:36.880
Wir gehen also von der zweiwertigen Logik aus, es gibt entweder nur

59:36.880 --> 59:40.240
wahr oder falsch, es gibt nichts dazwischen, deswegen das dritte, es

59:40.240 --> 59:41.400
muss nicht gezeigt werden.

59:41.900 --> 59:44.740
Das heißt, es gibt nur zwei Werte, wahr und falsch.

59:44.740 --> 59:50.620
Starke Terme werden Formeln genannt, Grundterme, die Formeln

59:50.620 --> 59:52.600
darstellen, heißen auch elementare Aussagen.

59:52.780 --> 59:57.120
Dieser Begriff der elementaren Aussage, der kommt also an

59:57.120 --> 01:00:00.460
verschiedenen Stellen jetzt nochmal vor, ist aber weiter sonst nicht

01:00:00.460 --> 01:00:02.740
zu vertiefen.

01:00:03.740 --> 01:00:07.560
Kommen wir zu dem Inhalt der mathematischen Logik.

01:00:08.080 --> 01:00:11.700
Eigentlich ist dieses erste Tafelbild, das ich Ihnen angegeben habe,

01:00:11.760 --> 01:00:15.540
das gibt diesen Inhalt nochmal sehr plastisch wieder und die

01:00:15.540 --> 01:00:18.660
Fragestellung nochmal sehr informell und plastisch wieder.

01:00:18.660 --> 01:00:25.940
Kommen wir mal zu der etwas formaleren Zuwendung, was Inhalte der

01:00:25.940 --> 01:00:27.260
mathematischen Logik sind.

01:00:27.780 --> 01:00:34.780
Wir haben immer Formeln der Sorte Buhl vor Augen.

01:00:35.660 --> 01:00:39.780
Wir beschäftigen uns mit Formeln der Sorte Buhl und was wir hier

01:00:39.780 --> 01:00:51.100
letztendlich uns überlegen ist, wie wir mit diesen Formeln schließen

01:00:51.100 --> 01:00:51.420
können.

01:00:51.520 --> 01:00:54.520
Das ist also sehr vergleichbar mit den Text- und

01:00:54.520 --> 01:00:55.880
Termersetzungssystemen.

01:00:55.880 --> 01:01:04.840
Aber wir wollen auf ein Kalkül raus oder ein Herleitungssystem raus,

01:01:05.100 --> 01:01:13.180
das uns letztendlich diesen Begriff der Wahrheit, des Wahren im Sinne

01:01:13.180 --> 01:01:15.960
der mathematischen Logik zu beschreiben erlaubt.

01:01:15.960 --> 01:01:24.520
Wir wollen sozusagen die wahren Buhl'schen Formeln erarbeiten.

01:01:25.360 --> 01:01:30.380
Und jetzt gehen wir nochmal zurück auf die Überlegung, die wir schon

01:01:30.380 --> 01:01:33.360
angestellt haben im Zusammenhang mit der Rechenstruktur, mit der

01:01:33.360 --> 01:01:34.280
Algebra Buhl.

01:01:34.280 --> 01:01:38.060
Wir wollen letztendlich jetzt von der Aussagenlogik her betrachtet

01:01:38.060 --> 01:01:44.900
alle Buhl'schen Formeln in dem Kalkül herleiten, die nach der Belegung

01:01:44.900 --> 01:01:53.900
und dann Auswertung der Formel zu dem Ergebnis true oder wahr werden.

01:01:53.900 --> 01:01:57.660
Die wollen wir syntaktisch beschreiben können mit diesem logischen

01:01:57.660 --> 01:01:58.180
Kalkül.

01:01:58.840 --> 01:01:59.440
Das steht hier.

01:02:00.360 --> 01:02:05.140
Und als Interpretation den Wert L haben, das ist genau die Aussage,

01:02:05.320 --> 01:02:11.120
die Semantikfunktion oder die Interpretationsfunktion soll den Wert

01:02:11.120 --> 01:02:12.100
true liefern.

01:02:12.100 --> 01:02:15.340
Mit denen wollen wir uns beschäftigen.

01:02:16.740 --> 01:02:21.520
Und dazu müssen wir uns überlegen, wie denn das Schlussfolgern

01:02:21.520 --> 01:02:21.960
aussieht.

01:02:22.960 --> 01:02:25.680
Und dieses Schlussfolgern müssen wir entsprechend formalisieren.

01:02:25.680 --> 01:02:32.160
Das heißt, wir müssen hier ein Regelsystem aufstellen, das uns diese

01:02:32.160 --> 01:02:36.340
Art des Schlussfolgerns sozusagen syntaktisch manifestiert.

01:02:37.260 --> 01:02:40.720
Die Formeln, das sind wie gesagt diese zweiwertigen Terme.

01:02:41.120 --> 01:02:44.380
Elementaren Aussagen hatten wir schon auf der letzten Folie.

01:02:45.240 --> 01:02:51.380
Und was wir hier eben wollen, ist diese Ableitung von Formeln aus

01:02:51.380 --> 01:03:00.140
einer vorgegebenen Menge von Formeln, von denen wir aber ausgehen,

01:03:00.220 --> 01:03:00.960
dass die wahr sind.

01:03:01.840 --> 01:03:07.220
Und was wir erreichen wollen ist, dass die abgeleiteten Formeln eben

01:03:07.220 --> 01:03:07.980
auch wahr sind.

01:03:08.660 --> 01:03:11.600
Das ist das, wenn wir das erreichen, wenn wir hier diesen

01:03:11.600 --> 01:03:18.000
Ableitungsbegriff, und das ist syntaktisch zu verstehen, das ist

01:03:18.000 --> 01:03:20.740
wieder Syntax, syntaktisch.

01:03:21.760 --> 01:03:23.440
Ableitung ist immer syntaktisch.

01:03:23.760 --> 01:03:29.720
Wenn wir sagen, wir finden ein Ableitungssystem, das aus wahren

01:03:29.720 --> 01:03:35.100
Formeln nur wahre Formeln produziert, dann haben wir zumindest schon

01:03:35.100 --> 01:03:36.020
mal diese Seite hier.

01:03:36.580 --> 01:03:40.060
Dann haben wir letztendlich diese Korrektheit.

01:03:40.920 --> 01:03:44.960
Gut, wir dürfen natürlich auch nur wahre Formeln reinstecken.

01:03:45.320 --> 01:03:49.040
Das wird aber im Ableitungssystem, im Herleitungssystem dann auch

01:03:49.040 --> 01:03:51.720
garantiert.

01:03:52.240 --> 01:03:56.940
Und die ganze weitere Herleitung führt eben dazu, dass wir nur zu

01:03:56.940 --> 01:03:57.840
wahren Aussagen kommen.

01:03:57.840 --> 01:03:59.920
Das ist genau hier die Korrektheit.

01:04:00.480 --> 01:04:05.520
Was wir dann noch machen müssen ist, damit wir wirklich diesen Begriff

01:04:05.520 --> 01:04:09.740
der wahren Formel sauber definieren können, müssen wir natürlich noch

01:04:09.740 --> 01:04:13.360
auf der anderen Seite was für die Vollständigkeit tun.

01:04:13.460 --> 01:04:16.880
Das heißt, wir müssen irgendwie garantieren, dass wir wirklich alle

01:04:16.880 --> 01:04:20.320
wahren Aussagen mit diesem Kalkül erwischen, mit diesem

01:04:20.320 --> 01:04:21.200
Ableitungsbegriff.

01:04:21.200 --> 01:04:24.800
Das ist also der Inhalt der mathematischen Logik.

01:04:24.880 --> 01:04:30.040
Sie sehen also, was hier steht, etwas trockener, das finden Sie genau

01:04:30.040 --> 01:04:35.720
in dem Bild wieder, bezogen jetzt stark auf Aussagen und auf

01:04:35.720 --> 01:04:36.960
Prädikatenlogik an der Stelle.

01:04:37.680 --> 01:04:40.860
Aussagenlogik, jetzt kommt hier nochmal diese Trennung, das sind

01:04:40.860 --> 01:04:42.900
wirklich einfache Terme der Sorte Buhl.

01:04:42.900 --> 01:04:49.080
Da kommen nur Buhlsche Elemente vor, die wir mit den entsprechenden

01:04:49.080 --> 01:04:50.600
Buhlschen Operationen verknüpfen.

01:04:51.500 --> 01:04:55.960
Insofern eine sehr eingeschränkte Welt, sage ich mal, sehr

01:04:55.960 --> 01:05:00.340
eingeschränkte Terme, die allerdings den Vorteil haben, dass sie auch

01:05:00.340 --> 01:05:01.480
sehr gut überschaubar sind.

01:05:01.480 --> 01:05:06.180
Ich kann mit diesen Termen eigentlich den Semantikbegriff dadurch

01:05:06.180 --> 01:05:11.280
behandeln, dass ich die im Sinne einer Wertetabelle belege und schaue,

01:05:11.340 --> 01:05:12.400
was kommt denn hinten raus.

01:05:13.240 --> 01:05:18.960
Also beispielsweise, wenn Sie sich Gedanken machen, wie kann ich denn

01:05:18.960 --> 01:05:27.040
hier diesen Und-Operator, wie kann ich da die Semantik festlegen und

01:05:27.040 --> 01:05:32.400
Sie legen die Semantik vollständig dadurch fest in der Aussagenlogik,

01:05:32.400 --> 01:05:37.400
und das können Sie in der Aussagenlogik, indem Sie sagen, hier kommt

01:05:37.400 --> 01:05:39.260
ein L raus und da kommt immer ein 0 raus.

01:05:39.900 --> 01:05:44.200
Sie gehen von der zweiwertigen Logik aus, Sie haben einen Tertium

01:05:44.200 --> 01:05:48.760
-Nondator, Sie haben kein weiteres Element und Sie haben mit dieser

01:05:48.760 --> 01:05:59.040
Wertetabelle, mit dieser Wertetabelle ist die Semantik von diesem

01:05:59.040 --> 01:06:03.160
Operator vollständig beschrieben.

01:06:05.740 --> 01:06:08.840
Das ist Semantik, diese Wertebelegung ist Semantik, Sie können auch

01:06:08.840 --> 01:06:12.820
die Interpretationsfunktion entsprechend daraus dann eben gestalten.

01:06:13.660 --> 01:06:16.700
Und das ist das Schöne bei der Aussagenlogik, das können Sie ja für

01:06:16.700 --> 01:06:21.820
alle Operationen machen, das heißt, Sie haben endlich einen

01:06:21.820 --> 01:06:23.100
Ergebnisraum, wenn Sie so wollen.

01:06:23.920 --> 01:06:28.600
Und das verlieren Sie bei der Prädikatenlogik allein schon dadurch,

01:06:28.760 --> 01:06:33.260
dass Sie das ausweiten, Sie interessieren sich hier auch noch für

01:06:33.260 --> 01:06:37.440
andere Sorten und Trägermengen und Sie nehmen in bestimmter Art und

01:06:37.440 --> 01:06:47.280
Weise in Ihren Prädikatenlogischen Termen, nehmen Sie darauf Bezug.

01:06:48.260 --> 01:06:53.840
Und das heißt, hier kriegen Sie sozusagen eine enorme Ausweitung

01:06:53.840 --> 01:06:59.120
dieses Ergebnisraumes, aber Sie können die ganzen Dinge, die Sie für

01:06:59.120 --> 01:07:04.800
die Aussagenlogik sich überlegen, nämlich dieses Bildchen hier, das

01:07:04.800 --> 01:07:08.680
gilt für die Aussagenlogik genauso wie für die Prädikatenlogik.

01:07:08.840 --> 01:07:14.880
Da ist also sozusagen die Analogie, sowohl in der Aussagenlogik als

01:07:14.880 --> 01:07:17.020
auch in der Prädikatenlogik geht es um wahre Aussagen.

01:07:18.160 --> 01:07:21.540
Und das können wir relativ schnell einsehen, dass das also für die

01:07:21.540 --> 01:07:25.120
prädikatenlogischen Ausdrücke um ein erhebliches schwieriger ist,

01:07:25.120 --> 01:07:30.280
diese Thematik zu behandeln, als für die Aussagenlogik, wo wir uns

01:07:30.280 --> 01:07:33.540
eben hier zurückziehen können auf diese Bewertungstabellen,

01:07:33.760 --> 01:07:34.680
Bewertungstablos.

01:07:37.560 --> 01:07:42.520
So, kommen wir zur Aussagenlogik, da werden wir also jetzt so die

01:07:42.520 --> 01:07:47.900
Begrifflichkeiten einführen und werden insbesondere eben auf den

01:07:47.900 --> 01:07:49.940
Kalkül kommen.

01:07:49.940 --> 01:07:59.840
Nämlich hier steckt eigentlich nichts anderes drin, als unser Kalkül

01:07:59.840 --> 01:08:01.100
für die Aussagenlogik.

01:08:02.580 --> 01:08:09.060
Kalkül für die Aussagenlogik ist

01:08:13.020 --> 01:08:19.640
letztendlich das Termersetzungssystem, das die mathematische

01:08:19.640 --> 01:08:22.900
Aussagenlogik beschreibt.

01:08:23.820 --> 01:08:30.260
Jetzt kommen wir erstmal zu diesem schon eingeführten Symbol, das

01:08:30.260 --> 01:08:31.320
Ableitungssymbol.

01:08:32.320 --> 01:08:40.360
Aus einer Hypothesenmenge ist eine Formel T ableitbar, heißt das, man

01:08:40.360 --> 01:08:41.340
beachte Syntax.

01:08:42.860 --> 01:08:49.100
Das ist eine Syntax, wie ein Termersetzungssystem funktioniert das,

01:08:49.880 --> 01:08:51.960
nur halt mit etwas anderen Spielregeln.

01:08:52.920 --> 01:08:59.340
Und das sind die Ableitungsregeln, das sind die Ersetzungsregeln, die

01:08:59.340 --> 01:09:01.740
wir eben aus den Text- und Termersetzungssystemen erkennen.

01:09:03.360 --> 01:09:10.200
Und das sind insgesamt drei, die wir jetzt hier einführen.

01:09:11.700 --> 01:09:18.180
Das Tertium Non Latur ermöglicht uns letztendlich diese erste Regel

01:09:18.180 --> 01:09:18.920
hinzuschreiben.

01:09:19.720 --> 01:09:27.280
Wir können aus dem Nichts heraus, jetzt muss man vielleicht noch das

01:09:27.280 --> 01:09:32.180
einführen, wenn ich sowas hinschreibe, dann entspricht das eigentlich,

01:09:33.000 --> 01:09:34.780
dass unsere Hypothesenmenge leer ist.

01:09:35.420 --> 01:09:41.120
Das entspricht sozusagen, dass ich aus dem Nichts einen Term herleiten

01:09:41.120 --> 01:09:41.440
kann.

01:09:41.440 --> 01:09:48.400
Und dann lasse ich diese leere Menge weg und schreibe links gar nichts

01:09:48.400 --> 01:09:48.580
hin.

01:09:49.460 --> 01:09:53.320
Das ist also hier nur eine Spezialform.

01:09:54.440 --> 01:09:59.120
An der Stelle ist das H leer, die leere Menge, und das T ist das T

01:09:59.120 --> 01:10:00.260
oder Nicht-T an der Stelle.

01:10:01.740 --> 01:10:07.940
Gut, und das kann ich mit dem loslegen.

01:10:08.780 --> 01:10:11.800
Da steht T oder Nicht-T kann ich immer hinschreiben, kann ich immer

01:10:11.800 --> 01:10:13.300
als wahr annehmen.

01:10:17.560 --> 01:10:20.900
Kommt daher, weil ich kein drittes Element zulasse, keinen dritten

01:10:20.900 --> 01:10:21.520
Wert zulasse.

01:10:22.800 --> 01:10:29.880
Der Modus ponens ist dann der eigentliche Kern, mit dem ich dann meine

01:10:29.880 --> 01:10:33.760
syntaktischen Ableitungen vollführe.

01:10:35.260 --> 01:10:41.840
Der besagt, hier haben wir die Hypothesenmenge, hier ist nochmal die

01:10:41.840 --> 01:10:45.220
Formelmenge, das könnte man auch Hypothesenmenge nennen.

01:10:45.220 --> 01:10:48.860
Ich habe das jetzt immer Hypothesenmenge genannt, daher kommt auch das

01:10:48.860 --> 01:10:51.420
H.

01:10:52.120 --> 01:10:56.860
Eine Hypothese ist eine Formel, von der ich ausgehe, dass die eben

01:10:56.860 --> 01:10:57.940
gültig ist.

01:11:01.340 --> 01:11:03.780
Das wäre vielleicht auch noch ganz interessant, dass ich Ihnen hier

01:11:03.780 --> 01:11:04.440
hinschreibe.

01:11:06.600 --> 01:11:08.640
Hier redet man auch von gültigen.

01:11:11.020 --> 01:11:15.560
Wenn ich von gültigen Aussagen rede, dann sind das herleitbare Reden.

01:11:16.360 --> 01:11:20.820
Wenn ich von wahren Aussagen rede, dann meine ich die Semantikseite.

01:11:20.880 --> 01:11:23.720
Wenn ich von gültig rede, dann ist das ein syntaktischer Begriff.

01:11:25.800 --> 01:11:27.060
Gültige, herleitbare Aussagen.

01:11:27.240 --> 01:11:28.500
Und dann sage ich eben an der Stelle,

01:11:31.800 --> 01:11:35.640
wenn die in der Hypothesenmenge auftreten, sind das gültige Aussagen.

01:11:36.120 --> 01:11:41.120
Das sind dann Aussagen, die ich eigentlich schon hergeleitet habe.

01:11:41.200 --> 01:11:43.760
Die kann ich in die Hypothesenmenge aufnehmen.

01:11:45.180 --> 01:11:52.820
Und jetzt habe ich hier diese beiden Formeln, die in der

01:11:52.820 --> 01:11:57.720
Hypothesenmenge sind, die habe ich jetzt sozusagen schon hergeleitet,

01:11:57.860 --> 01:12:00.480
oder von denen gehe ich aus, dass die gültig sind, so muss ich sagen.

01:12:01.440 --> 01:12:08.520
Und wenn die die Form haben, dass ich weiß, T1 ist gültig, und die

01:12:08.520 --> 01:12:15.680
Formel Nicht-T1 oder T2 ist gültig, dann kann ich hier leiten, T2,

01:12:16.200 --> 01:12:18.440
dann ist die Gültigkeit von T2 gegeben.

01:12:18.960 --> 01:12:20.040
Das ist der Modus Pronens.

01:12:21.180 --> 01:12:24.580
Und den kann man sich dann auch nochmal hier nochmal ein bisschen

01:12:24.580 --> 01:12:25.300
klarer machen.

01:12:26.320 --> 01:12:31.320
Nämlich, dieses Nicht-T1 oder T2, das ist ja nichts anderes als die

01:12:31.320 --> 01:12:32.740
Implikation, die wir hier haben.

01:12:34.220 --> 01:12:37.900
Das ist ja nur eine andere Schreibweise für diesen Implikationsfall.

01:12:38.640 --> 01:12:43.640
Und dann kann man sich das also schon plausibel machen.

01:12:43.780 --> 01:12:46.980
Wir kommen gleich darauf, dass das also auch zu korrekten Ergebnissen

01:12:46.980 --> 01:12:47.300
führt.

01:12:47.560 --> 01:12:49.660
Muss man einfach nur die Interpretationsfunktion darauf anwenden.

01:12:50.400 --> 01:12:57.000
Wenn X impliziert Y und wir kennen die Prämisse des X, dann können wir

01:12:57.000 --> 01:12:58.220
eben auch das Y herleiten.

01:12:58.520 --> 01:13:00.140
Das drückt der Modus Pronens aus.

01:13:01.080 --> 01:13:06.640
Und das dritte Gesetz, das zieht sozusagen die semantische Äquivalenz

01:13:06.640 --> 01:13:11.940
und die semantischen Äquivalenzen in dieses Kalkülsystem rein, in

01:13:11.940 --> 01:13:12.840
dieses Kalkül rein.

01:13:12.840 --> 01:13:18.380
Besagt nämlich, wenn ich die semantische Äquivalenz von zwei Termen

01:13:18.380 --> 01:13:27.460
kenne oder wenn ich die weiß, wenn ich die sozusagen irgendwie aus der

01:13:27.460 --> 01:13:37.080
Buhl'schen Algebra heraus ableiten kann, dann kann ich aus der

01:13:37.080 --> 01:13:41.520
Hypothesenmenge, die aus der einen Formel besteht, die zweite Formel

01:13:41.520 --> 01:13:42.240
ableiten.

01:13:42.960 --> 01:13:45.860
Und ich kann genauso, das ist da an der Stelle symmetrisch, ich kann

01:13:45.860 --> 01:13:50.540
natürlich auch aus T2 T1 ableiten.

01:13:51.460 --> 01:13:55.340
Das ist sozusagen, ich ziehe die semantische Äquivalenz, die sich aus

01:13:55.340 --> 01:14:01.860
der Buhl'schen Algebra heraus ergibt, hier sind bitte die Gesetze,

01:14:02.800 --> 01:14:07.800
nochmal zu berücksichtigen, ziehe ich in diesen Kalkül rein.

01:14:08.080 --> 01:14:11.720
Das ist die Anwendung der Gleichheitsgesetze.

01:14:12.660 --> 01:14:19.680
Jetzt können wir hier einen einfachen Hilfsatz, einen Lemma, damit

01:14:19.680 --> 01:14:26.860
können wir mal die erste Anwendung dieses Kalküls vornehmen.

01:14:27.860 --> 01:14:35.060
Und dieses Lemma bedeutet oder drückt aus, wenn wir aus der

01:14:35.060 --> 01:14:42.640
Hypothesenmenge H ableiten können, dass TA impliziert TB.

01:14:45.200 --> 01:14:51.900
Dann können wir auch Folgendes ableiten, dass wir dieses TA in die

01:14:51.900 --> 01:14:55.080
Hypothesenmenge aufnehmen, also die Hypothesenmenge um das TA

01:14:55.080 --> 01:14:56.120
ergänzen.

01:14:57.040 --> 01:15:01.940
TA vereinigt TA und aus dieser Hypothesenmenge, die jetzt um das TA

01:15:01.940 --> 01:15:04.880
erweitert ist, können wir dann das TB ableiten.

01:15:05.660 --> 01:15:12.840
Das ist also ein einfacher Hilfsatz und letztendlich steckt dahinter

01:15:12.840 --> 01:15:14.480
der Modus ponens, wie Sie sehen.

01:15:15.220 --> 01:15:18.960
Sie können nämlich Folgendes machen, Sie fangen mit der Voraussetzung

01:15:18.960 --> 01:15:26.560
hier an, dann lösen Sie diese Implikation auf, schreiben eben statt TA

01:15:26.560 --> 01:15:29.360
impliziert TB, nicht TA oder TB.

01:15:29.960 --> 01:15:33.580
Dann können Sie jetzt hier an der dritten Stelle, auf der dritten

01:15:33.580 --> 01:15:40.020
Zeile schreiben Sie einfach den Modus ponens hin, mit entsprechend TA

01:15:40.020 --> 01:15:48.800
ist an der Stelle das T1 und TB ist das T2.

01:15:49.500 --> 01:15:55.380
Das ist genau diese Zeile hier auf dieses TA und TB angewendet, das

01:15:55.380 --> 01:15:56.760
können Sie ja nennen, wie so lustig sind.

01:15:56.760 --> 01:16:00.620
Und können daraus TB ableiten.

01:16:01.460 --> 01:16:08.360
Und jetzt kommt hier eigentlich noch eine Zeile rein, mit der Sie

01:16:08.360 --> 01:16:12.840
diese Zeile nochmal etwas umgestalten.

01:16:12.840 --> 01:16:30.000
Nämlich, wenn Sie das schreiben, nicht TA oder TB, vereinigt TA und

01:16:30.000 --> 01:16:31.660
dann können Sie hier ableiten TB.

01:16:32.860 --> 01:16:38.800
Haben Sie das eigentlich nur nochmal etwas anders angeordnet, diese

01:16:38.800 --> 01:16:41.660
Zeile hier nochmal hingeschrieben.

01:16:43.120 --> 01:16:48.140
Und jetzt können Sie hier eben das eigentliche, was Sie beweisen

01:16:48.140 --> 01:16:49.860
wollen, daraus ableiten.

01:16:50.460 --> 01:16:53.820
Aus diesen beiden ableiten sollte man hier nicht sagen, sondern daraus

01:16:53.820 --> 01:16:56.700
den Schluss ziehen, das ist nämlich eine Schlussfolgerung hier.

01:16:56.700 --> 01:17:00.960
Das ist ein Schluss, den Sie ziehen, Schlussfolgerung.

01:17:03.740 --> 01:17:09.840
Diese Schlussfolgerung können Sie nämlich jetzt treffen, weil Sie an

01:17:09.840 --> 01:17:19.200
der Stelle diese rechte Seite, die Sie hier aus der Hypothesenmenge H

01:17:19.200 --> 01:17:26.520
abgeleitet haben, die können Sie auf die linke Seite schreiben.

01:17:27.100 --> 01:17:28.940
Und das ist genau das, was Sie hier getan haben.

01:17:29.740 --> 01:17:36.340
Und dann kommen Sie zu dem Schluss, dass Sie hier das TB herleiten

01:17:36.340 --> 01:17:36.640
können.

01:17:36.980 --> 01:17:40.860
Was dahinter steckt, das muss man vielleicht nochmal in allgemeiner

01:17:40.860 --> 01:17:41.580
Form darstellen.

01:17:41.680 --> 01:17:48.000
Das ist nämlich hier nicht in allgemeiner Form eingeführt.

01:17:48.660 --> 01:18:04.670
Es gilt Folgendes, dass die in einem früheren Schritt, also

01:18:04.670 --> 01:18:12.730
Ableitungsschritt, die in einem früheren Ableitungsschritt des

01:18:12.730 --> 01:18:26.610
Beweises abgeleiteten Aussagen dürfen,

01:18:36.840 --> 01:18:49.280
zu der Ableitung weiterer Aussagen verwendet werden.

01:18:50.500 --> 01:18:55.700
Und das ist das, was wir hier genau gemacht haben, verwendet werden.

01:18:57.960 --> 01:19:04.540
Konkret heißt das, dass Sie hier, wenn Sie was abgeleitet haben, diese

01:19:04.540 --> 01:19:09.120
abgeleiteten Aussagen in die Hypothesenmenge mit aufnehmen können.

01:19:09.180 --> 01:19:13.400
In der Hypothesenmenge stecken sozusagen die schon insofern, wenn Sie

01:19:13.400 --> 01:19:19.000
zumindest ein korrektes Kalkül haben, die bislang als gültig

01:19:19.000 --> 01:19:21.010
aufgezeigten Aussagen.

01:19:21.010 --> 01:19:24.530
Das ist genau das, was wir hier gemacht haben, das kann man also in

01:19:24.530 --> 01:19:26.450
folgender Form nochmal verallgemeinern.

01:19:26.530 --> 01:19:36.990
Wenn ich aus H T1 ableite, im nächsten Schritt kann ich dieses T1

01:19:36.990 --> 01:19:42.870
sozusagen in die Hypothesenmenge mit aufnehmen und das mitverwenden,

01:19:43.170 --> 01:19:48.470
um zum Beispiel jetzt einen anderen Term T2 abzuleiten.

01:19:49.270 --> 01:19:53.770
Und das führt dann, wenn Sie das eben dann weiter betreiben, dass Sie

01:19:53.770 --> 01:20:02.570
irgendwie eine T1 bis Tn und daraus können Sie dann eben ein Tn plus 1

01:20:02.570 --> 01:20:05.550
ableiten.

01:20:06.350 --> 01:20:13.550
Das heißt, Sie können dann auch hinschreiben, aus H können Sie das Tn

01:20:13.550 --> 01:20:15.250
plus 1 ableiten.

01:20:15.410 --> 01:20:22.510
Aus H haben Sie erst mal das T1, gegebenenfalls das T2 und so weiter

01:20:22.510 --> 01:20:23.650
abgeleitet.

01:20:23.770 --> 01:20:27.370
Und hier nehmen Sie natürlich auch wieder das T1 bis Tn zur Hilfe, um

01:20:27.370 --> 01:20:31.030
das Tn plus 1 abzuleiten, weil Sie ja sozusagen ein ganz mechanisches

01:20:31.030 --> 01:20:33.050
Vorgehen hier zugrunde legen.

01:20:35.670 --> 01:20:40.930
Letztendlich genau diese Art des Vorgehens haben wir jetzt hier an der

01:20:40.930 --> 01:20:42.430
Stelle verwendet.

01:20:43.170 --> 01:20:48.510
Und wir kommen also jetzt hier zu dem formalen System oder Theorie

01:20:48.510 --> 01:20:49.950
oder Kalkül.

01:20:51.210 --> 01:20:52.310
Das ist der dritte Begriff.

01:20:53.530 --> 01:20:57.110
Das ist nämlich die Aktionmenge und die Menge von Ableitungsregeln.

01:20:58.090 --> 01:21:04.210
Aktionmenge, das sind die Aussagen, die wir als wahr annehmen, in

01:21:04.210 --> 01:21:04.970
denen wir ausgehen.

01:21:05.750 --> 01:21:09.070
Und die Theoreme, das was wir hier ableiten, das ist eben die Menge

01:21:09.070 --> 01:21:10.230
der ableitbaren Formeln.

01:21:10.810 --> 01:21:13.570
Das sind also nochmal die Begriffe hier ergänzt.

01:21:14.110 --> 01:21:18.170
Und jetzt kommen wir zur Frage, zur Eigenschaft der Konsistenz oder

01:21:18.170 --> 01:21:19.790
Inkonsistenz einer Theorie.

01:21:23.730 --> 01:21:30.070
Und wir nennen eine Theorie oder auch ein formales System, das sind ja

01:21:30.070 --> 01:21:35.790
gleichbedeutende Begriffe, das nennen wir inkonsistent, falls wir jede

01:21:35.790 --> 01:21:37.910
Formel ableiten können.

01:21:37.910 --> 01:21:43.030
Wenn wir jede Formel ableiten können, dann können wir insbesondere

01:21:43.030 --> 01:21:50.170
ableiten aus dieser Hypothesenmenge, können wir nämlich T ableiten und

01:21:50.170 --> 01:21:53.790
dann können wir auch nicht T ableiten.

01:21:54.090 --> 01:21:54.650
Das heißt das.

01:21:56.290 --> 01:22:01.450
Ich kann also sowohl einen Term als auch die Negation dieses Termes

01:22:01.450 --> 01:22:01.950
ableiten.

01:22:02.650 --> 01:22:11.510
Und letzten Endes führt das dazu, dass ich auch Falls ableiten kann.

01:22:12.390 --> 01:22:14.510
Ich kann True ableiten, ich kann Falls ableiten.

01:22:15.070 --> 01:22:18.470
Ich kann also alles ableiten und dann kann man sich schon vorstellen,

01:22:18.630 --> 01:22:23.210
dass die Konsistenz nicht gewahrt ist.

01:22:23.790 --> 01:22:27.470
Das nennen wir an der Stelle inkonsistent, inkonsistente Theorie.

01:22:27.470 --> 01:22:33.570
Und das Theorem, was wir jetzt sehr einfach auch beweisen können, ist

01:22:33.570 --> 01:22:38.470
das folgende, dass wir in einer Theorie der Aussagenlogik, falls wir

01:22:38.470 --> 01:22:47.070
hier das Falls ableiten können, dann ist automatisch dieses Kalkül

01:22:47.070 --> 01:22:51.790
oder diese Theorie inkonsistent oder gleichbedeutend mit der

01:22:51.790 --> 01:22:53.670
Definition von Inkonsistenz.

01:22:54.030 --> 01:22:57.530
Jede Aussage T ist damit ableitbar.

01:22:58.410 --> 01:23:03.310
Und diesen Schluss können wir nämlich ziehen aufgrund der Tatsache,

01:23:05.530 --> 01:23:10.430
dass wir aus Falls jeden beliebigen Term T ableiten können.

01:23:10.510 --> 01:23:11.050
Das steht hier.

01:23:11.690 --> 01:23:15.190
Aus Falls können wir jeden beliebigen Term T ableiten.

01:23:15.990 --> 01:23:21.590
Und den Beweis, den kann man natürlich jetzt von vorne nach hinten

01:23:21.590 --> 01:23:23.470
versuchen, das nochmal nachzuvollziehen.

01:23:23.830 --> 01:23:29.010
Wenn Sie den selber aufstellen, wenn Sie den selber sich entwickeln

01:23:29.010 --> 01:23:32.450
wollen, dann sollten Sie von unten nach oben anfangen.

01:23:32.810 --> 01:23:37.710
Nämlich das ist genau, wie man hier die Beweisschritte sehr schnell

01:23:37.710 --> 01:23:38.750
und einfach erkennt.

01:23:39.350 --> 01:23:43.650
Erstmal starten wir hier von dem, was wir ja sozusagen rauskriegen

01:23:43.650 --> 01:23:49.150
wollen, dass wir aus Falls einen beliebigen Term T ableiten können.

01:23:49.250 --> 01:23:51.890
Über T machen wir keine Aussage, T ist ein beliebiger Term.

01:23:53.650 --> 01:23:57.850
Und jetzt kommen wir erstmal zu diesem Schritt hier, also zu dieser

01:23:57.850 --> 01:24:02.990
Zeile, genau durch unser vorhergehendes Lemma.

01:24:04.770 --> 01:24:06.650
Das ist die Anwendung unseres Lemmas.

01:24:06.650 --> 01:24:15.810
Nämlich in der Form, dass wir hier aus, wenn Sie das mal einsetzen,

01:24:17.370 --> 01:24:24.850
aus der leeren, also da ist die Hypothesenmenge leer, Falls vereinigt

01:24:24.850 --> 01:24:37.200
T, können wir daraus folgt, dass Falls T ableitbar ist.

01:24:37.200 --> 01:24:42.180
Was wir hier letztendlich machen ist, vom Beweisvorgehen her ist ja

01:24:42.180 --> 01:24:47.520
so, dass wir diesen Schritt, also diese Richtung nachweisen müssen.

01:24:47.860 --> 01:24:50.400
Wir gehen ja von oben nach unten in der Beweisführung.

01:24:50.820 --> 01:24:53.820
Diese Richtung haben wir ja jetzt nur ausgewählt, von unten nach oben,

01:24:53.880 --> 01:24:55.040
um den Beweis zu verstehen.

01:24:55.760 --> 01:25:00.200
Aber wir kommen hier genau, also in diese Richtung setzen wir das

01:25:00.200 --> 01:25:00.720
Lemma ein.

01:25:00.720 --> 01:25:10.740
Und das ist genau das Einsetzen von den verschiedenen Komponenten des

01:25:10.740 --> 01:25:11.060
Lemmas.

01:25:11.200 --> 01:25:13.580
Und dann kommen Sie genau zu dieser Aussage.

01:25:13.960 --> 01:25:19.720
Was Sie jetzt noch machen ist, an der Stelle an dem Falls zu arbeiten.

01:25:20.540 --> 01:25:27.200
Und hier wird jetzt sozusagen der Implikationspfeil aufgelöst.

01:25:28.080 --> 01:25:33.120
Sie kommen dann, setzen Sie das Falls, da setzen Sie nicht True ein.

01:25:33.840 --> 01:25:37.640
Dann kommen Sie zu diesem Bulschen Term.

01:25:38.060 --> 01:25:41.060
Und was Sie jetzt sehen, wenn Sie hier weiter nach oben gehen, Sie

01:25:41.060 --> 01:25:46.580
machen eigentlich nichts anderes als irgendwelche Umformungen im

01:25:46.580 --> 01:25:50.780
Rahmen der Bulschen Algebra, auf der Ebene der Bulschen Terme.

01:25:50.780 --> 01:26:02.100
Und Sie kommen dann zu einer Aussage, die in dem Kalkül immer gültig

01:26:02.100 --> 01:26:06.580
ist, laut dem Tertium Non Dator, wo Sie also gar keine Hypothese für

01:26:06.580 --> 01:26:07.000
brauchen.

01:26:08.060 --> 01:26:19.140
Und das ist genau, was Ihr Ziel ist, dass Sie nämlich zu einer Aussage

01:26:19.140 --> 01:26:22.620
kommen, die also immer Gültigkeit hat, T oder nicht T.

01:26:23.100 --> 01:26:31.100
Und wenn Sie diesen Beweis von oben nach unten nachempfinden, dann

01:26:31.100 --> 01:26:37.260
können Sie also hier auch rausbekommen, wie Sie sozusagen dieses

01:26:37.260 --> 01:26:38.460
Theorem beweisen können.

01:26:38.800 --> 01:26:41.260
Gut, ich werde an der Stelle das nächste Mal noch fortsetzen.

01:26:41.400 --> 01:26:43.920
Wir werden das nächste Mal, das möchte ich vielleicht noch kurz

01:26:43.920 --> 01:26:48.260
ankündigen, weil es ja die letzte Veranstaltung vor Weihnachten ist,

01:26:48.340 --> 01:26:49.580
die etwas kürzer gestalten.

01:26:52.520 --> 01:26:57.480
Das heißt, der Herr Scholderer wird also wahrscheinlich so nach 40, 45

01:26:57.480 --> 01:27:02.460
Minuten übernehmen, dass wir voraussichtlich am Mittwoch in 1,5

01:27:02.460 --> 01:27:04.300
Stunden durch sind, auch mit der zentralen Übung.

01:27:04.720 --> 01:27:04.960
Danke.