# nLab type

Contents

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.

Last revised on April 27, 2017 at 13:01:46. See the history of this page for a list of all contributions to it.
{"ft_lang_label":"__label__en","ft_lang_prob":0.7449473,"math_prob":0.961317,"size":4654,"snap":"2022-40-2023-06","text_gpt3_token_len":1154,"char_repetition_ratio":0.14709677,"word_repetition_ratio":0.0,"special_character_ratio":0.20004298,"punctuation_ratio":0.053672317,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9759243,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2023-01-27T21:00:23Z\",\"WARC-Record-ID\":\"<urn:uuid:375dff1e-030a-41ca-92af-cc0e47c2e7b0>\",\"Content-Length\":\"45807\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:2bf1ba8b-e61f-4c22-89ad-516d773aeadb>\",\"WARC-Concurrent-To\":\"<urn:uuid:c4963d14-372c-4f54-aaee-648afd09b54d>\",\"WARC-IP-Address\":\"128.2.25.48\",\"WARC-Target-URI\":\"https://ncatlab.org/nlab/show/type\",\"WARC-Payload-Digest\":\"sha1:MCSPYGOPGO7N34NCW2XGCMBKWVE4Q2FI\",\"WARC-Block-Digest\":\"sha1:FSSE6M5HZ4GMGSHTUNL7KJY4LSB623D7\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2023/CC-MAIN-2023-06/CC-MAIN-2023-06_segments_1674764495012.84_warc_CC-MAIN-20230127195946-20230127225946-00064.warc.gz\"}"}