Differences
This shows you the differences between two versions of the page.
| Both sides previous 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:19] nikolaj |
||
|---|---|---|---|
| Line 313: | Line 313: | ||
| 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 $b$ of $B$." |
| - | In type theory, the judgement is | + | The proof is of course $b=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$ | ||
