The Curry Howard Isomorphism said that types are propositions and programs are their proofs. A proposition is an assertion (declarative statement), which is either true or false (but not both).
Consider the following examples of propositions:
- The equation 2 * 3 = 5
- If it is storming outside, then I take an Uber to class; otherwise, I walk, and if it is sunny, then I ride my bicycle:
Variable | Clause |
a | It is storming outside |
b | I take an Uber to class |
c | I walk |
d | It is sunny |
e | I ride my bicycle |
The following is the written logic version:
a implies b and ((not a) implies (c and (d implies e)))
The following is the logical symbols version:
(a ⇒ b) ∧ (¬a ⇒ (c ∧ (d⇒ e)))