some theorem schemas of propositional logic
Based on the axiom system in this entry (http://planetmath.org/AxiomSystemForPropositionalLogic), we will exhibit some theorem schemas, as well as prove some meta-theorems of propositional logic. All of these are based on the important deduction theorem, which is proved here (http://planetmath.org/DeductionTheoremHoldsForClassicalPropositionalLogic).
First, some theorem schemas:
Many of these can be easily proved using the deduction theorem:
we need to show , which means we need to show . Since is , by modus ponens, .
since is , to show , we need to show , but this is obvious.
we need to show . Since is a deduction of from , and the result follows.
this is because , so .
this is the result of the first two theorem schemas above.
For the next four schemas, we need the the following meta-theorems (see here (http://planetmath.org/SomeMetatheoremsOfPropositionalLogic) for proofs):
If , then by M1, so by M2. Similarly, .
comes from 7, and since implies by M1, by M2. Therefore, by M1.
If , then and by M1, so by M1 again, and therefore by M2. Similarly, . Combining the two and apply M1, we have the result.
If , then and , so , , and by M1. By M1 again, we have and , and another application of M1, . Therefore, by M2, , Similarly, . Combining the two and applying M1, we have the result.
by modus ponens 3 times.
is a deduction of from and .
is a deduction of from , and .
is just an axiom, while comes from two applications of the deduction theorem to , which is the result of the deduction of from and .
|Title||some theorem schemas of propositional logic|
|Date of creation||2013-03-22 19:33:04|
|Last modified on||2013-03-22 19:33:04|
|Last modified by||CWoo (3771)|
|Defines||law of double negation|
|Defines||law of the excluded middle|
|Defines||ex falso quodlibet|