first order language


Let Σ be a signaturePlanetmathPlanetmathPlanetmath. The first order language FO(Σ) on Σ contains the following:

  1. 1.

    the set S(Σ) of symbols of FO(Σ), which is the disjoint unionMathworldPlanetmath of the following sets:

    1. (a)

      Σ (the non-logical symbols),

    2. (b)

      a countably infiniteMathworldPlanetmath set V of variables,

    3. (c)

      the set of logical symbols {,,¬,,,,},

    4. (d)

      the singleton consisting of the equality symbol {=}, and

    5. (e)

      the set of parentheses (left and right) {(,)};

  2. 2.

    the set T(Σ) of terms of FO(Σ), which is built inductively from S(Σ), as follows:

    1. (a)

      Any variable vV is a term;

    2. (b)

      Any constant symbol in Σ is a term;

    3. (c)

      If f is an n-ary function symbol in Σ, and t1,,tn are terms, then f(t1,,tn) is a term.

  3. 3.

    the set F(Σ) of formulasMathworldPlanetmath of FO(Σ), which is built inductively from T(Σ), as follows:

    1. (a)

      If t1 and t2 are terms, then (t1=t2) is a formula;

    2. (b)

      If R is an n-ary relation symbol and t1,,tn are terms, then (R(t1,,tn)) is a formula;

    3. (c)

      If φ is a formula, then so is (¬φ);

    4. (d)

      If φ and ψ are formulas, then so is (φψ);

    5. (e)

      If φ is a formula, and x is a variable, then (x(φ)) is a formula.

In other words, T(Σ) and F(Σ) are the smallest sets, among all sets satisfying the conditions given for terms and formulas, respectively.

Formulas in 3(a) and 3(b), which do not contain any logical connectives, are called the atomic formulas.

For example, in the first order language of partially ordered rings, expressions such as

0,x2, and y+zx

are terms, while

(x=xy),(x+yyz), and (x((x0)(0x)))

are formulas, and the first two of which are atomic.

Remarks.

  1. 1.

    Generally, one omits parentheses in formulas, when there is no ambiguity. For example, a formula (φ) can be simply written φ. As such, the parentheses are also called the auxiliary symbols.

  2. 2.

    The other logical symbols are obtained in the following way :

    φψ :=def¬(¬φ¬ψ)   φψ :=def¬φψ
    φψ :=def(φψ)(ψφ)   x(φ) :=def¬(x(¬φ))

    where φ and ψ are formulas. All logical symbols are used when building formulas.

  3. 3.

    In the literature, it is a common practice to write Σωω for FO(Σ). The first subscript means that every formula in FO(Σ) contains a finite number of ’s (less than ω), while the second subscript signifies that every formula has a finite number of ’s. In general, Σαβ denotes a languagePlanetmathPlanetmath built from Σ such that, in any given formula, the number of occurrences of is less than α and the number of occurrences of is less than β. When the number of occurrences of (or ) in a formula is not limited, we use the symbol in place of α (or β). Clearly, if α and β are not ω, we get a language that is not first-order.

First Order Languages as Formal Languages

If the signature Σ and the set V of variables are countableMathworldPlanetmath, then S(Σ),T(Σ), and F(Σ) can be viewed as formal languagesMathworldPlanetmath over a certain (finite) alphabet Γ. The set Γ should include all of the logical connectives, the equality symbol, and the parentheses, as well as the following symbols

R,F,V,I,#,

where they are used to form words for relationMathworldPlanetmath, formula, and variable symbols. More precisely,

  • VIn# stands for the variable vn,

  • RIn#Im# stands for the m-th relation symbol of arity n, and

  • FIn#Im# stands for the m-th function symbol of arity n,

where m,n0 are integers. The symbol # is used as a delimiter or separator. Note that the constant symbols are then words of the form F#Im#. It can shown that S(Σ),T(Σ) and F(Σ) are context-free over Γ, and in fact unambiguous.

References

  • 1 W. Hodges, A Shorter Model TheoryMathworldPlanetmath, Cambridge University Press, (1997).
  • 2 D. Marker, Model Theory, An Introduction, Springer, (2002).
Title first order language
Canonical name FirstOrderLanguage
Date of creation 2013-03-22 12:42:46
Last modified on 2013-03-22 12:42:46
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 28
Author CWoo (3771)
Entry type Definition
Classification msc 03C07
Classification msc 03B10
Synonym auxiliary symbol
Synonym first-order language
Related topic Type2
Related topic Language
Related topic AtomicFormula
Defines first order language
Defines term
Defines formula