Quantifier (logic)
Formal semantics

Mathematical semantics is the application of mathematics to study the meaning of expressions in a formal language. It has three elements: a mathematical specification of a class of objects via syntax, a mathematical specification of various semantic domains and the relation between the two, which is usually expressed as a function from syntactic objects to semantic ones. This article only addresses the issue of how quantifier elements are interpreted.The syntax of a formula can be given by a syntax tree. A quantifier has a scope, and an occurrence of a variable x is free if it is not within the scope of a quantification for that variable. Thus in

the occurrence of both x and y in C (y, x) is free, while the occurrence of x and y in B (y, x) is bound (i.e. non-free).

An interpretation for first-order predicate calculus assumes as given a domain of individuals X. A formula A whose free variables are x,..., x is interpreted as a Boolean -valued function F (v,..., v) of n arguments, where each argument ranges over the domain X. Boolean-valued means that the function assumes one of the values T (interpreted as truth) or F (interpreted as falsehood). The interpretation of the formula

is the function G of n -1 arguments such that G (v,..., v) = T if and only if F (v,..., v, w) = T for every w in X. If F (v,..., v, w) = F for at least one value of w, then G (v,..., v) = F. Similarly the interpretation of the formula

is the function H of n -1 arguments such that H (v,..., v) = T if and only if F (v,..., v, w) = T for at least one w and H (v,..., v) = F otherwise.

The semantics for uniqueness quantification requires first-order predicate calculus with equality. This means there is given a distinguished two-placed predicate "="; the semantics is also modified accordingly so that "=" is always interpreted as the two-place equality relation on X. The interpretation of

then is the function of n -1 arguments, which is the logical and of the interpretations of

Each kind of quantification defines a corresponding closure operator on the set of formulas, by adding, for each free variable x, a quantifier to bind x. For example, the existential closure of the open formula n >2 ∧ x + y = z is the closed formula ∃ n ∃ x ∃ y ∃ z (n >2 ∧ x + y = z); the latter formula, when interpreted over the positive integers, is known to be false by Fermat's Last Theorem. As another example, equational axioms, like x + y = y + x, are usually meant to denote their universal closure, like ∀ x ∀ y (x + y = y + x) to express commutativity.
change_case:english_capital