Logic: Curry-Howard Correspondence and Natural numbers

The foundations of Lean represent "all" of Mathematics. This means:

• The Curry-Howard correspondence: proofs are programs, propositions are types; allows logical connectives to be represented and rules of deduction to be implemented.
• The basic objects of Mathematics are constructed in terms of inductive types.
• The basic relations of Mathematics are constructed in terms of inductive types.

We will illustrate the latter two points in the context of Natural numbers.

Classical logic: example Natural Numbers

• A language is a set of constants, (n-ary) functions, (n-ary) predicates (relations).
  • For natural numbers:
    • Constant: 0
    • Functions: succ, +, ×
    • Predicates: =, ≤
• Mathematical objects: Terms, are built from
  • Constants
  • Variables: fixed (countably infinite) set of variables x₀, x₁, ...
  • Functions applied to terms
• Properties, i.e., Formulas are built from
  • Predicates applied to terms
  • Logical connectives: ∧, ∨, ¬, →, ↔
  • Quantifiers: ∀, ∃
• Theory: Axioms are formulas that are assumed to be true.
  • For natural numbers: Peano axioms
  • We also include logical axioms, example excluded middle.
• Deduction rules: Proofs are constructed from
  • Rules of inference: Modus ponens, i.e., A → B, A implies B., Generalization, i.e., A implies ∀ x, A.

Logic in Lean

• Propositions are types.
• Proofs are terms.
• The logical connectives are inductive types or constructions from inductive types:
  • Implicication is represented by A → B is a function from A to B.
  • False, True
  • And, Or
  • Not is A → False
  • forall, exists

Quantifiers

• ∀ x : α, P x is (x : α) → P x.
• ∃ x : α, P x is ∃ x, P x or Exists (fun x => P x).
  • A proof of existence is a pair consisting of
    • x : α for which P x holds.
    • A proof (witness) that P x holds.

def forall_example : Prop

Equations

• forall_example = ∀ (x : Nat), x = x

def exists_example : Prop

Equations

• exists_example = ∃ (x : Nat), x = x

Constructing the Language of Natural Numbers

• Our rules should allow us to constuct the "set" of natural numbers.
• We should be able to define the operations on natural numbers.
• We should be able to define the relations on natural numbers.
• We should be able to represent the axioms of Peano arithmetic, including the induction axiom schema.
• Our constructions should be such that all the axioms are theorems.

def MyNat.mul (m n : MyNat) : MyNat

Equations

• MyNat.zero.mul n = MyNat.zero
• m'.succ.mul n = n #+# m'.mul n

The subtle point is to define relations such as ≤ and =. These are indexed inductive types.

inductive MyNat.le : MyNat → MyNat → Prop

• refl (n : MyNat) : n.le n
• step (m n : MyNat) : m.le n → m.le n.succ

def MyNat.one : MyNat

Equations

• MyNat.one = MyNat.zero.succ

def MyNat.two : MyNat

Equations

• MyNat.two = MyNat.one.succ

instance MyNat.instLE : LE MyNat

Equations

• MyNat.instLE = { le := MyNat.le }

theorem MyNat.zero_le (n : MyNat) : MyNat.zero ≤ n

theorem MyNat.le_refl (n : MyNat) : n ≤ n

The induction principle encodes not only that refl and step are constructors of le, but also that they are the only ways to prove le.

Transitivity of ≤ is a theorem.

theorem MyNat.le_trans {m n k : MyNat} : m ≤ n → n ≤ k → m ≤ k

What is recursion?

When an inductive type like MyNat is defined, the following are automatically defined:

• MyNat
• Its constructors: zero, succ
• Recursion principle: MyNat.rec

Further, some equality principles are automatically defined:

For defining functions from MyNat to MyNat, we have a simple "motive".

noncomputable def MyNat.fctrl : MyNat → MyNat

Equations

• t.fctrl = MyNat.rec MyNat.one (fun (n p : MyNat) => n.succ.mul p) t