Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
intuitionistic_propositional_logic [2016/04/13 11:17] nikolaj |
intuitionistic_propositional_logic [2016/04/13 11:20] nikolaj |
||
|---|---|---|---|
| Line 309: | Line 309: | ||
| $(A\to B)\land((A\to B)\to B)\to B$ | $(A\to B)\land((A\to B)\to B)\to B$ | ||
| - | "If it's the case that 'A implies B' and also that 'A implies B' implies B, then B is the case." | + | "If it's the case that '$A$ implies $B$' and also that '$A$ implies $B$' implies $B$, then $B$ is the case." |
| Under the BHK interpretation (Curry-Howard), this reads" | Under the BHK interpretation (Curry-Howard), this reads" | ||
| - | "Given any 'function to $B$', that we may call $f$, as well as a function $F$ from a 'functions to $B$' to $B$, you can construct an element $F(f)$ of $B$. | + | "Given any 'function to $B$', that we may call $f$, as well as a function $F$ from a 'functions to $B$' to $B$, you can construct an element of $B$." |
| - | In type theory, the judgement is | + | The proof / the element is of course $F(f)$. In type theory, that judgement is |
| $\lambda x.(\pi_2x)(\pi_1 x)\ :\ (A\to B)\times((A\to B)\to B)\to B$ | $\lambda x.(\pi_2x)(\pi_1 x)\ :\ (A\to B)\times((A\to B)\to B)\to B$ | ||
