Matpic
mathematics, in pictures
Concept

Type theory

A system of rules that gives every term in a calculation a type and allows only combinations whose types fit. It began as a guard against paradox and now underlies programming languages and proof assistants, where a program's type is the statement it proves.

Named by 2 essays across one field — each of them below, with the objects they name alongside it.

Does this set contain that one — and the row that is missing. A membership table with the diagonal marked, and beneath it the complement of the diagonal, which is not among the rows.

A list that cannot contain itself

The set of all sets that do not contain themselves is not a set. The argument is the diagonal again, applied to a table whose rows and columns are the same objects, and it destroyed the foundations of mathematics in a postcard.

logic · Diagonalisation Ackermann's function as one polymorphic term. A : N → N → N; A(0,0)=1 in 6 steps, A(0,1)=2 in 6 steps, A(0,2)=3 in 6 steps, A(0,3)=4 in 6 steps, A(0,4)=5 in 6 steps, A(0,5)=6 in 6 steps, A(1,0)=2 in 10 steps, A(1,1)=3 in 13 steps, A(1,2)=4 in 16 steps, A(1,3)=5 in 19 steps, A(1,4)=6 in 22 steps, A(1,5)=7 in 25 steps, A(2,0)=3 in 17 steps, A(2,1)=5 in 33 steps, A(2,2)=7 in 55 steps, A(2,3)=9 in 83 steps, A(2,4)=11 in 117 steps, A(2,5)=13 in 157 steps, A(3,0)=5 in 37 steps, A(3,1)=13 in 191 steps, A(3,2)=29 in 881 steps, A(3,3)=61 in 3795 steps, A(3,4)=125 in 15765 steps.

One type for every use

In the simply typed calculus a numeral must be told in advance what kind of thing it will iterate, and with input and output of one type it computes only polynomials with tests. Let a single type stand for every type — a numeral is then a term of type ∀X. (X → X) → X → X, used at whatever type each occasion needs — and the same few symbols compute subtraction, exponentials and Ackermann's function, which grows faster than anything built from primitive recursion. Every run still finishes, and the proof that it does lies just beyond the reach of second-order arithmetic.

logic · Proof systems

Named alongside it

The objects these essays reach for when they reach for this one.

ConsistencyComprehensionComputationDiagonal argumentMembershipNormal formProof systemRecursionRussell paradoxSelf-referenceSet theoryTermination

All concepts