Proof checking
Type theory
A formal foundation in which terms have types and propositions can be types.
Definition
Type theory
Type theory specifies how terms, types, functions, and equality are formed and checked.
Dependent type theory lets types mention values. Systems in the Lean family use this structure to represent mathematical statements and proofs.
01
Example
A proof of P → Q is represented as a function that turns any proof of P into a proof of Q.
02
Important distinction
Different type theories choose different primitive rules, equality rules, and universes.
After reading this article, you should be able to
- Define Type theory in the sense used on this site.
- Explain the propositions-as-types interpretation for implication.