Frage? Ach nee, wollte ja mein Pointer noch haben.

So wir sind tief abgestiegen am Montag in die in gewisser Weise Theorie der Logik

erster Stufe und sind dann hinterher bis zu den Anfängen der Kalküle erster Stufe gekommen.

Wir waren angefangen mit Substitutionen und hatten uns eine Stunde davor das Substitutionswertlemmer

angeguckt und das ist dieses Lemmer das sagt wenn man den Wert einer Instanz von A ausrechnet,

dann kann man das machen indem man den Wert von A ausrechnet wenn man den Wert von B für

X in die Valuation reinsteigen. Das heißt so eine Kommunitationseigenschaft und die werden wir jetzt

für die Korrektheit der Kalküle immer mal wieder brauchen. Wir haben uns als nächstes dann

angeguckt natürliche Schließen für die Logik erster Stufe. Wir haben wie wir es erwarten würden in

diesem Kalkül des natürlichen Schließen vier neue Regeln für jeden Quantor eine, eine Einführungsregel

und eine Eliminationsregel. Man kann ein Quantor einführen wenn man für ein beliebiges X etwas weiß

wobei beliebig eben gerade wichtig ist dass das X nicht in irgendeiner Annahme vorkommt denn das

würde ja die Beliebigkeit von X einschränken dann kann man für alle XA schließen und wenn ich weiß

was für alle XA ist kann ich für ein beliebiges Term kann ich einsetzen für X. Dual dazu die

Existenz Einführung wenn ich für irgendeinen Zeugen B weiß das A gilt kann ich sagen es gibt

ein XA. Wenn Peter schläft und Peter ein Student ist dann weiß ich es gibt einen Student der schläft

und wir haben die Existenz Elimination wenn wir wissen dass es ein X gibt so das A gilt dann kann

ich diesem X einen neuen Namen geben kann das durch eine lokale Konstante ersetzen und alles was ich

aus dieser zusätzlichen Annahme schließen kann kann ich auch allgemein schließen weil ich weiß

ja es gibt ein X das ist oft sehr wichtig wenn man mit den Dingen arbeitet. Das ist so der Kalkül

den wir haben für das natürliche schließen und das ist so die Grundlage dessen was man

mathematische Beweisungs nennt wir haben uns dann eine Sequenzen schreibweise angeguckt wo man sagt

ich werde die ich werde die Annahmen die ich gerade habe diese Art von Annahmen die schreibe ich

einfach als Gamma irgendwie vor den Nagel und da kann man dann genau sehen wo die Annahmen

zusätzlich eingeführt werden und wo sie wieder verschwinden. So eine andere Art und Weise diesen

Kalkül zu schreiben und wir haben hier die Regeln in dieser schreibweise und was ich eigentlich

wollte damit ist dass wir uns hinterher angucken wie man Beweise erster stufe zum Beispiel irgendwie

linear aufschreiben kann. Dies hier ist im wesentlichen die Form in der dann auch Beweissysteme

in Beweise anzeigen. In irgendeiner solchen Form ist das typischerweise und wir finden solche

Beweise solche Systeme die mit die interaktiv Beweise bauen können sind in so was wie der

Programmverifikation der Stand der Kunst. Da setzt man sich hin und bastelt solche Biester nicht

für die Irrationalität von Wurzel 2 sondern davon dass irgendwie in der Kommunikation im

Kommunikationsprotokoll zwischen innen und der Bank es nie gelingen kann einem außen dass es

keinen Außenstehenden gibt der irgendwie von ihrem Konto Geld abheben kann. Solche Sachen sind da

interessant aber sie bauen letztlich solche Beweise auf im Kalkül des natürlichen Schließens.

Und das System macht in solchen Systemen im wesentlichen dass es Schritt für Schritt nachprüft

stimmen die Inferenzregeln überein. Das ist also dann so etwas wie ein Beweisprüfer das kann man sehr leicht

implementieren denn alles was man implementieren muss ist das da Transformationsregeln. Die sind

sind einfach und dann kann man irgendwie sagen ein solcher Beweis ich habe jeden Schritt geprüft.

Der Beweis ist tatsächlich. Im Prinzip ist das der Stand der Kunst außer natürlich dass man für

echte industrielle oder auch akademische Anwendungen dass man da größere Beweise hat und

auch natürlich stärkere Logik. Weil man viele es gibt Sachen die man in der Logik erster stufe

nicht ausdrücken kann. Und aber im Prinzip ist das dasselbe. Um ihnen so ein bisschen eine

Größenordnung zu geben. Es hat in der Mathematik jetzt zwei größere Beweise gegeben. Also einerseits

hat haben Leute in Frankreich das Pfeiff-Thomson Theorem bewiesen. Das war so eine Sache wo sich

etwa sechs bis acht Leute für sechs bis acht Jahre hingesetzt haben und gemeinsam einen großen

Beweis gebaut haben. Und dann gibt es mittlerweile einen Beweis der Kepler Vermutung. Kepler Vermutung

ist das das kennen sie wenn sie wenn sie Orangen stapeln. Dann so dass man so so Pyramidal die

aufbaut. Man macht vier Mal vier Orangen und dann macht man da in die Zwischenräume drei mal drei

und dann zwei mal zwei und dann oben eine drauf. Und es gab lange Zeit und das hat Kepler schon