substitutions in propositional logic
Uniform Substitution
One area of mathematics where substitution plays a prominent role is mathematical logic. In this entry, we are mainly interested in propositional logic. Recall that a substitution is a function preserving the empty word and concatenation. In a propositional logic, has the following additional characteristics:
-
•
only one alphabet , often infinite, consisting of all propositional variables, logical connectives, and parentheses, is involved;
-
•
maps to singletons, so we might as well think of as mapping into ;
-
•
fixes the logical connectives and parentheses;
-
•
is a set of well-formed formulas (rather than a set of words over ).
is also called a uniform substitution because for any propositional variable that occurs in , replaces each and every occurrence of in by . In practice, we write
to mean change all occurrences of in by , and leave all other variables fixed. This includes the case when does not occur in , in which case . corresponds to a substitution that sends to and fixes all variables in not equal to . This is called an individual substitution. More generally,
means: change all occurrences of in to , for each , and leave all other variables fixed. This is called a simultaneous substitution, and corresponds to a substitution that sends to and fixes all other variables in . Simultaneous substitutions are not the same as iterated individual substitutions:
For example, if , then .
Recursive Definition of Substitution
Substitutions can also be defined inducitvely, starting from propositional variables. For the sake of simplicity, we only define uniform substitutions on one variable.
Definition. Suppose and are wff’s, and a propositional variable. Then
-
1.
is a propositional variable. If is , then . Otherwise, .
-
2.
-
3.
If is , then .
-
4.
If is , then .
-
5.
If is , then .
Since is , we see that is . In addition, if the language of the logic contains a modal connective, say , we have
-
6.
If is , then .
Sets Closed under Uniform Substitution
A set of wff’s is said to be closed under uniform substitution if for any , for any (uniform) substitution . We also say the set is closed under US (for uniform substitution), or obeys the rule of US. The smallest set containing a wff that is closed under US is called a schema based on , and is denoted by , the bold face version of . An element of is called a substitution instance, or simply an instance of . For example, if is , where and are propositional variables, then
is a substitution instance of , where is replaced by and by .
It is easy to see that a set is closed under US iff it is closed under individual substitution (IS). Obviously, one direction is clear, as IS is just special case of US. Conversely, suppose , which is closed under IS. Let be all the propositional variables in , and are arbitrary wff’s. Let be propositional variables, none of which occur in any of . Then
There are in general two ways to specify a given axiom system for a propositional logic:
-
•
list wff’s as axioms, and as inference rules, including US, or
-
•
list schemas as axiom schemas, and as inference rules, excluding US
Both specifications are equivalent, in that they produce the same set of theorems.
Non-Uniform Substitution
It is also possible to consider substitutions that only replace some, but not all, occurrences of a propositional variable in a formula , or replace a variable at different locations in by different formulas. For example, if is , then
-
•
is obtained by replacing the first occurrences of and by ;
-
•
is obtained by replacing the first and second occurrences of by and respectively.
Replacements such as these are called non-uniform substitutions. Technically, these are no longer substitutions, for they are no longer functions on , as individual variables may be mapped to different things depending on their location in the formula. In the first example above, is mapped to both and , depending on whether it is the first or second occurrence in .
To present a non-uniform substitution, let be the list all the propositional variables in in order. Note that since a propositional variable may occur multiple times in , may occur multiple times in . Suppose each is replaced by . Let be the list . Then we denote
by this non-uniform substitution. In the two examples above, is the first wff, while is the second.
Nevertheless, non-uniform substitution is useful in one respect: preservation of theoremhood. This fact is the famous substitution theorem, which says, if are all the propositional variables (not necessarily distinct) in a wff that are listed in order of appearance in , then replacing each variable by deductively equivalent formulas produces equivalent result. In short, if for , then
A set closed under non-uniform substitution (NUS) is defined in the same way as that of uniform substitution. It is easy to see that the smallest set closed under NUS containing the formula is the schema , where is a list of pairwise distinct propositional variables. For example, the smallest set closed under NUS containing is . It is not hard to see that if the NUS closure of a formula is used as an axiom schema for a logic, with modus ponens as a rule of inference, then the logic is inconsistent.
First Order Logic
In a first order logic, substitutions are more complicated. Given a wff , does not necessarily mean replacing all occurrences of by . Here, again, a substitution is no longer a substitution in the sense above. In fact, replacements of symbols, like non-uniform substitutions, are conditional on the locations of the symbols in the wff . These conditions are collectively known as the substitutability of a term for the variable , and is discussed in more detail here (http://planetmath.org/Substitutability).
Title | substitutions in propositional logic |
Canonical name | SubstitutionsInPropositionalLogic |
Date of creation | 2013-03-22 19:32:41 |
Last modified on | 2013-03-22 19:32:41 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 22 |
Author | CWoo (3771) |
Entry type | Definition |
Classification | msc 03B99 |
Synonym | instance |
Synonym | US |
Related topic | Substitutability |
Defines | simultaneous substitution |
Defines | uniform substitution |
Defines | schema |
Defines | substitution instance |