Klarstellung bezüglich der Substitution im Folgenkalkül

Der ursprüngliche fettgedruckte Text ist korrekt. In der Tat,$t$ist ein Term, keine Formel, und daher können darin keine Quantifizierer oder andere Bindeglieder vorkommen, also jede darin vorkommende Variable$t$ist kostenlos (in$t$) bei Notwendigkeit. Eigentlich ist Ihre Version des fettgedruckten Textes (der "kostenlos" hinzufügt) nicht falsch, sondern nur überflüssig: Das Hinzufügen von "kostenlos" ändert nichts an der Einschränkung.

Der Punkt ist, dass, wenn Sie ersetzen$t$für jedes kostenlose Auftreten von$x$In$A$, einige Variablen in$t$(die sind frei in$t$zwangsläufig, wie oben gesagt) gebunden werden können$A[t/x]$(wegen einiger Quantoren in$A$), und das gilt es zu vermeiden.

Allgemeiner gesagt ist der Begriff „frei sein“ nicht absolut, sondern immer relativ zu einem Kontext, in dem Variablen auftreten. Die freien Variablen einer Formel$A$sind die Variablen, die frei vorkommen in $A$, dh die nicht durch irgendwelche Bindemittel gebunden sind$A$. Die freien Variablen eines Terms$t$sind die Variablen, die frei sind $t$, dh die nicht durch irgendwelche Bindemittel gebunden sind$t$(was immer der Fall ist, weil es in einem Begriff in der Logik erster Ordnung keine Binder gibt).