enter image description here

For example "Clearly there are operations e->e0, f->f1...".What would be an instance of such operations? And what does it mean the mapping c->h(g) ?

  • $\begingroup$ The subscript 0 and 1 just seem to denote the introduction rule for disjunction. The construction of $h$ and $g$ depends on $c : \neg (A \lor \neg A)$, so by discharging the assumption you get a function $\neg (A \lor \neg A) \to \bot$, i.e. $\neg\neg(A \lor\neg A)$. $\endgroup$ Commented May 25 at 18:55
  • $\begingroup$ Still trying to understand exactly what he meant but your comment was helpful, thanks! $\endgroup$
    – nskywalker
    Commented May 26 at 6:52
  • $\begingroup$ @NaïmFavier so the assumption to be discharged would be e or e0? $\endgroup$
    – nskywalker
    Commented May 27 at 11:35
  • $\begingroup$ No, the assumption is $c$. The final proof term is $\lambda c. (\lambda f. c(f_1)) (\lambda e. c(e_0))$. $\endgroup$ Commented May 27 at 11:37
  • $\begingroup$ See here for a better explanation of this proof. $\endgroup$ Commented May 27 at 11:41


You must log in to answer this question.

Browse other questions tagged .