user1838636
Reputation
Top tag
Next privilege 10 Rep.
 May 1 awarded Tumbleweed Feb 9 accepted Curry-Howard isomorphism for disjunction elimination Feb 6 answered Curry-Howard isomorphism for disjunction elimination Feb 6 revised Expection operator defined on colors deleted 3 characters in body Feb 6 comment Curry-Howard isomorphism for disjunction elimination Sorry for the many edits, it is a bit cumbersome on this website to stage an elaborate message as a comment. Wel, $P \vee Q$ is easily modeled as $(P \rightarrow \bot) \rightarrow Q$. My problem is that it does not seem possible to create a lambda term for disjunction elimination (disjunction introduction is not a problem though). Or am I missing something here? Feb 6 comment Curry-Howard isomorphism for disjunction elimination I would like to point out that $\wedge I$ and $\wedge E$ are possible to model without product object, by using the following definition: $P \wedge Q \equiv (P \rightarrow (Q \rightarrow \bot)) \rightarrow \bot$ Now, we can have $\wedge I$ like $\lambda p . \lambda q . \lambda a . p q$. For $\wedge E$, we then have $\lambda a . \text{doubleNegElim} \; (\lambda x . a (\lambda y . x y))$. Here $\text{doubleNegElim}$ is some continuation function. I guess my problem is that if I'm able to define this for $\wedge$, why cant I define it for $\vee$ without introducing extra constructs. Feb 6 asked Curry-Howard isomorphism for disjunction elimination Nov 25 awarded Scholar Nov 25 accepted Expection operator defined on colors Nov 25 answered Expection operator defined on colors Nov 22 awarded Editor Nov 22 revised Expection operator defined on colors edited body Nov 22 awarded Student Nov 22 asked Expection operator defined on colors