substitutability
In any logical system, the way to obtain (well-formed) formulas from existing ones is by attaching logical connectives to existing ones. For example, in classical propositional logic, if and are formulas, the following
are formed by attaching logical connectives , and appropriately to and .
Another convenient device is substitution:
replace all occurrences of some symbol in a formula by an expression .
We denote the resulting expression by
For example, in classical propositional logic, if is , then is
On the other hand, the expressions
-
•
, which is , and
-
•
, which is ,
are not formulas. Thus, one must be careful when performing substitutions on formulas lest the resulting expressions are ill-formed. In other words, conditions must be placed on and in in order that is a (well-formed) formula. These conditions are called the substitutability conditions. In this entry, we will concentrate on substitutability conditions on predicate logic. Details on substitions in propositional logic can be found in here (http://planetmath.org/SubstitutionsInLogic).
Substitution in First-Order Logic
Substitution works pretty much the same way for first-order logic as in propositional logic. However, the substitutability conditions are more subtle. Take a look at the following example:
If we replace by , we end up with
which is non-sensical (not a wff). This is because occurs in the formula as a bound variable. (one reason why we distinguish the variables occurring in first order formulas into two types: free and bound).
We now formalize the notion of substitution in first-order logic. There are two parts: substitution for terms, and substitution for formulas.
Definition. For any term , any symbol , and any expression , define inductively, as follows:
-
1.
if is an individual variable or a constant symbol, then is if is , and is otherwise;
-
2.
if is , where is an -ary function symbol, and each is a term, then is .
For example, if is , then is .
It is easy to see that is a term and an individual variable, then is a term. In addition, by induction, one can easily show that if the formula is true, so is the formula .
Next, we define substitution for formulas. In light of the last example at the beginning of this section, we need to be a little careful.
Definition. Let be a formula, a symbol, and an expression. The expression is again define inductively:
-
1.
if is , then is ;
-
2.
if is , then is ;
-
3.
if is , then is ;
-
4.
if is , then is ;
-
5.
if is , then is if , and is otherwise.
Again, substitutions involving logical connectives , , and the universal quantifier can be derived from the rules given above.
For example, if is , then is , whereas is just .
Given that is a formula, it is easy to see that if is an individual variable, and is a term, then is a formula.
In addition, it is easy to see that sentences are not affected by substitutions: if is a sentence, then is just . In other words, sentences can not be changed into formulas with free variables.
Conversely, can a formula with free variables be changed into a sentence by substitution? Certainly. For example, if is
then is
Although syntactically correct, this is undesirable in many situations, particularly when we are interested in the interpretations of these formulas. In the example above, we have changed , which many very well be true in many interpretations, into , something with a fixed meaning (and always false if is interpreted as the usual less than relation).
The problem with the situation described in the last paragraph arises because a free variable in becomes bound in . To eliminate this undesirable situation, we define the notion of “free for”:
Definition. Let be an individual variable, a term, and a formula. We define the relation is free for, or substitutable for in , inductively, as follows:
-
1.
is an atomic formula;
-
2.
is , and is free for in ;
-
3.
is , and is free for in and in ;
-
4.
is , and either
-
–
( does not occur free in ), or
-
–
does not occur in , and is free for in .
-
–
In words, is free for in iff whenever is a variable in , no literal subformula of of the form contains an occurrence of which is free in .
For example, is free for in the following formulas:
but not in the following formulas:
Given any formula , we again write to mean that variable occurs in . A substitution instance of is just , or for short. Furthermore, if is free for in , then is called a free substitution instance of .
It is easy, by induction, to show that if terms and are free for in , and that the formula is true, the substitution instances and are logically equivalent, as intended.
Title | substitutability |
Canonical name | Substitutability |
Date of creation | 2013-03-22 19:12:15 |
Last modified on | 2013-03-22 19:12:15 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 24 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 03B10 |
Classification | msc 03B05 |
Synonym | substitutable for |
Related topic | Subformula |
Related topic | FreeAndBoundVariables |
Defines | free for |
Defines | free substitution instance |