equivalent formulation of substitutability
Proposition 1.
Suppose a variable x occurs free in a wff A. A term t is free for x in A iff no variables in t are bound by a quantifier in A[t/x].
Proof.
We do induction on the complexity of A.
-
•
If A is atomic, then any t is free for x in A, and clearly A[t/x] is just A, which has no bound variables.
-
•
If A is of the form B→C, then t is free for x in A iff t is free for x in both B and C iff no variables in t are bound in either B or C iff no variables in t are bound in A.
-
•
Finally, suppose A is of the form ∃yB. Since x is free in A, x is not y, and t is free for x in A iff y is not in t and t is free for x in B iff, by induction, y is not in t and no variables of t are bound in B[t/x] iff no variables of t are bound in ∃yB[t/x], which is just A[t/x] (since x≠y).
∎
If x does not occur free in A (either x occurs bound in A or not at all in A), then t is obviously free for x in A, but A[t/x] is just A, and there is no guarantee that variables in t are bound in A or not.
In the special case where t is a variable y, we see that y is free for x in A iff y is not bound in A[y/x], provided that x occurs free in A. In other words, y is free for x in A iff no free occurrences of x in A are in the scope of Qy, where Q is either ∃ or ∀. So if y is not bound in A, y is free for x in A, regardless of whether x is free or bound in A. Also, x is always free for x in A.
Title | equivalent formulation of substitutability |
---|---|
Canonical name | EquivalentFormulationOfSubstitutability |
Date of creation | 2013-03-22 19:35:57 |
Last modified on | 2013-03-22 19:35:57 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 6 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 03B05 |
Classification | msc 03B10 |
\@unrecurse |