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

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}'$.

• This makes no sense at all. The definition of consistent says: "A set H of wffs is consistent iff there is wff A such that not H $\vdash$ A." In other words, a set of wffs H is consistent if there exists some wff A, such that H cannot suffice to derive A. If [p→q]. then by substitution [[p→q]→r] is a theorem. So, by detachment, 'r' is a theorem; an entirely arbitrary variable. Thus, every wff is a theorem and there is no wff A such that not H $\vdash$ A. For any wff A, H $\vdash$ A, where H is the new axiom set. Commented Jul 13, 2018 at 15:44
• Does it matter that $[p \to q]$ is an axiom, not an axiom scheme? Therefore I believe that you can't substitute into it to get $[[p \to q] \to r]$? Commented Jul 14, 2018 at 17:29
• That's an interesting question. First off, if [p$\rightarrow$q] is an axiom, but not an axiom schema, then P has no axioms, it only has axiom schema. So, the problem would propose adding that axiom to the existing axiom schema. Second, it looks like evaluating [p→q] as a tautology or not still works the same way according to Mauro's reference. But, it's not a tautology. Commented Jul 14, 2018 at 19:57
• Thinking more on it, the rule of substitution is valid for both axioms and axiom schema. So, if the rule of substitution would have to get explicitly disallowed for a particular axiom such as [p→q], but still come as valid for an axiom like [[[p∨p]→p]→[q→[[p∨p]→p]]] . That wouldn't just alter the axioms/axiom schema, but it would also alter the (derivable) rules of inference. Commented Jul 14, 2018 at 20:10
• @DougSpoonwood I think the idea is that $\mathcal{P}$ has all the axioms generated by the axiom schemes listed in the question. $\mathcal{P}'$ has all those axioms, plus one more; the single wff $[p \to q]$. Commented Jul 14, 2018 at 20:16

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.

• This doesn't work. As soon as you add [p→q], the Soundness Theorem fails. Thus, there is no contradiction of the Soundness Theorem, because, again, it's not a theorem. Commented Jul 13, 2018 at 15:35
• @DougSpoonwood His proof says that it is a contradiction with the Soundness Theorem for $\mathcal{P}$, not $\mathcal{P'}$. The Soundness Theorem for $\mathcal{P}$ still holds right? Commented Jul 14, 2018 at 17:33
• @user695931 Each axiom in P is a tautology, and the rules of inference are valid, so yes, the Soundness Theorem for P still holds. Commented Jul 14, 2018 at 19:44
• @DougSpoonwood So I believe your first comment does not hold? Commented Jul 14, 2018 at 20:47
• @user695931 My first comment says that when you add [p→q] to the system, the Soundness Theorem fails. So, my first comment works. Commented Jul 14, 2018 at 23:47

It suffices to show that there is a model of $\mathcal P$ where $p\to q$ is true.

As $\mathcal P$ is consistent, let $M$ be a model of $\mathcal P$. If $M$ says that $q$ is true or that $p$ is false, we are done. Otherwise (i.e., if it says $q$ is false and $p$ is true), swap $p$ and $q$, i.e., let $M'$ be such that it's truth value for a wff is the truth value $M$ assigns to the same wff wit $p,q$ exchanged. Then $M'$ is still a model of $\mathcal P$, and here $p\to q$ is true.

• Thank you for your answer. The text that this is from has not introduced models yet. Is there another approach? Commented Jul 12, 2018 at 3:46
• This doesn't work either. Every single wff is provable if [p→q] is an axiom. Commented Jul 13, 2018 at 15:46
• @DougSpoonwood Please check my comment under the question. Commented Jul 14, 2018 at 17:38