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] :
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.