Shahada ya kwanza (juu)FoundationsImepangwa
Type theory and propositions as types
Simply typed and dependent type theories, the Curry–Howard correspondence between proofs and programs, inductive types, and the type theory behind proof assistants such as Lean, compared with axiomatic set theory.
math.found.type-theory
Somo la mada hii bado halijaandikwa. Muhtasari ulio hapa chini ni sehemu ya ramani ya mtaala na haujakaguliwa.
Inajengwa juu ya
Masharti ya awali ya lazima 17 (hadi chini kabisa)
Utajifunza
- Type-check terms of the simply typed λ-calculus and read them as proofs in intuitionistic propositional logic.
- Explain dependent function (Π) and dependent pair (Σ) types and use them to express ∀ and ∃.
- Define the natural numbers and lists as inductive types and derive their induction principles.
- Contrast a type-theoretic foundation, where every term has a type, with ZFC, where everything is a set and membership is global.
Fasili
- A typing judgement t : A asserts that the term t has type A.
- Curry–Howard correspondence: propositions correspond to types and proofs to terms; implication corresponds to function types.
- An element of a dependent function type Π (x : A), B(x) sends each a : A to an element of B(a).
- An inductive type is freely generated by its constructors; for example ℕ is generated by zero and succ.
Nadharia
- The simply typed λ-calculus is strongly normalising.
- Normalisation of proofs in intuitionistic natural deduction corresponds to β-reduction of typed λ-terms.
- Lean's logic is a dependent type theory in the tradition of the calculus of inductive constructions, with a hierarchy of universes; classical principles such as choice are added as explicit axioms.
Mawazo potofu ya kawaida
- Thinking type theory and set theory are interchangeable; they have different primitive notions and are related by interpretations, not identical.
- Treating types as sets: a term has its type as part of its meaning, whereas a set may belong to many unrelated sets.
- Assuming every program is a meaningful proof; in a consistent type theory, non-terminating terms are excluded.
Inaelekea kwa
Ugunduzi wa hiari
- Proof theory Normalisation of typed λ-terms corresponds to removing detours in natural-deduction proofs, a central theme of proof theory.
- Formal methods Dependent types let programs carry machine-checked proofs of their own specifications.
- ← Propositional logic and truth tables
- ← Russell's paradox and why sets need axioms
- ← First steps in Lean
- ← Formalising mathematics in Lean and Mathlib
- ← ZFC: axiomatic set theory
Njia za kujifunza
Usomaji zaidi
- Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, Theorem Proving in Lean 4
- Jean-Yves Girard, Yves Lafont and Paul Taylor, Proofs and Types (1989)
- Rob Nederpelt and Herman Geuvers, Type Theory and Formal Proof: An Introduction (2014)