### Or… if $$p$$ and $$\neg p$$, then anything

A rather counterintuitive observation is that many inconsistent systems are, in fact, complete! More precisely, if a formal system that includes propositional logic can derive a contradiction, then it can derive anything, and is therefore complete.

Why? Because it turns out that the following formula is a theorem of propositional logic:

$p \supset (\sim p \supset q)$

Exercise for the reader: derive the formula. [My almost solution]

In words, ‘if p, then if not p, then q’. In other words, if you can derive both $$p$$ and $$\lnot p$$, then (via the rule of detachment twice) you can derive $$q$$. And remember, by the rule of substitution, any formula can be substituted for a sentential variable to derive another formula. So, if we can derive $$p$$ and $$\lnot p$$, and we can substitute anything we want for $$q$$, then we can derive anything! To put it shortly, from a contradiction, anything can be derived.

This fact has an interesting consequence. It’s actually quite cute. We just showed that if a system (that includes propositional logic) can derive a contradiction, then it can derive any formula. So, if any formula cannot be derived, then it must not be able to derive a contraction! In other words, proving that a single formula is not derivable within a system is equivalent to proving that the system is consistent.

How might we prove that a formula cannot be derived? By employing some meta-mathematical reasoning about the system as a whole. Note, we are going to prove something about the system, which is very different from deriving something within the system. Here’s one general strategy:

1. Find a property which is true of all the axioms.
2. Demonstrate that the property is preserved via all the transformation rules. In other words, demonstrate that all formulas derived from the axioms, i.e. theorems, will also have this property.
3. Find a formula which does not have this property. This formula must not be a theorem.

As a toy example, imagine all the axioms were made up of 25 or more symbols. And imagine every transformation rule only increases the number of symbols in the derived formula. If you can construct a formula with fewer than 25 symbols, then you know it’s not a theorem.