Hi everyone.
I was wondering if someone can clear something up for me.
What exactly does it take for a given term or variable to be freely substitutable in a formula.
When would it be the case that...
1. (for every x(fi(x))---> fi(x))
2. (for every x(fi(x))---> fi(y))
3. (for every x(fi(x))---> fi(t))
where fi is a formula, x is a variable in fi, y is some variable, and t is some term
And those three sentences are to be considered separately.
A term t can be substituted for a variable x in a formula φ if, after one replaces x with t, none of the variables of t are in the scope of quantifiers of φ. We are trying to avoid the situation when φ has a subformula of the form ∀y. (... x ...) or ∃y. (... x ...) and t has a free variable y. Then when x is replaced by t, the previously free y incorrectly becomes bound. For example, the formula ∃y. x < y is true for any value of x, but after we replace x with y + 1, we get ∃y. y + 1 < y, which is false. Intuitively, the existentially bound y in the formula has no relationship with y in the term y + 1, so identifying them is a mistake. If we want to substitute y + 1 for x, we need to change the bound variable from y to, say, z: ∃z. x < z; then the result of the substitution ∃z. y + 1 < z is still true for any value of y.
Do you mean, when are these formulas valid? A variable can always be replaced by itself. As for 2 and 3, they may not be valid if x occurs in the scope of ∀y or ∃y (in the case of 2), or ∀z or ∃z where z is a free variable in t (in the case of 3).Originally Posted by SLeviNK
  |
LinkBack URL
About LinkBacks