Proof that propositional logic remains consistent after the addition of a single axiom

logicpropositional-calculus

I was wondering if someone might be able to supply a hint for the following exercise:

Let $\mathcal{P}'$ be the system obtained from $\mathcal{P}$ by adding the single wff $[p \to q]$ to the axioms of $\mathcal{P}$. Show that $\mathcal{P}'$ is consistent.

The axiom schemes of $\mathcal{P}$ are

$[[A \lor A] \to A]$

$[A \to [B \lor A]]$

$[[A \to B] \to [[C \lor A] \to [B \lor C]]]$

Modus Ponens is the only primitive rule of inference.

I have been unsuccessfully trying to prove that a contradiction can not be a theorem of $\mathcal{P}'$.

Best Answer

Ref to : Peter Andrews, An Introduction to Mathematical Logic and Type Theory, page 35.

Assueme that $\mathcal P' = \mathcal P \cup \{ p \to q \}$ is inconsistent.

By definition, this means that $\mathcal P'$ proves every formula.

Thus, also : $\mathcal P' \vdash \lnot (p \to q)$ and, by Deduction Theorem [see 1116, page 30] :

$\mathcal P \vdash (p \to q) \to \lnot (p \to q)$.

But we have that $(p \to q) \to \lnot (p \to q)$ is not a tautology [check with the truth assignment $\varphi : \text {Var} \to \{ \text T, \text F \}$ such that : $\varphi(p)= \text F$ and $\varphi(q)= \text T$].

Thus, we have a contradiction with the Soundness Theorem for $\mathcal P$ [see 1200]: Every theorem of $\mathcal P$ is a tautology.

Related Question