properties of consistency
Fix a (classical) propositional logic . Recall that a set of wff’s is said to be -consistent, or consistent for short, if . In other words, can not be derived from axioms of and elements of via finite applications of modus ponens. There are other equivalent formulations of consistency:
-
1.
is consistent
-
2.
Ded is not the set of all wff’s
-
3.
there is a formula such that .
-
4.
there are no formulas such that and .
Proof.
We shall prove
-
.
Since .
-
.
Any formula not in will do.
-
.
If and , then is a deduction of from and , but this means that for any wff .
-
.
Since , as a result.
∎
Below are some properties of consistency:
-
1.
is consistent iff .
-
2.
is not consistent iff .
-
3.
Any subset of a consistent set is consistent.
-
4.
If is consistent, so is Ded.
-
5.
If is consistent, then at least one of or is consistent for any wff .
-
6.
If there is a truth-valuation such that for all , then is consistent.
-
7.
If , and contains the schema based on , then is not consistent.
Remark. The converse of 6 is also true; it is essentially the compactness theorem for propositional logic (see here (http://planetmath.org/CompactnessTheoremForClassicalPropositionalLogic)).
Proof.
The first two are contrapositive of one another via the theorem , so we will just prove one of them.
-
2.
iff by the deduction theorem iff by the substitution theorem.
-
3.
If is not consistent, . If , then as well, so is not consistent.
-
4.
Since is consistent, Ded. Now, if Ded, but by the remark below, , a contradiction.
-
5.
Suppose is consistent and any wff. If neither and are consistent, then and , or and , or and by the substitution theorem on , but this means is not consistent, a contradiction.
-
6.
If for all , for all such that . Since , is consistent.
-
7.
Suppose for some valuation . Let be the propositional variables in such that and be the variables in such that . Let be the instance of the schema where each is replaced by and each replaced by (which is ). Then . Furthermore, . Now, for any valuation , since and , we get . In other words, for all valuations , so is valid, and hence a theorem of by the completeness theorem. But this means that , which implies that .
∎
Remark. The set Ded is called the deductive closure of . It is so called because it is deductively closed: iff Ded.
Proof.
If , then , so certainly Ded, as Ded is a superset of .
Before proving the converse, note first that if and , by modus ponens. This implies that Ded is closed under modus ponens: if and are both in Ded, so is .
Now, suppose Ded. We induct on the length of the deduction sequence of . If , then and we are done. Now, suppose the length of is . If is either a theorem or in Ded, we are done. Now, suppose is the result of applying modus ponens to two earlier members, say and . Since is a deduction of from Ded, and it has length , by the induction step, . Similarly, . But this means that by the last paragraph. ∎
Title | properties of consistency |
---|---|
Canonical name | PropertiesOfConsistency |
Date of creation | 2013-03-22 19:35:07 |
Last modified on | 2013-03-22 19:35:07 |
Owner | CWoo (3771) |
Last modified by | CWoo (3771) |
Numerical id | 18 |
Author | CWoo (3771) |
Entry type | Feature |
Classification | msc 03B45 |
Classification | msc 03B10 |
Classification | msc 03B05 |
Classification | msc 03B99 |
Related topic | FirstOrderTheories |
Defines | deductive closure |
\@unrecurse |