I've made it to section 12 in Kleene's Mathematical Logic, which is about completeness. Surprisingly, I was able to understand how every valid formula is provable. However, one of the exercises he gives (12.4) is to show that every formula is provable after adding $A \supset B$ to the axioms of the propositional calculus. I understand that adding this axiom kind of breaks everything down, because it makes the deduction theorem a moot point. I've had a bit of trouble formalizing my thoughts though.

One of the theorems (theorem 10) says that if $\vdash A\supset B$, then $A \vdash B$. However, if $A \supset B$ is an axiom, then the hypothesis is always true and B is always provable. Is this all that's required to show that introducing implication as an axiom makes every formula provable? It seems right in my mind, but also "too easy," so I just wanted to get some verification.



That's basically it. To show that $B$ is provable, take for $A$ some true statement $\top$. Then $\top\vdash B$, so $\vdash B$.

  • $\begingroup$ What you've said is correct, but I don't think that's what he/she said in the original question. $\endgroup$ – Doug Spoonwood Sep 18 '14 at 19:37

" However, if A⊃B is an axiom, then the hypothesis is always true and B is always provable."

That doesn't hold. (A⊃B) can be an axiom, but the hypothesis "A" is not always true. So that won't work.

But, let's say that (A⊃B) is our only axiom, and we have the rule of substitution. What can you do then?

Let x/y indicate that formula "x" gets substituted with formula "y". Then, we could write a proof like this:

axiom              1 (A⊃B)
1 A/(A⊃B)          2 ((A⊃B)⊃B)
2, 1 modus ponens  3 B

Notice that deriving B here is not affected by the substitution made in the axiom. We could write another proof like this:

axiom             1 (A⊃B)
1 B/C             2 (A⊃C)
2 A/(A⊃B)         3 ((A⊃B)⊃C)
3, 1 modus ponens 4 C

Since C is arbitrary, it follows that we could get any formula given (A⊃B) as an axiom.

This shows that modus ponens would break down if (A⊃B) were an axiom.


I'll suggest the following approach, recalling that the new axiom :

$\vdash A \rightarrow B$

is an axiom schema.

If we add it , we can use in derivations every instance of it.

Thus, we can have :

$\vdash \lnot P \rightarrow Q$

and also :

$\vdash \lnot P \rightarrow \lnot Q$.

Now we can use them with axiom n°7, page 16 :

$\vdash (A \rightarrow B) \rightarrow ((A \rightarrow \lnot B) \rightarrow \lnot A)$

to derive, by modus ponens twice :

$\vdash \lnot \lnot P$.

Then apply axiom n°8, page 16 :

$\vdash \lnot \lnot A \rightarrow A$

to conclude with :

$\vdash P$.

But $P$ is a formula whatever; thus, the addition of the new axiom licenses us to prove every formula, and the system is now inconsistent.

The issue does not involve specifically the Deduction Theorem.

We can destroy consistency of propositional calculus adding as axiom a formula $A$ whatever which is not a tautology (and thus : $\nvdash A$).

If we consider, instead of $A \rightarrow B$, a new formula : $A \lor B$, adding it as a new axiom produces the same result.

Substitute $P$ for both $A$ and $B$ and we have : $\vdash P \lor P$, which implies $\vdash P$.

Then we do the same with $\lnot P$ and we have : $\vdash \lnot P$.

Conclusion : propositional calculus plus the axiom $\vdash A \lor B$ is inconsistent.

  • 1
    $\begingroup$ "Substitute ¬P for both A and B and we have : ⊢P∨P, which implies ⊢P." I think there's a typo there. $\endgroup$ – Doug Spoonwood Sep 20 '14 at 21:14

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.