substitution theorem for propositional logic
In this entry, we will prove the substitution theorem for propositional logic based on the axiom system found here (http://planetmath.org/AxiomSystemForPropositionalLogic). Besides the deduction theorem, below are some additional results we will need to prove the theorem:
-
1.
If and , then .
-
2.
and iff .
-
3.
.
- 4.
-
5.
(ex falso quodlibet)
-
6.
implies iff .
The proofs of these results can be found here (http://planetmath.org/SomeTheoremSchemasOfPropositionalLogic).
Theorem 1.
(Substitution Theorem) Suppose are all the propositional variables, not necessarily distinct, that occur in order in , and if are wff’s such that , then
where is the wff obtained from by replacing by the wff via simultaneous substitution.
Proof.
We do induction on the number of in wff .
If , is either a propositional variable, say , or , which respectively means that is either or . The former is the assumption and the latter is a theorem.
Suppose now has occurrences of . We may write as uniquely by unique readability. Also, both and have at most occurrences of .
Let be and be . Then is and , where is , is , is , and is .
Then
by induction | (1) | |||
by 2 above | (2) | |||
by induction | (3) | |||
by 2 above | (4) | |||
(5) | ||||
(6) | ||||
(7) | ||||
by the deduction theorem | (8) | |||
by a similar reasoning as above | (9) | |||
(10) |
∎
As a corollary, we have
Corollary 1.
If , then , where is a propositional variable that occurs in , is a set of positions of occurrences of in , and the wff is obtained by replacing all that occur in the positions in in by wff .
Proof.
For any propositional variable not being replaced, use the corresponding theorem , and then apply the substitution theorem. ∎
Remark. What about , given ? Here, and are wff’s obtained by uniform substitution of (all occurrences of ) in and respectively. Since is just , an instance of the schema by assumption, the result follows directly if we assume is a theorem schema.
Using the substitution theorem, we can easily derive more theorem schemas, such as
-
7.
(Law of Contraposition)
-
8.
-
9.
(Peirce’s Law)
Proof.
-
7.
Since is already a theorem schema, we only need to show . By law of double negation (4 above) and the substitution theorem, it is enough to show that . But this is just an instance of an axiom schema. Combining the two schemas, we get .
-
8.
First, observe that by modus ponens. Since , we have by the substitution theorem. So by the deduction theorem, and by the deduction theorem again. Apply the deduction two more times, we get .
-
9.
To show , it is enough to show by and modus ponens, or by the deduction theorem. Now, since (as they are the same thing, and because is a theorem schema), by the law of double negation and the substitution theorem, , and we have . So to show , it is enough to show , which is enough to show that and , according to a meta-theorem found here (http://planetmath.org/SomeTheoremSchemasOfPropositionalLogic). To show , it is enough to show , and is such a deduction. The second statement is clear.
∎
As an application, we prove the following useful meta-theorems of propositional logic:
Proposition 1.
There is a wff such that and iff
Proof.
Assume the former. Let be a deduction of from and a deduction of from , then
is a deduction of from . Conversely, assume the later. Pick any wff (if necessary, pick ). Then by ex falso quodlibet. By modus ponens, we have . Similarly, . ∎
Proposition 2.
If and , then
Proof.
By assumption, we have and . Using modus ponens and the theorem schema , we have , or
Similarly, . By the law of double negation and the substitution theorem, we have , or
By the previous proposition, , or . Applying the substitution theorem and the law of double negation, we have
∎
Title | substitution theorem for propositional logic |
---|---|
Canonical name | SubstitutionTheoremForPropositionalLogic |
Date of creation | 2013-03-22 19:33:08 |
Last modified on | 2013-03-22 19:33:08 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 17 |
Author | CWoo (3771) |
Entry type | Result |
Classification | msc 03B05 |
Related topic | AxiomSystemForPropositionalLogic |
Defines | substitution theorem |