Ja, herzlich willkommen. Kleiner Rückgriff, Herr Goncharow berichtete aus der Intensivübung

das Unklarheitbestand über die genaue Aussage des Fundamentalsatzes der Arithmetik. Er steht

korrekt im Skript habe ich gerade nachgeguckt. Wie habe ich ihn hier formuliert? Habe ich gesagt

jede natürliche Zahl ist Produkt von Primzahlen oder jede positive natürliche Zahl?

Jede natürliche. Gut, also im Skript steht es korrekt jede positive natürliche Zahl. Null ist

nicht ein Produkt von Primzahlen. Es ist selbst keine und es ist auch nicht Produkt von irgendwas.

Also jede positive natürliche Zahl im Skript, das Sie online finden, steht es korrekt.

Bringt mich zum nächsten Thema. Herr Goncharow berichtete erfreut aus der Intensivübung,

dass der Besuch ungewöhnlich rege sei. Es waren sieben Leute da. Die Intensivübung ist für die

Leute gedacht, die wenn ich hier vorne Sachen erzähle oder sie sich die Übungszettel angucken

und so weiter, nicht unmittelbar das Gefühl haben, ja das verstehe ich eben mal so auf Schlagweg.

So daraus könnte man jetzt meinen schließen zu können, dass von 180 Leuten glaube ich,

die hier ungefähr für die Veranstaltung angemeldet sind, 173 dieses Gefühl haben,

das ich gerade beschrieben habe. Wenn das so ist, bin ich froh und glücklich. Wenn dem,

was ich eher erwarte, nicht ganz so ist, würde ich also denjenigen, bei denen das Gefühl,

dass sie das hier alles so unmittelbar mitnehmen, nicht ganz so folig dann doch nahelegen,

vielleicht sich bei der Intensivübung mal einzufinden. Herr Goncharow ist gerne bereit

und auch qualifiziert, ihre Fragen hoffentlich dann zu beantworten.

Formale Deduktion, wir beschäftigen uns heute also mit

einem formalen Schlusssystem für natürlich die Aussagenlogik, die unser Thema nun mal gerade ist.

Was heißt das eigentlich? Formale Deduktion. Formale Deduktion heißt, wir lösen uns für

Zwecke der Schlussfolgerung in unserer Logik von der Semantik, die wir nun letztes Mal gerade

besprochen haben, und hantieren stattdessen rein syntaktisch. Das heißt, wir haben im traditionellen

Fall ein Stück Papier vor uns, auf das kritzeln wir irgendwelche Symbole und diese Symbole

manipulieren wir nach irgendwelchen formalen Regeln, die im Prinzip nicht verlangen, dass wir

verstehen, was da bei uns auf dem Papier steht. Die verlangen nur, dass wir die Symbole lesen können,

die da auf dem Papier steht, also miteinander vergleichen, gleiche Symbole erkennen und Symbole

korrekt abschreiben. Das ist so ungefähr die Art Fähigkeit, die man dafür haben muss. Was

gleichzeitig mit sich bringt, es verlangt dann letztlich keinen menschlichen Benutzer, um solche

Formalen Deduktionen durchzuführen, sondern wenn wir das System einmal haben, kann das letztlich

auch ein Computer. Und das ist keine reine Theorie, sondern es gibt verbreitete Programme,

die das tatsächlich können und ich werde ja wahrscheinlich eher gegen Ende der heutigen

Sitzung ein solches Programm auch tatsächlich vorführen. Das ist der interaktive Theorienbeweiser

Coq mit Q am Ende benannt nach einem der Peps oder der Typentheorie Thierry Coq-Coin. Wir können

nichts dafür, dass es so heißt. Und da werde ich also ein paar formale Beweise in diesem Programm

durchführen. Solche Dinge zu tun ist auch Teil der Übungen. Also es gibt demnächst Übungen,

auf denen sie angehalten werden, eben solche Beweise in dem Programm selbst zu führen. Ich

kann daher an dieser Stelle auch nur schon mal den Tipp geben, das demnächst mal zu installieren,

auf welchem Rechner Sie ihn auch zu Hause immer so haben. Ich habe es vorhin auch auf meinem Rechner

selbst gemacht, auch wenn ich mir meinen Administrator mitbringe, um zu testen, ob hier

der Beamer funktioniert. Also selbst ich bin in der Lage, mir also dieses Programm auf meinem

Rechner zu installieren. Machen Sie es mal rechtzeitig, dass Sie also das zur Verfügung

haben, wenn es nachher an die Aufgaben geht. So. Ja, woraus besteht denn nun üblicherweise

so ein formales Deduktionssystem? Üblicherweise aus erstens Axiomen. Axiome sind Formeln,

die ich einfach so auf Papier schreiben darf, wenn ich sie gerade mal brauche. Das ist also

so ein Grundvorrat an Formeln, die halt gültig sind und die ich deswegen einfach, wenn ich sie

benötige, hernehmen darf. Und es gibt Regeln. Regeln sind also Anleitungen dafür, wie ich aus

schon hingeschriebenen Formeln, die schon auf meinem Stück Papier stehen, weitere Formeln erzeuge,

die ich ebenfalls auf Papier schreiben darf. Die Regeln kommen typischerweise von der Notation her

in einem festen Format daher. Die haben hier einen Regelstrich. Oberhalb des Regelstrichs