Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Free variable Tableaux
Ich glaube das Free variable Tableaux soweit zu verstehen, habe aber noch ein paar Probleme mit der genauen Definition.
In den notes wird erwähnt, dass die witness Skolemvariable bei der exists Regel von allen Metavariablen abhängen muss, aber in der Regeldefinition wird es von allen freien Variablen abhängig gemacht. Es kann doch auch freie Variablen geben, die keine Metavariablen sind oder?
In dem Beispiel 13.1.11 auf note 429 instanziieren wir y durch a. Danach steht auf der rechten Seite q(b)T und q(a)F. Rein nach Definition sollten wir jetzt hier doch auch die false Regel anwenden dürfen, weil wir ja z.b. [a/b] als MGU finden können.
Also im wesentlichen kommt es mir so vor als ob hier freie Variablen allgemein und Metavariablen durcheinander geworfen werden…
…kann es theoretisch, wenn die Formel kein Satz ist (i.e. von vorneherein freie Variablen beinhält). In dem Fall „musst“ du zumindest semantisch eh den universellen Abschluss der Formel betrachten, dann hast du a bunch of allquantoren, die du dann loswerden musst, indem du metavariablen einführst… 
Also, tl;dr: oBdA sind alle freien variablen metavariablen 
b ist keine Variable; Konstanten darfst du nicht ersetzen