natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
transfinite arithmetic, cardinal arithmetic, ordinal arithmetic
prime field, p-adic integer, p-adic rational number, p-adic complex number
arithmetic geometry, function field analogy
The Church numerals are an encoding of the natural numbers into untyped lambda-calculus.
The th Church numeral is the operation of “iteration times”, sending a function to its th iterate. Thus is the identity function, , , and so on.
The Church numeral can be regarded as a realizer or “proof” that we can do induction up to . See this discussion.
Named after Alonzo Church.
Last revised on September 13, 2024 at 15:38:52. See the history of this page for a list of all contributions to it.