Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
intuitionistic_propositional_logic [2016/04/13 11:19] nikolaj |
intuitionistic_propositional_logic [2016/08/28 01:17] nikolaj |
||
|---|---|---|---|
| Line 307: | Line 307: | ||
| In fact, take any $A,B$ and observe that | In fact, take any $A,B$ and observe that | ||
| - | $(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 $b$ 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$." |
| - | The proof is of course $b=F(f)$. In type theory, that 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$ | ||
