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:
If and , then .
and iff .
(ex falso quodlibet)
implies iff .
The proofs of these results can be found here (http://planetmath.org/SomeTheoremSchemasOfPropositionalLogic).
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 .
|by 2 above||(2)|
|by 2 above||(4)|
|by the deduction theorem||(8)|
|by a similar reasoning as above||(9)|
As a corollary, we have
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 .
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
(Law of Contraposition)
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 .
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:
There is a wff such that and iff
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, . ∎
If and , then
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|
|Date of creation||2013-03-22 19:33:08|
|Last modified on||2013-03-22 19:33:08|
|Last modified by||CWoo (3771)|