Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

So, ich beginne mit einem Nachtrag bzw. einer Korrektur zur Syntaxsitzung, in der ich definiert hatte Substitution.

So, und da bin ich in eine Anfängerfalle gefallen.

Also Substitution in eine allquantifizierte Formel ist noch etwas nicht trivialer als ich das angeschrieben hatte.

Also wir müssen auf zwei Dinge aufpassen.

Erstens, wir dürfen die gebundene Variable nicht substituieren.

Okay, daran habe ich gedacht. Woran ich nicht gedacht habe, ist also geistig auf Nachtung gewesen sein muss, das ist ein Standardpunkt.

Man muss ferner darauf achten, dass das, was man da rein substituiert, nicht die gebundene Variable erwähnt, sonst kriegt man Unsinn.

Beispiel, wenn ich also, was will ich da machen?

Ja, nehmen wir mal so eine Formel hier. Also für alle x, wenn x gleich y ist, dann gilt p von x.

Gut, das ist eine extrem unsinnige Formel, das ist dasselbe wie p von y, wenn Sie mal genau hingucken.

Aber immerhin, es ist eine legale Formel. Ich kann mir vorstellen, dass die vielleicht irgendwo innerhalb eines weiteren allquantus steht.

Und ich jetzt vielleicht mal auf die Idee komme, diesen allquantur zu spezialisieren, indem ich also für y einsetze.

Und sagen wir mal, ich will jetzt also, ich komme auf die Idee, y zu ersetzen durch x. Nun, wenn ich das naiv mache,

jetzt brauche ich wieder so eine Farbe, um anzudeuten, so grün ist giftig, also was ich jetzt mache, ist falsch. Deswegen giftgrün.

So, nicht gleich schreibe ich jetzt mal. Ja, was passiert, wenn ich das naiv mache?

Wenn ich das naiv mache, kommt heraus für alle x, so.

So war es hier, ja? Ich schreibe hier immer doppelt impliziert, ich habe einfach impliziert mal geschrieben.

So, wenn wir uns diese Formel hier ansehen, die sagt etwas völlig anderes. Jetzt ist plötzlich diese Bedingung hier x gleich x trivial.

Die können wir gleich wieder vergessen. Was hier also steht, ist für alle x gilt p von x.

Also ich kriege durch substituieren etwas, was die Bedeutung vollständig entsteht.

Ja, und das liegt natürlich daran, dass ich etwas, was ursprünglich mal eine freie Variable war, dieses x hier,

was irgendwie von außerhalb kommt, hier importiere und plötzlich verwechsel mit der hier lokal gebundenen Variable x hier etwas völlig anderes ist.

So, und da muss man also aufpassen, dass man solche Unfälle vermeidet. Wie vermeide ich die nun?

Die Namen von gebundenen Variablen, hier dieses für alle x zum Beispiel, die sind ja Schall und Rauch.

Ja, die kann ich umbenennen, ohne die Bedeutung einer Formel im Wesentlichen zu ändern.

So, wenn ich also hier so einen Clash kriege wie hier oder kriegen würde, ja, dann weiche ich den einfach aus, indem ich die Variable umbenenne.

So, das heißt, die vollständige Definition ist die folgende.

So, also, ich kann jetzt hier eine Fallunterscheidung machen, je nachdem, ob ich einen Clash kriege oder nicht.

Einfacher ist es einfach immer davon auszugehen, dass man einen Clash kriegt und vorsichtshalber mal die gebundene Variable umzubenennen.

Ja, das heißt, ich übersetze nicht, sondern ich gebe als Ergebnis an eine Formel, wo ich mal die gebundene Variable umbenenne, in y.

Ich schreibe erstmal hier grob hin, y ist eine frische Variable, eine, die ich bisher nicht erwähne.

Ich schreibe gleich noch formal hin, was das heißt.

So, und jetzt kommt hier wieder das Phi mit einer Substitution, die ist etwas anders als Sigma, die ist Sigma-Strich.

So, und zwar sage ich jetzt, wie ich dieses Sigma-Strich definiere, indem ich sage, was macht Sigma-Strich mit irgendeiner Variablen V?

Da gibt es zwei Fälle. So, ein Sonderfall ist eben dieses ursprüngliche X hier.

Mit dem mache ich etwas anderes als mit den anderen.

Das ursprüngliche X, das will ich ja eigentlich nicht ersetzen, so wie wir es letztes Mal auch geschrieben haben, weil es von außen gar nicht sichtbar ist.

So, nun will ich es aber dann und eigentlich doch ersetzen, weil ich es ja umbenenne in y.

Und das muss ich natürlich nicht nur hier im Quantor machen, das muss ich auch in dem Phi machen, sonst bekomme ich natürlich auch eine völlig andere Formel.

So, das heißt, da kommt raus y, wenn zufällig v gleich x ist.

Gut, und ansonsten substituiere ich, wie durch Sigma vorgegeben, das heißt, da kommt raus Sigma von v sonst.

Und das Ganze, wie gesagt, für ein frisches y.

Das heißt, y kommt in nichts vor, was wir da reinstecken.

Erstens nicht in Phi.

Da kann man sich auch schnell Beispiele überlegen, wo der Blödsinn rauskommt, wenn Phi schon y als freie Variable erwähnt und ich aus dieser freien Variable plötzlich die gebundene Variable mache.

Und zweitens darf y nicht vorkommen in dem, was ich da rein substituiere.

Das, was ich da rein substituiere, sind diejenigen Terme Sigma v, für die das v tatsächlich in Phi vorkommt.

Und das ist genau das Problem, von dem ich gerade sprach.

Wenn ich das hier nicht beachte, wenn ich also da eine Variable rein substituiere, also wenn ich hier einen Term rein substituiere, der schon die gebundene Variable erwähnt,