My teacher has assigned us this exercise as part of our homework:

Give a natural deduction proof of $(\alpha\to\beta)\to(\beta\to\gamma)\to(\alpha\to\gamma)$

Here is an example of natural deduction that he gave us:

$\vdash \alpha\to\beta\to\alpha$.

This is a tautology, but it's easier to prove than to verify:
$\alpha,\beta\vdash\alpha$, hypothesis
$\alpha\vdash\beta\to\alpha$, deduction theorem
$\vdash\alpha\to\beta\to\alpha$, deduction theorem

Here is my attempt:

Hypothesis: $(\alpha\to\beta),(\beta\to\gamma) \vdash (\alpha\to\gamma)$
Deduction thm: $(\alpha\to\beta) \vdash(\beta\to\gamma)\to(\alpha\to\gamma)$
Deduction thm: $\vdash(\alpha\to\beta)\to(\beta\to\gamma)\to(\alpha\to\gamma)$

Is this enough? I feel like I need to take apart the functions inside the parentheses and check those as well, but I don't know how.

  • $\begingroup$ Is your "hypothesis" an axiom of your natural deduction system? If so, your proof is fine. If not, you need to derive it from whatever your axioms are. $\endgroup$ – Lord_Farin Nov 19 '13 at 17:46

Unless you already have that hypothesis, you need to get to that hypothesis first.

Also, (α→β)→(β→γ)→(α→γ) is ambiguous. You almost surely want to prove ((α→β)→((β→γ)→(α→γ))). Additionally, you don't actually use the deduction (meta) theorem, you use the rule of inference that it implies as valid. I'll call this rule "conditional introduction".

I don't know your format exactly or what you have exactly, but a proof might go something like this:

Hypothesis (rule of modus ponens/detachment): (α→β), α $\vdash$ β

Weakening: (α→β), α, (β→γ) $\vdash$ β

Commutation on the left side: (α→β), (β→γ), α $\vdash$ β

Identity: (α→β), (β→γ), α $\vdash$ β, (β→γ)

Detachment: (α→β), (β→γ), α $\vdash$ γ

Conditional introduction: (α→β), (β→γ) $\vdash$ (α→γ)

  • $\begingroup$ Thank you! Everything makes sense to me in this proof, although I have one question. Is "Weakening" a deductive step in the proof, or just a necessary assumption in order to complete the proof? $\endgroup$ – Jeff Nov 20 '13 at 1:00
  • $\begingroup$ @Jeff I'm not sure. We'd need to know the specifics of your formal system. With a formal system we need to know that every step of a given proof satisfies the definition of a proof. This can mean that every step is either an assumption or hypothesis, an axiom, or follows from previous steps in the proof solely by the rules of inference permitted. $\endgroup$ – Doug Spoonwood Nov 20 '13 at 4:14

$$\begin{align} (1) & \alpha \rightarrow \beta && [\text{HYP}] \\ (2) & \beta \rightarrow \gamma && [\text{HYP}] \\ (3) & \alpha && [\text{HYP}] \\ (4) & \beta && [\text{MP}(1,3)] \\ (5) & \gamma && [\text{MP}(2,4)] \\ (6) & \alpha \rightarrow \gamma && [\rightarrow\text{-intro}(3,5)] \\ (7) & (\beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow \gamma) && [\rightarrow\text{-intro}(2,6)] \\ (8) & (\alpha \rightarrow \beta) \rightarrow ((\beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow \gamma)) && [\rightarrow\text{-intro}(1,7)] \\ \end{align}$$

  • $\begingroup$ Not much left to do here. $\endgroup$ – Dan Christensen Nov 20 '13 at 0:35

If, as Doug suggested, you are really required to prove

$A\implies B \implies (B\implies C \implies (A\implies C))$,

you could start with 3 successive premises, the first two being:

  1. Suppose $A\implies B$

  2. Suppose $B\implies C$

  3. Suppose ???

(I don't like Greek letters!)


I will replace $\alpha$ with $A$, $\beta$ with $B$, and $\gamma$ with $C$ to use the truth table generator and Fitch-style natural deduction proof checker.

To resolve the question of ambiguity, the following truth table shows that one cannot prove $((A\to B)\to(B\to C))\to(A\to C)$:

enter image description here

The counterexample is in the fourth line of the table where $A=T$, $B=F$, and $C=F$.

With the ambiguity resolved, here is a natural deduction proof:

enter image description here

Michael Rieppel. Truth Table Generator. https://mrieppel.net/prog/truthtable.html

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/


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.