I'm using the book An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, and it does not have any solutions and barely any examples. I want to understand how to prove that all wff are theorems. Here is one exercise.

Let $\Lambda$ be a formulation of propositional calculus in which the sole connective are negation and disjunction, the sole rule of inference is Modes Ponens, and with the following axiom schema: $\sim[A\vee B]\vee[B\vee C] $. Prove that $\Lambda$ is absolutely inconsistent.

I know that I need to prove that every wffs is a theorem with only the rule "if $A$ and $\sim A \vee B$ are theorems, B is a theorem" and the above axiom.

Now, let $F$ be a wff, how do I prove it's a theorem, where do I even start?

  • 1
    $\begingroup$ You've mis-stated the modus ponens inference rule. IN Andrews's book it is "From $A$ and $\sim{A} \lor B$ to infer $B$" -- it is not about what is a wff!! $\endgroup$ Feb 2, 2013 at 8:45
  • $\begingroup$ @Peter Ok. I'll rectify that. Thanks $\endgroup$ Feb 2, 2013 at 8:46
  • $\begingroup$ No. It is not required that the premisses which are inputs to a modus ponens inference are already theorems (think about the import of the Deduction Theorem). $\endgroup$ Feb 2, 2013 at 9:05
  • $\begingroup$ But isn't that what I had earlier, if we have A and ∼A∨B as well formed formula I can deduct B. $\endgroup$ Feb 2, 2013 at 9:13
  • $\begingroup$ No. What you wrote before was about inferring from the assumptions that $A$ is a wff and $\sim{A} \lor B$ is a wff to the conclusion that $B$ is a wff. What you need is the rule as I gave it. [The assumption that 2 + 3 = 4, and the assumption that "2 + 3 = 4" is a wff are quite different, aren't they? One is false the other can be true.] $\endgroup$ Feb 2, 2013 at 9:18

1 Answer 1


First, let's find a proof of $X$ where $X$ is a propositional variable rather than an arbitrary formula. Afterwards, if want to prove an arbitrary wff $A$, we can take our proof of $X$ and replace every $X$ in that proof with $A$. This works because the system we're working with here has no axioms or inference rules that allow us to do something with a propositional variable that we can't also do with a more complex formula.

We can find a proof of $X$ from the conclusion up by a sort of semi-smart brute force search. Every premise we need must be concluded either by modus ponens or as an instance of the axiom scheme, so whenever we need does not have the right shape to be an instance of the axiom, it must be concluded by modus ponens.

This is, for example, the case for the final conclusion $X$, so the last step in the proof must be modus ponens. We then have to prove $$ {\sim} A \lor X \qquad\text{and}\qquad A $$ for some $A$ whose structure we're free to choose. The first of these cannot be an axiom no matter which $A$ we choose, so it itself must be concluded by modus ponens. So what we now need to prove is $$ {\sim}B \lor [{\sim}A\lor X] \qquad\qquad B \qquad\qquad A $$ The first one of these looks promising because it will be an instance of the axiom if only we decide that $B$ is going to be $C\lor{\sim}A$. That leaves us with the following to prove:

$$ C\lor{\sim}A \qquad\qquad A $$ The first of these again needs to be proved by modus ponens (the negation is in the wrong place and we don't have any rule saying that $\lor$ is commutative), so we need $$ {\sim}D \lor [C\lor {\sim}A] \qquad\qquad D \qquad\qquad A $$ and the first of these becomes an axiom if $D$ is $E\lor C$. That coverts our proof obligations to $$ E\lor C \qquad\qquad A $$ and these can both be axioms by choosing appopriate unfoldings for $E$, $C$, and $A$, namely

  • $A = {\sim}[X\lor X]\lor [X\lor X]$
  • $E = {\sim}[X\lor X]$
  • $C = X\lor X$

Putting everything together we can write down our proof in standard order:

  1. $~{\sim}[X\lor X]\lor [X\lor X] \qquad$ (axiom)
  2. $A \qquad$ (1, definition of $A$)
  3. $E\lor C \qquad$ (1, definition of $E$ and $C$)
  4. ${\sim}[E\lor C]\lor[C\lor {\sim}A] \qquad$ (axiom)
  5. $C \lor {\sim}A \qquad$ (3, 4, MP)
  6. ${\sim}[C\lor {\sim}A]\lor[{\sim}A\lor X] \qquad$(axiom)
  7. ${\sim}A\lor X \qquad$ (5, 6, MP)
  8. $X \qquad$ (2, 7, MP)
  • $\begingroup$ Very elegantly done! $\endgroup$ Feb 3, 2013 at 16:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.