Definition:Freely Substitutable
Jump to navigation
Jump to search
Definition
Let $\mathbf C$ be a WFF of predicate logic.
Let $x$ be a variable in $\mathbf C$.
Let $\phi \left({y_1, \ldots, y_n}\right)$ be a term in which the variables $y_1, \ldots y_n$ occur.
Then $\phi \left({y_1, \ldots, y_n}\right)$ is freely substitutable for $x$ in $\mathbf C$ if and only if no free occurrence of $x$ occurs in a well-formed part of $\mathbf C$ which is of the form:
- $( Q y_i: \mathbf B )$
where $Q$ is a quantifier and $\mathbf B$ is a WFF.
Also known as
One often sees free for as a convenient abbreviation for freely substitutable for.
Also see
- Confusion of Bound Variables, showing what goes wrong when substituting a variable that is not free for another.
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.3$
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\mathrm{II}.8$ Further Semantic Notions: Definition $\mathrm{II.8.9}$