title: Curious OCaml author: Lukasz Stafiniak header-includes:
What logical connectives do you know?
| $\top$ | $\bot$ | $\wedge$ | $\vee$ | $\rightarrow$ |
|---|---|---|---|---|
| $a \wedge b$ | $a \vee b$ | $a \rightarrow b$ | ||
| truth | falsehood | conjunction | disjunction | implication |
| "trivial" | "impossible" | $a$ and $b$ | $a$ or $b$ | $a$ gives $b$ |
| shouldn't get | got both | got at least one | given $a$, we get $b$ |
How can we define them? Think in terms of derivation trees:
$$ \frac{ \frac{\frac{\,}{\text{a premise}} \; \frac{\,}{\text{another premise}}}{\frac{\,}{\text{some fact}}} \; \frac{\frac{\,}{\text{a premise}} \; \frac{\,}{\text{another premise}}}{\frac{\,}{\text{another fact}}}} {\text{final conclusion}} $$
To define the connectives, we provide rules for using them: for example, a rule $\frac{a \; b}{c}$ matches parts of the tree that have two premises, represented by variables $a$ and $b$, and have any conclusion, represented by variable $c$.
Introduction rules say how to produce a connective. Elimination rules say how to use it. Text in parentheses is comments. Letters are variables: stand for anything.