Here is a table of logical symbols/connectives/quantifiers and their computational equivalents.

Note that I slightly transformed Lean 4 inductives here: turned all `structure`

s into `inductive`

s (to make the format consistent), removed comments, and wrote all `Type (max u v)`

as `Type _`

(just to save some space).

Logic | Computation |
---|---|

inductive False : Prop | inductive Empty : Type |

inductive True : Prop where| intro | inductive Unit : Type where| unit |

inductive And (a : Prop) (b : Prop) : Prop where| intro (left : a) (right : b) | inductive Prod (α : Type u) (β : Type v) : Type _ where| mk (fst : α) (snd : β) |

inductive Or (a : Prop) (b : Prop) : Prop where| inl (h : a)| inr (h : b) | inductive Sum (α : Type u) (β : Type v) : Type _ where| inl (val : α)| inr (val : β) |

inductive Exists {α : Sort u} (p : α → Prop) : Prop where| intro (w : α) (h : p w) | inductive Sigma {α : Type u} (β : α → Type v) : Type _ where| mk (fst : α) (snd : β fst) |

The only difference between the logical connectives and their computational equivalents is the fact that former return a `Prop`

(`Sort 0`

), and the latter return a `Type _`

(`Sort 1+`

).

**Elimination rules **from formal logic correspond to

ing. Whenever you declare an inductive, e.g. **match**`inductive MyType`

, Lean automatically gives you the `match MyType.intro a b`

, `MyType.casesOn`

, `MyType.rec`

, and multiple other functions (in case of `Exists`

and `Or`

, Lean also gives us `Exists.elim`

and `Or.elim`

, but this is just syntax sugar). All of them compile to `MyType.rec`

- a so-called recursor function.**Introduction rules** from formal logic correspond to using type **constructors** (`And.intro`

, `Or.inl`

, `Or.inr`

, etc.). For example, `∨I`

is represented as `Or.inl proofOfA`

.

Here is a table with notation for the types above.

Inductives | Expression | Sugar |
---|---|---|

inductive False, inductive Empty | `False` , `Empty` | |

inductive True, inductive Unit | `True` , `Unit` | |

inductive And, inductive Prod | `And a b` | == `a ∧ b` |

`Prod α β` | == `α × β` | |

inductive Or, inductive Sum | `Or a b` | == `a ∨ b` |

`Sum α β` | == `α ⊕ β` | |

inductive Exists, inductive Sigma | `Exists (λ x : α => p)` | == `∃ x : α, p` |

`Sigma (λ a : α => β a)` | == `Σ a : α, β a` == `(a : α) × β a` |

Notice how the notation we're used to refers to the use of the inductive type itself (and not to the use of its constructors). For example, `a ∧ b`

means `And a b`

(and not

).~~And.intro hA hB~~

The only exceptions to this rule are:

`()`

, which is sugar for`Unit.unit`

(and not`Unit`

); and`(2, 3)`

, which is sugar for`Prod.mk 2 3`

(and not`Prod 2 3`

).

**Prod** is also called a **pair**.**Sigma** is also called a **dependent pair**.