This entry is about the notion in type theory. For the unrelated notion of the same name in model theory see at

type (in model theory).

**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**

In modern logic, we understand that every variable should have a *type*, or *domain of discourse* or be of some *sort*. For instance we say that if a variable $n$ is constrained to be an integer then “$n$ is of integer type” or “of type $\mathbb{Z}$”. The usual formal expression from set theory for this – $n \in \mathbb{Z}$ – is then often written $n \colon \mathbb{Z}$

We speak of *typed logic* if this typing of variables is enforced by the metalanguage. In formulations of a theory the types are often called *sorts*. More generally, *type theory* formalizes reasoning with such typed variables. See there for more

(Untyped logic may be seen as simply a special case, in which there is only a single unique type. Thus, untyped logic has *one* type, not *no* type.)

Reasoning with types is formalized in natural deduction (which in turn is formalized in a logical framework such as Elf).

Behaviour of types is specified by a 4-step set of rules

Deep relations between type theory, category theory and computer science relate types to other notions, such as objects in a category. See at *computational trinitarianism* for more on this.

Last revised on April 27, 2017 at 13:01:46. See the history of this page for a list of all contributions to it.