In X1212, we add a new axiom to \mathcal{P} and discuss the consistency of the new system. One way to see is to view the new axiom as a hypothesis. Generally, one can decide efficiently the consistency of \mathcal{P} after adding finitely many new axioms. Really, one just need to check whether the conjunction of those axioms is a contradiction or not. However, if we are allowed to add infinite many formule as axioms, such as the axiom scheme in X1213, one probably (not necessarily) will end up with an inconsistent logistic system.
Common Mistakes:
- Some students mentioned in their proof of X1212 that if we have the theorem schema A\supset .\sim A\supset B and Modus Ponens as a primitive or derived rule of inference in our system, then absolutely consistency is equivalent to consistency with respect to negation. This is true. But actually, by definition, absolutely consistency follows immediately if one get the consistency with respect to negation.
- Notice that inconsistency with respect to negation doesn’t imply absolutely inconsistency. In X1213, some students prove that the new system is not consistent with respect to negation, but they forgot to say the sufficient condition for the equivalence of two kinds of inconsistency. However, there is a quite direct way to prove that every wff is a theorem.