本科高年级Foundations课程已上线

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

打开课程显示到达此主题所需的全部内容

前置知识

First-order logic The λ-calculus

17 项必需的前置知识（一直追溯到底）

你将学会

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.

定义

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.

定理

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.

常见误解

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.

通向

Categorical logic Homotopy type theory Formalising published mathematics

可选发现

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

学习路径

Computer science and formal methods