First order predicate calculus - notion of freely substitutable

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.

Quote:

---

Originally Posted by SLeviNK

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

---

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).

Thanks again! That makes a lot more sense now.