6 reputation
4
bio website
location
age
visits member for 1 year, 8 months
seen May 14 at 9:21

May
1
awarded  Tumbleweed
Apr
25
revised Removing backups in an exponential fashion
added 397 characters in body
Apr
24
revised Removing backups in an exponential fashion
edited body
Apr
24
revised Removing backups in an exponential fashion
added 4 characters in body
Apr
24
revised Removing backups in an exponential fashion
edited body
Apr
24
asked Removing backups in an exponential fashion
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