Ja, herzlich willkommen. Entgegen anders lautenden Gerüchten sind wir durch das Informatiker und

deswegen schmeißen wir auch gerne ab und zu mal Maschinen an, natürlich immer nur mit komischen

Dingen, also auch dieses Mal wieder mit KOK. Wir haben ja jetzt mehr gelernt letztes Mal,

was nun also die Geschichte mit den formalen Herleitungen angeht. Und insbesondere können

wir jetzt also formale Herleitungen führen in voller propositionaler Logik erster Stufe.

Das bringt jetzt KOK nicht weiter in Bedrängnis, die Ausdrucksstärke von KOK liegt,

weiß jetzt gar nicht wie viele Stufen oberhalb von Prädikatenlogik erster Stufe, ich würde mal

grob gesagt sagen drei oder so was. Das ist also alles ohne Mühe hier noch drin. Und ja,

wir sehen das jetzt einfach mal an zwei Beispielen an. Das Interface kennen Sie ja wahrscheinlich

schon. Wie auch im aussagenlogischen Fall fangen wir damit an, dass wir klassische Logik importieren,

das ist also in KOK nicht standardmäßig voreingestellt, dass die Logik klassisch ist,

aber man kann es einfach dann dekretieren. Es kommen jetzt so ein paar technische Einzelheiten,

die im Moment noch nicht völlig verständlich sein werden, erst dann, wenn die heutige Sitzung

vorbei ist und wir die Semantik von Logik erster Stufe eingeführt haben. Es hilft trotzdem,

sich jetzt schon mal vorzustellen, dass Logik erster Stufe, die ja keinen expliziten Grundbereich

hat, wenn ich einen Quantor anschmeiße für alle x oder existiert x, dann ist es anders, als man das

vielleicht aus der Mengenlehre oder so gewohnt ist, nicht dabei gesagt alle x aus was denn,

gemeint ist eben alle x schlechthin. Wenn man das jetzt in so einer Ausdrucksstärke,

in Logik wie KOK modelliert, die also explizite Typen gewohnt ist, eben also eher wie Mengenlehre

ist, als die Logik erster Stufe, dann muss man eben diesen Grundbereich, über den man redet,

den muss man explizit einführen und das geschieht, indem da oben eine Menge d explizit eingeführt

wird. Die werden Sie gleich in der Semantikdefinition wiedererkennen. Das d steht für Domain,

also Englischbereich, also der Grundbereich, über den geredet wird. So, wir wollen reden zunächst

mal über eine Formel, die ein einziges Prädikat, groß p, erwähnt und Prädikat heißt dann, gut es

ist in diesem Falle ein binäres Prädikat, das hier aufgeschrieben ist in dieser sogenannten

Curry-Schreibweise, das heißt also statt hier etwas hinzuschreiben, was zwei Argumente nimmt,

schreiben wir eine Funktion hin, die nimmt ein Argument vom Typ d und ist dann aber nicht zufrieden,

sondern will noch ein zweites Argument, das heißt also, wenn ich die Funktion angewendet habe auf

dieses Argument aus d, dann kommt raus, das ist rechtsrum geklammert zu lesen, ich schreibe die

Klammern vielleicht mal scherzishalber explizit hin, ist also so rum geklammert zu lesen, dann kommt

also raus eine weitere Funktion und nicht etwa schon ein Wert, das heißt, um dann wirklich ein

Wert zu kriegen, muss man dieser Funktion noch ein zweites Argument anfüttern, das heißt eine

solche Funktion hier ist erkennbar, dasselbe wie eine Funktion mit zwei Argumenten, sie erlaubt nur

etwas flexiblere Schreibweisen, zum Beispiel kann ich sie auf nur ein Argument anwenden, wenn ich will.

So und was dann rauskommt am Ende ist vom Typ prop, sprich ein Wahrheitswert, das ist also jetzt

gesamtermaßen eine bultische Funktion mit zwei Argumenten, also ein Prädikat. Gut, wir lesen das

mal bis dahin ein und zu gucken, ob es schluckt. Okay, p is assumed ist jetzt so ein bisschen

irreführend, also es wird angenommen als ein Bewohner dieses Typs hier D nach D nach prop.

Es ist nicht etwa jetzt hier gemeint, dass angenommen wird, dass p für irgendwas tatsächlich

gilt oder sowas. So und jetzt schreiben wir hier unser Theorem hin, das man nicht vollständig

erkennen kann im Moment, das machen wir kurz mal hier breiter. So das Theorem ist etwas, was wir

letzte Stunde schon bewiesen hatten und zwar sogar eben in natürlichem Schließen bewiesen hatten,

das ist jetzt Absicht, damit man also den Beweis hier halbwegs wieder erkennt. Also was sagt das

Theorem, das Theorem sagt, wenn es ein y gibt, das zu allen x in dieser Relation p steht, p war

letztes mal, kannst ja entsprechend hier mal vielleicht auch austauschen, also nehmen wir

stattdessen mal k, das sollst du da auch machen, da auch und natürlich hier unten später. So,

das war's. So, nicht k wie kennt, das ist jetzt passiert. Das heißt hier, wir wollen zeigen,

wenn es also jemanden gibt, den alle kennen, dann kennt jeder irgendjemanden. Haben wir uns

letztes mal schon überlegt, nämlich mindestens den einen, den sowieso alle kennen. So, ja wir

lesen das Theorem mal ein. So, jetzt machen wir wieder schmaler, damit man die Scheiben rechts