Editing First-order logic (section)

====Non-logical symbols====<!-- This section is linked from [[Axiom of empty set]] -->
[[Non-logical symbol]]s represent predicates (relations), functions and constants. It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes:

* For every integer ''n''&nbsp;≥&nbsp;0, there is a collection of [[arity|''n''-''ary'']], or ''n''-''place'', ''[[predicate symbol]]s''. Because they represent [[Finitary relation|relations]] between ''n'' elements, they are also called ''relation symbols''. For each arity ''n'', there is an infinite supply of them:
*:''P''<sup>''n''</sup><sub>0</sub>, ''P''<sup>''n''</sup><sub>1</sub>, ''P''<sup>''n''</sup><sub>2</sub>, ''P''<sup>''n''</sup><sub>3</sub>, ...
* For every integer ''n''&nbsp;≥&nbsp;0, there are infinitely many ''n''-ary ''function symbols'':
*:''f<sup> n</sup>''<sub>0</sub>, ''f<sup> n</sup>''<sub>1</sub>, ''f<sup> n</sup>''<sub>2</sub>, ''f<sup> n</sup>''<sub>3</sub>, ...

When the arity of a predicate symbol or function symbol is clear from context, the superscript ''n'' is often omitted.

In this traditional approach, there is only one language of first-order logic.<ref>More precisely, there is only one language of each variant of one-sorted first-order logic: with or without equality, with or without functions, with or without propositional variables, ....</ref> This approach is still common, especially in philosophically oriented books.

A more recent practice is to use different non-logical symbols according to the application one has in mind. Therefore, it has become necessary to name the set of all non-logical symbols used in a particular application. This choice is made via a ''[[signature (logic)|signature]]''.<ref>The word ''language'' is sometimes used as a synonym for signature, but this can be confusing because "language" can also refer to the set of formulas.</ref>

Typical signatures in mathematics are {1, ×} or just {×} for [[group (mathematics)|group]]s,<ref name="Tarski53"/> or {0, 1, +, ×, <} for [[ordered field]]s. There are no restrictions on the number of non-logical symbols. The signature can be [[empty set|empty]], finite, or infinite, even [[uncountable]]. Uncountable signatures occur for example in modern proofs of the [[Löwenheim–Skolem theorem]].

Though signatures might in some cases imply how non-logical symbols are to be interpreted, [[#Semantics|interpretation]] of the non-logical symbols in the signature is separate (and not necessarily fixed). Signatures concern syntax rather than semantics.

In this approach, every non-logical symbol is of one of the following types:

* A ''predicate symbol'' (or ''relation symbol'') with some ''valence'' (or ''arity'', number of arguments) greater than or equal to 0. These are often denoted by uppercase letters such as ''P'', ''Q'' and ''R''. Examples:
** In ''P''(''x''), ''P'' is a predicate symbol of valence 1. One possible interpretation is "''x'' is a man".
** In ''Q''(''x'',''y''), ''Q'' is a predicate symbol of valence 2. Possible interpretations include "''x'' is greater than ''y''" and "''x'' is the father of ''y''".
** Relations of valence 0 can be identified with [[propositional variable]]s, which can stand for any statement. One possible interpretation of ''R'' is "Socrates is a man".
* A ''function symbol'', with some valence greater than or equal to 0. These are often denoted by lowercase [[Latin script|roman letters]] such as ''f'', ''g'' and ''h''. Examples:
** ''f''(''x'') may be interpreted as "the father of ''x''". In [[arithmetic]], it may stand for "-x". In set theory, it may stand for "the [[power set]] of x".
** In arithmetic, ''g''(''x'',''y'') may stand for "''x''+''y''". In set theory, it may stand for "the union of ''x'' and ''y''".
** Function symbols of valence 0 are called ''constant symbols'', and are often denoted by lowercase letters at the beginning of the alphabet such as ''a'', ''b'' and ''c''. The symbol ''a'' may stand for Socrates. In arithmetic, it may stand for 0. In set theory, it may stand for the [[empty set]].

The traditional approach can be recovered in the modern approach, by simply specifying the "custom" signature to consist of the traditional sequences of non-logical symbols.