Line 34: |
Line 34: |
| ===Step 2=== | | ===Step 2=== |
| | | |
− | <pre>
| + | Assign types in the following specification: |
− | Assign types in the specification: | |
| | | |
− | x_A = x_A I_(A=>A)
| + | {| align="center" cellpadding="8" width="90%" |
| + | | <math>x_A ~=~ x_A \operatorname{I}_{A \Rightarrow A}</math> |
| + | |} |
| | | |
− | to arrive at a propositional typing for I : A => A,
| + | A suitable type assignment provides a propositional typing for <math>\operatorname{I} : A \Rightarrow A,</math> whose type, read as a proposition, is a theorem of intuitionistic propositional calculus. |
− | whose type, read as a proposition, is a theorem of | |
− | intuitionistic propositional calculus. | |
− | </pre>
| |
| | | |
| ===Step 3 (Optional)=== | | ===Step 3 (Optional)=== |