Deriving $A \rightarrow ( B \rightarrow C ) \rightarrow ( ( A \rightarrow B ) \rightarrow ( A \rightarrow C ) )$ in the sequent calculus

Question

I need to prove the following theorem: $A\to (B\to C) \to ((A\to B) \to (A\to C))$

using the sequent calculus method.

Using the rules:

$$ G, A \Rightarrow B,D \over G \Rightarrow A \to B , D $$

and

$$ G \Rightarrow A,D \ \ \ \ G,B \Rightarrow D \over A\to B \Rightarrow D $$

and the Identity Axiom :
$$ \over G,A \Rightarrow A,D $$

• $\to$ is an ordinary implication sign,
• $\Rightarrow$ is the sequential implication sign,
• $G,D$ are finite (and possibly empty) sets of propositions, and
• $G\Rightarrow D$ is to mean, that the conjuction of the propositions in $G$, implies the disjunction of those in $D$.

I really can't go anywhere so far, thanks for your help in advance.

Answer 1

What you've called "rule" is usually called "axiom" or "axiom scheme" and "identities" are usually called "rules".

1. $A \Rightarrow A, B, C$ (axiom) and $A, B \Rightarrow B, C$ (axiom) implies $A, A\rightarrow B \Rightarrow B, C$ by the second rule.

2. 1 and $A, A\rightarrow B, C \Rightarrow C$ (axiom) implies $A, A\rightarrow B, B\rightarrow C \Rightarrow C$ by the second rule.

3. $A \rightarrow B,A \Rightarrow A, C$ (axiom) and 2 implies $A, A\rightarrow B, A\rightarrow(B\rightarrow C) \Rightarrow C$ by the second rule.

4. 3 implies $A\rightarrow B, A \rightarrow(B\rightarrow C) \Rightarrow A\rightarrow C$ by the first rule.

5. 4 implies $A \rightarrow(B\rightarrow C) \Rightarrow (A\rightarrow B )\rightarrow(A\rightarrow C)$ by the first rule.

6. 5 implies $\Rightarrow (A \rightarrow(B\rightarrow C)) \rightarrow ((A\rightarrow B )\rightarrow(A\rightarrow C))$ by the first rule.

Answer 2

A "long" comment.

You can use this example to "format" the sequent calculus axiom and rules :

$${ \quad \over \Gamma, A \implies A, \Delta } \, \text{(Axiom)}$$

$${ \Gamma \implies A \quad B \implies \Delta \over \Gamma \implies A \rightarrow B, \Delta } \, \text{(Rule)}$$

Answer 3

Sequent proofs should tend to write themselves without you having to think about them (which is the the point of using them!). The motto is: start from where you want to end up and work backwards (or rather upwards: in other words, write the sequent you want to prove at the bottom, and construct the tree from bottom to top ...).

You want to establish the sequent

$$\Rightarrow A\to (B\to C) \to ((A\to B) \to (A\to C))$$

Given your rules, that can only come from

$$A\to (B\to C) \Rightarrow (A\to B) \to (A\to C)$$

which in turn must surely come from

$$A\to (B\to C), (A\to B) \Rightarrow A\to C$$

which in turn must come from

$$A\to (B\to C), (A\to B), A \Rightarrow C$$

So how do we get that? We'll have to use your final rule. Deal with the most complex wff first, and that must come from

$$(B\to C), (A \to B), A \Rightarrow C\quad and\quad A\to B, A \Rightarrow A, C$$

You can see how to get the right-hand one of those (it's what you are calling an identity)! So what about the left sequent? That comes from e.g.

$$C, (A \to B), A \Rightarrow C \quad and\quad (A \to B), A \Rightarrow B, C$$

And you can immediately see how to get the left-hand one of those. And the right-hand sequent obviously comes from

$$B, A \Rightarrow B, C \quad and \quad A \Rightarrow A, B, C$$

Turn all that the other way up to get a top-to-bottom proof from "identities" (better "axioms") via the rules for moving $\to$ around.

The moral is you don't have to puzzle to construct this sort of proof. To repeat: just write your proof "from the bottom up" doing the obvious thing at every stage. That, as I said, is the delight of sequent proofs!