A first-order language specifies its constant, operation, and relation symbols, together with the arity of each nonconstant symbol.
A signature specifies the sorts, operation symbols with their input and output sorts, and relation symbols with their input sorts. The logical connectives and quantifiers are supplied separately by the chosen logic. This separates the nonlogical vocabulary from the rules defining a coherent theory.
For coding arithmetic computations, the signature in use is . Bounded remainder tests and polynomial equations use only these symbols. This is a statement about the language: interpretation in the natural numbers does not impose the axioms of a ring.
A first-order term is built recursively from variables and constant symbols by applying function symbols to existing terms. Evaluation in a first-order structure follows the same recursion. An atomic formula applies a relation to terms, or asserts their logical equality.
A finite set of formulas mentions only finitely many nonlogical symbols. This observation lets compactness reduce arguments in a language indexed by a large set to a finite sublanguage.
Articles by others on the same topic
There are currently no matching articles.