Proof axiomatically:

$\vdash \forall x (\neg (Ax \rightarrow Bx) \rightarrow (\neg Ax \rightarrow \neg Bx))$

You can use in your deduction as step the equivalence of $\varphi$ with $\neg\neg\varphi$:

$\varphi\vdash\neg\neg\varphi$ and $\neg\neg \varphi \vdash \varphi$

Also used are the following axioms:

1 $(∀x(φ→ψ)) \rightarrow (\forall x \varphi \rightarrow \forall x \psi)$
2 $\varphi \rightarrow \forall x \varphi$ ($x$ not free in $\varphi$)
3 $\forall x \varphi \rightarrow [t/x]\varphi$
a $\varphi \rightarrow (\psi \rightarrow \varphi)$
b $\varphi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi)\rightarrow(\varphi \rightarrow \chi))$
c $(\neg \varphi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \varphi)$

So starting out on this question, I had hopes of delivering an answer. But alas, my plans were foiled, I could not get a deduction. So, I decided to have a peek at the answer, and it baffled me completely:

  1. $\vdash Bx \rightarrow (Ax \rightarrow Bx)$ (a)
  2. $\neg\neg Bx\vdash Bx$ ($\neg\neg\varphi\vdash\varphi$)
  3. $\neg\neg Bx \vdash Ax \rightarrow Bx$ (MP, 1, 2)
  4. $Ax \rightarrow Bx \vdash \neg\neg(Ax \rightarrow Bx)$ ($\varphi\vdash\neg\neg\varphi$)
  5. $\vdash (Ax \rightarrow Bx) \rightarrow \neg\neg(Ax \rightarrow Bx)$ (deduction theorem on 4)
  6. $\neg\neg Bx \vdash \neg\neg(Ax \rightarrow Bx)$ (MP, 3, 5)
  7. $\vdash \neg\neg Bx \rightarrow \neg\neg(Ax \rightarrow Bx)$ (deduction theorem on 6)
  8. $\vdash (\neg\neg Bx \rightarrow \neg\neg(Ax \rightarrow Bx)) \rightarrow (\neg(Ax \rightarrow Bx) \rightarrow \neg Bx)$ (c)
  9. $\vdash \neg(Ax \rightarrow Bx) \rightarrow \neg Bx$ (MP, 7, 8)
  10. $\neg(Ax \rightarrow Bx) \vdash \neg(Ax \rightarrow Bx)$ (assumption)
  11. $\neg(Ax \rightarrow Bx) \vdash \neg Bx$ (MP, 9, 10)
  12. $\vdash \neg Bx \rightarrow (\neg Ax \rightarrow \neg Bx)$ (a)
  13. $\neg(Ax \rightarrow Bx) \vdash (\neg Ax \rightarrow \neg Bx)$ (MP, 11, 12)
  14. $\vdash \neg(Ax \rightarrow Bx) \rightarrow (\neg Ax \rightarrow \neg Bx)$ (deduction theorem on 13)
  15. $\vdash \forall x (\neg(Ax \rightarrow Bx) \rightarrow (\neg Ax \rightarrow \neg Bx))$ (universal generalization on 14)

Starting from 1, I immediately run into a wall. I have absolutely no idea how it got here. Where does $Bx$ come from? So, I start from the bottom. This goes a bit easier, but backtracking it is still not easy. This goes well up until 10/9-ish, again, I run into a wall. No ideas on how to get to the following statement, let alone to 1.

My question is this: can someone guide me through this deduction, with the simplest of explanation?

  • $\begingroup$ Are you sure about the correct "trnscription" of your axiom system ? Are they from some textbook ? The formula $A \rightarrow (B \rightarrow A)$ is a tautology; thus must be provable in every complete proof system (in Mendelson's is an axiom of propositional logic). I think that your axiom a) is "the wrong one"; it must be $\varphi \rightarrow (\psi \rightarrow \varphi)$; in this acse step 1) is just an instance of it. Your a) cannot be, because is not a tautology ... $\endgroup$ – Mauro ALLEGRANZA May 21 '14 at 16:44
  • $\begingroup$ You're absolutely correct, I edited my post. $\endgroup$ – Garth Marenghi May 21 '14 at 17:28

This is a long comment ...

The above proof is "complicated" and difficult to grasp because the axiomatic (or Hilbert-style) proof-system is very "opaque", in terms of euristic (finding how to build up the required proof).

Natural deduction is far better for this.

A possible way to "simplify" the search of a proof in a case like that above, which is basically a "propositional" proof (the only "quantifier" rule is invoked in the last step), is to "enlarge" the set of rules available.

How ? Starting from the propositional axioms a)-c) and proving their completeness for the tautologies, i.e.proving the meta-theorem which states that all tautologies are provable from the above axioms with modus ponens.

In this way, we may use in our proofs every instance of a tautology.

Assuming having done this, we may build another proof of the theorem using the following tautologies :

$\vDash_{TAUT} (\varphi \rightarrow \psi) \lor (\psi \rightarrow \varphi)$ --- $(TAUT_1)$

and :

$\vDash_{TAUT} \lnot \sigma \rightarrow [ (\sigma \lor \tau) \rightarrow \tau) ]$ --- $(TAUT_2)$

and :

$\vDash_{TAUT} (\varphi \rightarrow \psi) \rightarrow (\lnot \psi \rightarrow \lnot \varphi)$ --- $(TAUT_3)$.

Now for the proof.

(1) Instantiate $TAUT_1$ with $Ax$ in place of $\varphi$ and $Bx$ in place of $\psi$ :

$\vdash (Ax \rightarrow Bx) \lor (Bx \rightarrow Ax)$

(2) Instantiate $TAUT_2$ with $(Ax \rightarrow Bx)$ in place of $\sigma$ and $(Bx \rightarrow Ax)$ in place of $\tau$ :

$\vdash \lnot (Ax \rightarrow Bx) \rightarrow ( [ (Ax \rightarrow Bx)\lor (Bx \rightarrow Ax) ] \rightarrow (Bx \rightarrow Ax) )$

(3) Assume :

$ \lnot (Ax \rightarrow Bx)$

(4) $\lnot (Ax \rightarrow Bx) \vdash [ (Ax \rightarrow Bx)\lor (Bx \rightarrow Ax) ] \rightarrow (Bx \rightarrow Ax)$ --- from 2) and 3) by modus ponens

(5) $\lnot (Ax \rightarrow Bx) \vdash (Bx \rightarrow Ax)$ --- from 1) and 4) by modus ponens

(6) Instantiate $TAUT_3$ with $Bx$ in place of $\varphi$ and $Ax$ in place of $\psi$ :

$ \vdash (Bx \rightarrow Ax) \rightarrow (\lnot Ax \rightarrow \lnot Bx)$

(7) $\lnot (Ax \rightarrow Bx) \vdash (\lnot Ax \rightarrow \lnot Bx)$ --- from 5) and 6) by modus ponens

(8) $\vdash \lnot (Ax \rightarrow Bx) \rightarrow (\lnot Ax \rightarrow \lnot Bx)$ --- from 7) by Deduction Theorem.

Now the "hard" work is done.

We have only to apply the Generalization Theorem :

if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$,

with $\Gamma = \emptyset$, to conclude from 8) :

$\vdash \forall x [\lnot (Ax \rightarrow Bx) \rightarrow (\lnot Ax \rightarrow \lnot Bx) ]$.

  • $\begingroup$ That is a long comment, thanks for the effort. I can't believe how difficult it is to be able to come up with a proof for this question, and that they've asked this question. It really undermines my "Yeah I'm going to be good at this" feeling. Anyways, you at least cleared up some of the questions I had, and I want to thank you for your time and effort, it is much appreciated! $\endgroup$ – Garth Marenghi May 23 '14 at 18:35
  • $\begingroup$ @GarthMarenghi - going on with your study of math log, you will find proof system like natural deduction and sequent calculus, which are much more easy and "user-friendly". The sequent calculus proof of the above theorem is "quite trivial"- $\endgroup$ – Mauro ALLEGRANZA May 23 '14 at 18:40

Axioms a)-c) are a complete set of axioms for propositional logic and thus we are allowed to use in your proofs every instance of tautologies (like $\varphi \leftrightarrow \lnot \lnot \varphi$).

In addition, axioms a)-b) are enough to prove the Deduction Theorem.

Please, note that axiom 1) is wrongly stated. It must be (see your previous post ) :

$\forall x(\varphi \rightarrow \psi) \rightarrow (\forall x \varphi \rightarrow \forall x \psi)$.

In axiom 2), we have to add the proviso that $x$ is not free in $\varphi$, otherwise the formula $φ→∀xφ$ is not valid: thus, it cannot be an axiom.

Whit these corrections, axioms a)-c) plus 1)-3) form a complete set of axioms for first-order logic.

I assume that the only inference rule is modus ponens.

Having said that, the proof looks fine to me, except for the last step : what is the invoked "universal generalization" ?

Do you have also the inference rule :

$${\varphi \over \forall x \varphi}$$

If so, there are some "interference" with the deduction theorem to be checked.

Otherwise, with only modus ponens as rule, we must use the Generalization Theorem :

if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.


Now the proof. We start using an instance of axiom a); the axiom is a schema. i.e. we may assert every instance of it, that is every formula obtained from the schema putting formulas whatever in place of $\varphi$ and $\psi$, provided that we substitute all occurrence of $\varphi$ (and $\psi$, and so on) with the same formula.

Thus, from :

$\vdash φ→(ψ→φ)$

putting $Bx$ in place of $\varphi$ and $Ax$ in place of $\psi$, we get 1) :

$\vdash Bx→(Ax→Bx)$.

Until 9) there are some easy steps. Then 10) is a new assumption; the "rule" is :

$\Gamma \vdash \varphi$, when $\varphi \in \Gamma$;

in our case : $\Gamma = \{ ¬(Ax→Bx) \}$.

Thus we state the temporary assumption : $\lnot (Ax \rightarrow Bx)$. We will "discharge" it in step 14) using the DT, in the same way as in step 7) we have "discharged" the temporary assumption $¬¬Bx$ introduced in step 2).

Having derived 9) :


with 10) we use modus ponens to derive : $\lnot Bx$, under the above temporary assumption 10); that is 11) :

$\lnot (Ax \rightarrow Bx) \vdash \lnot Bx$.

Now we use a new instance of axiom a) : $\vdash φ→(ψ→φ)$, putting $\lnot Bx$ in place of $\varphi$ and $\lnot Ax$ in place of $\psi$. Thus, we get 12) :


Finally, we use modus ponens with 11) and 12) to "detach" : $(¬Ax→¬Bx)$.

But $\lnot Bx$ (we have used it in the last application of mp) "depends on" the temporary assumption 10); thus also the conclusion of mp depends on it, and we have 13) :

$¬(Ax→Bx) \vdash (¬Ax→¬Bx)$.

The last steps are easy.

Note about axiom schemata [from : Peter Smith, Types of Proof System (2010)].

Let's have an example of an axiomatic system to be going on with. In this system $\mathsf M$, to be found e.g. in Mendelson's classic Introduction to Mathematical Logic, the only propositional connectives built into the basic language of the theory are '$\rightarrow$' and '$\lnot$' ('if ... then ...' and 'not', the same choice of basic connectives as in Frege's Begrisschrift).

The axioms are then all wffs [wee-formed formulas] which are instances of the schemata [see footnote] :

Ax1. $(A \rightarrow (B \rightarrow A))$

Ax2. $((A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow)))$

Ax3. $((\lnot B \rightarrow \lnot A) \rightarrow ((\lnot B \rightarrow A) \rightarrow B))$.

$\mathsf M$'s one and only rule of inference is modus ponens, the rule from $A$ and $(A \rightarrow C)$ infer $C$.

In this axiomatic system, a proof from the given premisses $A_1, A_2, ...A_n$ to conclusion $C$ is a linear sequence of wffs such that each wff is either :

(i) a premiss $A_i$,

(ii) a logical axiom, i.e. an instance of Ax1, Ax2 or Ax3, or

(iii) follows from two previous wffs in the sequence by modus ponens, and

(iv) the final wff in the sequence is $C$.

When there is such a proof we will write :

$A_1, A_2, ... A_n \vdash_{\mathsf M} C$.

If we can prove $C$ from the axioms alone without additional premisses, we'll say that $C$ is a theorem, and write simply $\vdash_{\mathsf M} C$.

Footnote. 3`Instances of the schemata'? An wff is an instance of a schema (plural: schemata) if it results for systematically replacing schematic letters $A, B, C$ etc. in the schema by particular wffs - with, in a given case, the same schematic letter always being substituted by the same wff.

Going back to our example (see : step 1), from the schemata a) :


[which is the same as Ax1 of Peter Smith's paper] we may "generate" as many instances as we want. To do this, we need two formulas whatever to be substituded in place of shematic letters $\varphi$ and $\psi$.

Example 1) : $p$ in place of $\varphi$ and $q$ in place of $\psi$ :


Example 2) : $0 = 0$ in place $\varphi$ and $1 = 0$ in place of $\psi$ :


Example 3) : $Bx$ in place $\varphi$ and $Ax$ in place of $\psi$ :


We have not "derived" $Bx$; we are using "instruction" n° (ii) of the above definition of proof :

a linear sequence of wffs such that each wff is [...] a logical axiom, i.e. an instance of Ax1, Ax2 or Ax3.

  • $\begingroup$ You're absolutely right about the errors. And yes, Modus Ponens is used as an inference rule. I know the proof must be right; I got it from the answers in the textbook. The problem I have with this, is that I cannot reproduce it. I don't understand how 1. is derived, and if I start from the bottom (number 15), then I also hit a wall around number 10/11. My question was if someone would be so kind as to explain how the derivation is derived. $\endgroup$ – Garth Marenghi May 21 '14 at 17:34
  • $\begingroup$ I understand your update; my problem here would be that in order to instantiate axiom a, you need $Bx$. $\endgroup$ – Garth Marenghi May 21 '14 at 19:14
  • $\begingroup$ @GarthMarenghi - NO From $\vdash φ→(ψ→φ)$ you have to put $Bx$ in place of $\varphi$ and $Ax$ in place of $\psi$ and you will get : $\vdash Bx→(Ax→Bx)$ $\endgroup$ – Mauro ALLEGRANZA May 21 '14 at 19:18
  • $\begingroup$ I understand. In order to use axiom a, we put in $Bx$ for $\varphi$. $\psi$ could be anything, it doesn't matter. But as far as my understanding goes, you must first derive $Bx$; only then can you use it in axiom a. Also, there's no indication whatsoever that makes me want to use axiom a here. $\endgroup$ – Garth Marenghi May 21 '14 at 19:38
  • $\begingroup$ @GarthMarenghi - some final additions; you have to review the use of axiom-schema in derivations. Can you tell us what is your textbook ? I can check the relevant pages and we can discuss it tomorrow. $\endgroup$ – Mauro ALLEGRANZA May 21 '14 at 20:35

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.