# Define inl : $σ → σ ∨ τ$

I'm a bit stuck in Geuvers' "Introduction to Type Theory" (http://www.cs.ru.nl/~herman/onderwijs/provingwithCA/paper-lncs.pdf), p. 39:

Exercise 13. Prove the derivability of some of the other logical rules: 1. Define inl : $σ → σ ∨ τ$

where $σ∨τ := ∀α.(σ→α)→(τ →α)→α$. I suppose one could use Definition 32 (p. 38) to derive $∀α.σ$ from $σ$ but that's about it (Definition 30 might be useful, too). No solutions are available and I'm not sure how to derive $α$ from $σ$ (should I just assume it?) or $σ→α$ from $σ$ or $∀α.(σ→α)→(τ →α)→α$ from $(σ→α)→(τ→α)→α$ or whatever other option there might be. Any ideas? Hints?

It seems to me that the requested derivation is :

1) $\sigma$ --- assumed [1]

2) $\sigma \to \alpha$ --- assumed [2]

3) $\alpha$ --- from 1) and 2) by $\to$-E

4) $(\tau \to \alpha) \to \alpha$ --- from 3) by $\to$-I

5) $(\sigma \to \alpha) \to (\tau \to \alpha) \to \alpha$ --- from 2) and 4) by $\to$-I, discharging [2]

6) $\forall \alpha [(\sigma \to \alpha) \to (\tau \to \alpha) \to \alpha]$ --- from 5) by $\forall$-I : $\alpha \notin FV(\sigma)$

7) $\sigma \lor \tau$ --- definition of $\lor$

$\sigma \to \sigma \lor \tau$ --- from 1) and 7) by $\to$-I, discharging [1].

• Thanks, this gave me some ideas, but 6) seems to be wrong -- $α$ is not supposed to be among free variables in the preceding lines (check $∀$-I in Definition 32) – jaam Jun 3 '15 at 22:39
• @jaamlysi - Correct : $\alpha$ is not free in the undischarged assumptions left prior to $\forall$-I : see step 6. – Mauro ALLEGRANZA Jun 4 '15 at 6:14
• I suppose you're right: I assumed the notation in Definition 32 to stand for "$α$ is not a free variable in the preceding lines" instead of "$α$ is not a free variable in the assumptions" – jaam Jun 4 '15 at 11:49
• @jaamlysi - that is the "standard" convention in natural deduction ... but it seems to me that in your paper nowhere it is formally stated; I've assumed it, but it may be useful to check on some other source. – Mauro ALLEGRANZA Jun 4 '15 at 12:11