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

  • 1
    $\begingroup$ 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. $\endgroup$ Commented Jul 13, 2018 at 15:44
  • 1
    $\begingroup$ 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]$? $\endgroup$
    – user695931
    Commented Jul 14, 2018 at 17:29
  • $\begingroup$ 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. $\endgroup$ Commented Jul 14, 2018 at 19:57
  • $\begingroup$ 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. $\endgroup$ Commented Jul 14, 2018 at 20:10
  • $\begingroup$ @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]$. $\endgroup$
    – user695931
    Commented Jul 14, 2018 at 20:16

2 Answers 2


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.

  • 1
    $\begingroup$ 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. $\endgroup$ Commented Jul 13, 2018 at 15:35
  • $\begingroup$ @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? $\endgroup$
    – user695931
    Commented Jul 14, 2018 at 17:33
  • $\begingroup$ @user695931 Each axiom in P is a tautology, and the rules of inference are valid, so yes, the Soundness Theorem for P still holds. $\endgroup$ Commented Jul 14, 2018 at 19:44
  • $\begingroup$ @DougSpoonwood So I believe your first comment does not hold? $\endgroup$
    – user695931
    Commented Jul 14, 2018 at 20:47
  • $\begingroup$ @user695931 My first comment says that when you add [p→q] to the system, the Soundness Theorem fails. So, my first comment works. $\endgroup$ 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.

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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .