0
$\begingroup$

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?

$\endgroup$
0
$\begingroup$

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].

$\endgroup$
  • $\begingroup$ 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) $\endgroup$ – jaam Jun 3 '15 at 22:39
  • $\begingroup$ @jaamlysi - Correct : $\alpha$ is not free in the undischarged assumptions left prior to $\forall$-I : see step 6. $\endgroup$ – Mauro ALLEGRANZA Jun 4 '15 at 6:14
  • $\begingroup$ 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" $\endgroup$ – jaam Jun 4 '15 at 11:49
  • $\begingroup$ @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. $\endgroup$ – Mauro ALLEGRANZA Jun 4 '15 at 12:11

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.