user1838636
Reputation
Top tag
Next privilege 10 Rep.
 May1 awarded Tumbleweed Apr25 revised Removing backups in an exponential fashion added 397 characters in body Apr24 revised Removing backups in an exponential fashion edited body Apr24 revised Removing backups in an exponential fashion added 4 characters in body Apr24 revised Removing backups in an exponential fashion edited body Apr24 asked Removing backups in an exponential fashion Feb9 accepted Curry-Howard isomorphism for disjunction elimination Feb6 answered Curry-Howard isomorphism for disjunction elimination Feb6 revised Expection operator defined on colors deleted 3 characters in body Feb6 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? Feb6 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. Feb6 asked Curry-Howard isomorphism for disjunction elimination Nov25 awarded Scholar Nov25 accepted Expection operator defined on colors Nov25 answered Expection operator defined on colors Nov22 awarded Editor Nov22 revised Expection operator defined on colors edited body Nov22 awarded Student Nov22 asked Expection operator defined on colors