# nLab type

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).

# Contents

## Idea

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.)

## Definition

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

## Properties

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.

Revised on October 20, 2014 16:13:38 by Urs Schreiber (185.26.182.29)