nLab constant of a theory



In logic, particularly in the syntactic notion of a (first-order) theory, a constant is a term without free variables, modulo equivalence imposed by equational axioms of the theory.


Recall that a signature Σ\Sigma of a theory (let us say a one-sorted theory, for the sake of simplicity) consists of constant symbols together with function symbols and relation symbols with assigned arities. Then

  • A constant symbol cc of Σ\Sigma is considered a constant term of the theory, and

  • If ff is a function symbol of arity nn and c 1,,c nc_1, \ldots, c_n are constant terms, then f(c 1,,c n)f(c_1, \ldots, c_n) is a constant term of the theory.

[Note that in some accounts, constant symbols are considered as function symbols of arity zero.]

For instance, the theory of rings is typically presented by a signature (R,+,,,0,1)(R, +, -, \cdot, 0, 1) where RR denotes the sort, with binary operations +,,+, -, \cdot and constant (symbols) 0,10, 1, whence other constant terms may be derived such as (1+1)((01)1)(1 + 1) \cdot ((0-1) -1).

Constant terms are syntactic expressions derived from the signature, but the axioms of the theory may impose equations between constant terms; for example, the equational axioms of ring theory force equations like

(1+1)((01)1)=0(1+((1+1)+1))(1 + 1) \cdot ((0-1) -1) = 0 - (1 + ((1 + 1) + 1))

so that what one is really after is equivalence classes of syntactic expressions. A constant of the theory is such an equivalence class of constant terms.


Let RR be a fixed commutative ring. The theory of RR-algebras may be presented just as the theory of rings, but including a constant symbol c rc_r for each element rRr \in R, and adding equations c 0=0c_0 = 0, c 1=1c_1 = 1, c r+c s=c r+sc_r + c_s = c_{r+s}, c rs=c rc sc_{r-s} = c_r - c_s, and c rc s=c rsc_r \cdot c_s = c_{r s}.

Constants of algebraic theories

For a more semantic description, suppose TT is a Lawvere theory, and let

Set T=Prod(T,Set)Set^T = \mathbf{Prod}(T, Set)

denote the category of TT-algebras = product-preserving functors TSetT \to Set. Then there is a forgetful functor

U:Set TSet,U: Set^T \to Set,

and constants of TT may be identified, up to natural isomorphism, with natural transformations of the form

1U1 \to U

(where 1=U 01 = U^0 here denotes the terminal functor Set TSetSet^T \to Set). Alternatively, constants of TT may be naturally identified with morphisms in the hom-set T(i(0),i(1))T(i(0), i(1)) where i:FinSet opTi: FinSet^{op} \to T is the product-preserving functor given as one of the data for TT.

The same idea applies to any infinitary algebraic theory.

From this point of view, identifying (equivalence classes of) nn-ary operations of TT with natural transformations f:U nUf: U^n \to U, one also often says that ff is constant if it factors through the unique map U n1U^n \to 1, as in constant morphism.

For example, for the Lawvere theory of commutative RR-algebras, nn-ary operations U nUU^n \to U are in natural bijection with polynomials pR[x 1,,x n]p \in R[x_1, \ldots, x_n], and such a pp is constant iff it belongs to the image of the canonical inclusion map RR[x 1,,x n]R \to R[x_1, \ldots, x_n]. See also constant polynomial.

Last revised on July 26, 2023 at 19:46:10. See the history of this page for a list of all contributions to it.