nLab signature (in logic)

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

In logic, a signature is a collection of data which prescribes the ‘alphabet’ of non-logical symbols of a logical theory, saying which operations and predicates are taken to be primitive.

The signature of a structure is the union of the collection of constant symbols, function symbols, and relation symbols in the language of said structure.

Definition

Types

Formally, a signature Σ\Sigma consists of

  • A set SS whose elements are called sorts or types of Σ\Sigma,

  • A set Rel(Σ)Rel(\Sigma) whose elements are called relation symbols, equipped with a function ar:Rel(Σ)S *ar: Rel(\Sigma) \to S^* to the free monoid on SS which prescribes an arity for each relation symbol,

  • A set Func(Σ)Func(\Sigma) whose elements are called function symbols, equipped with a function

    dom,cod:Func(Σ)S *×S\langle dom, cod \rangle: Func(\Sigma) \to S^* \times S

    which prescribes an arity or type for each function symbol. A function symbol ff may be written as dom(f)cod(f)dom(f) \to cod(f), or as d 0(f)d 1(f)d_0(f) \to d_1(f), to indicate its arity.

The majority of (but far from all) mathematical concepts are described by means of a single-sorted signature, where SS consists of a single element XX. Examples where multisorted signatures are used is the theory of categories (with an object sort and a morphism sort) and (multi)directed graphs (with a vertex sort and an edge sort). But in the single-sorted or one-sorted case, the free monoid on the one-sort set is isomorphic to \mathbb{N}, and the arity of a relation is a number nn. Hence we speak of an nn-ary relation (unary, binary, etc.). Similarly, the arity of a function symbol or operation ff is the number nn which indexes dom(f)dom(f) (hence we speak of unary operations, binary operations, etc.) In either the single-sorted or multisorted case, a 0-ary operation (where the domain empty) is usually called a constant.

A relational signature is where Func(Σ)Func(\Sigma) is empty, and an equational or algebraic signature is where Rel(Σ)Rel(\Sigma) is empty. (In the latter case, the only relation symbol is the equality symbol, but this is typically considered a logical symbol.) Occasionally one allows a relational signature to have constants.

Models

A (set-theoretic) model or interpretation MM of a signature consists of functions which assign

  • To each sort ss a set M(s)M(s),

  • To each relation symbol RR of arity s 1,,s n\langle s_1, \ldots, s_n \rangle a subset M(R)M(s 1)××M(s n)M(R) \hookrightarrow M(s_1) \times \ldots \times M(s_n),

  • To each function symbol ff of type s 1,,s ns\langle s_1, \ldots, s_n \rangle \to s a function M(f):M(s 1)××M(s n)M(s)M(f): M(s_1) \times \ldots \times M(s_n) \to M(s). Such a function is called an operation (that interprets ff). In the case of constants of type ss, the empty product on the left is taken to be a terminal or 1-element set 11, whose element needs no name but is often given a generic name like ‘**’.

More generally a signature may be interpreted in other categories CC besides Set; for this it is reasonable to suppose that CC is at least a regular category. See also

Theories

In terms of a signature one may formulate propositions, sequents and then theories. See there for more details.

Examples

An important point to bear in mind is that essentially the same theories (where ‘same’ means that the categories of models are equivalent or even isomorphic) may have very different signatures. For example,

  • The theory of groups is usually described as a single-sorted theory whose signature has one binary operation (called ‘multiplication’) mm, one constant ee (called ‘identity’), and one unary operation (called ‘inversion’) ii. But it can also be described using a signature with just one (binary) operation mm; there one adds in extra axioms which posit the existence of an identity and of inverse elements. Or, it can be described using a signature with a single (binary) operation dd (for ‘division’). All these are examples of equational signatures.

  • A Boolean ring is usually described as a commutative ring with identity in which multiplication is idempotent, hence the theory of Boolean rings is usually presented using the signature normally reserved for rings (with identity). A Boolean algebra may be described using a variety of signatures, for example non-equationally, involving a binary relation \leq and function symbols \wedge, ¬\neg, \top.

  • The theory ZFC is usually described using a single-sorted relational signature with one binary relation \in. However, other approaches are possible: one can also describe ZFC with a relational symbol \subseteq together with a unary function symbol singsing (to be interpreted as taking a ‘set’ SS, i.e., an element of a ZFC structure, to a singleton ‘set’ {S}\{S\}).

Remarks

The multiplicity of ways in which one can describe essentially the same class of objects is a phenomenon which in higher category theory is often referred to as bias. Often one desires to use an ‘unbiased’ approach which includes different signatures under one roof and on the same footing. In the case of algebraic (equational) theories, this can be done using the device of clones or Lawvere theories, which does not single out certain non-logical operations as ‘privileged’.

There are several reasons though why one might prefer to retain some bias, for example:

  • Tradition, familiarity, thus ease of reference. For example, a group is a set equipped with a binary mm, an unary ii, and a constant ee, rather than a set equipped with a single division operation, or a finite product-preserving functor for that matter.

  • Mathematical intuition. That is, different signatures may invoke different intuitions or attitudes toward a subject; for example, “Boolean rings” may invoke a more algebraic or algebro-geometric attitude (as in Stone duality) whereas “Boolean algebras” may invoke a more logical attitude (propositional logic).

  • Differences in logical strength. That is, first-order logic should be thought of as coming in layers, ranging from equational logic up to pretopos logic, and different signatures may need differing levels of logical strength for them to be interpreted as intended. Equational logic may be preferred on occasion because it is a very weak logic, whereas relational signatures often require at least the strength of regular categories for them to be interpreted correctly.

The language of a signature

Each signature Σ\Sigma generates a language whose elements are first-order predicates: expressions formed by using an alphabet of logical symbols together with Σ\Sigma, considered as an alphabet of non-logical symbols, according to certain rules. For an account of the traditional logical syntax, see Wikipedia.

First-order languages can also be structured categorically through the notion of hyperdoctrine. The base of the hyperdoctrine is a cartesian monoidal category Term(Σ)\mathbf{Term}(\Sigma) consisting of sorts and terms, or rather, the objects are formal (cartesian) products of sorts, written as finite lists, and the morphisms are tuples of terms generated by the function symbols of the signature. A detailed categorical description of Term(Σ)\mathbf{Term}(\Sigma) may be found here.

Given the base Term(Σ)\mathbf{Term}(\Sigma), the language itself is structured as a certain Boolean hyperdoctrine, i.e., a functor

Lang(Σ):Term(Σ) opBoolLang(\Sigma): \mathbf{Term}(\Sigma)^{op} \to Bool

where for each morphism ff in the base, the morphism f *=Lang(Σ)(f)f^\ast = Lang(\Sigma)(f) has a left adjoint f\exists_f and a right adjoint f\forall_f, subject to a Beck-Chevalley condition for each pullback square in the base. To describe it with more traditional logical terminology: the functor takes each object (i.e., product of sorts) w=s 1s 2s nw = s_1 s_2 \ldots s_n to the Boolean algebra Pred(w)Pred(w) of predicates of arity ww that built up from the formal relations of the signature using first-order logic operations. The sorts s is_i appearing in the arity are matched bijectively with the free variables of the predicate, and are the types of those variables. Then, the functor takes each morphism f:vwf: v \to w, given by an nn-tuple of terms τ i:vs i\tau_i: v \to s_i, to the Boolean algebra map f *:Pred(w)Pred(v)f^\ast: Pred(w) \to Pred(v) obtained by substituting, in predicates of arity ww, the term τ i\tau_i for the free variable x ix_i that is matched with s is_i, resulting in a predicate of arity vv.

A more precise categorical description of Lang(Σ)Lang(\Sigma), in terms of a universal property, is as follows. Let S *S^\ast denote the underlying set of free monoid generated by the set of sorts SS; regard S *S^\ast as a discrete category. The formal relations of the signature give a functor

i:S *Seti: S^\ast \to Set

sending each product w=s 1s nw = s_1 \ldots s_n to the set of relations RRel(Σ)R \in Rel(\Sigma) that have arity ww. Let j:S *Term(Σ)j: S^\ast \to \mathbf{Term}(\Sigma) be the obvious inclusion functor (the identity on objects). Define an interpretation of Σ\Sigma to be a pair consisting of a Boolean hyperdoctrine M:Term(Σ) opBoolM: \mathbf{Term}(\Sigma)^{op} \to Bool together with a natural transformation ϕ:iUMj\phi: i \to U M j:

S * i Set j ϕ U Term(Σ) op M Bool\array{ S^\ast & \stackrel{i}{\to} & Set \\ \mathllap{j} \downarrow & \Downarrow \mathrlap{\phi} & \uparrow \mathrlap{U} \\ \mathbf{Term}(\Sigma)^{op} & \underset{M}{\to} & Bool }

where U:BoolSetU: Bool \to Set is the underlying set functor. There is an obvious notion of morphism between interpretations (M,ϕ)(M,ϕ)(M, \phi) \to (M', \phi'), given by a natural transformation MMM \Rightarrow M' compatible with the data ϕ,ϕ\phi, \phi'.

Definition

The language Lang(Σ)Lang(\Sigma) is the initial object in the category of interpretations of Σ\Sigma.

References

  • Categorical Logic and Type Theory, Bart Jacobs

Last revised on February 14, 2024 at 06:53:34. See the history of this page for a list of all contributions to it.