Elementary language
An elementary language (also: language of the first level with the set of symbols S) is a formal language defined within the framework of the first level predicate logic . With these languages, mathematical theories can be treated logically; so z. As the set theory etc. Experience shows even be that all mathematical statements in an appropriate firstorder language formalize leave, and that all provable statements within a firstorder language using the sequent calculus can be derived.
The alphabet of a first level language
definition
The alphabet of a firstlevel language includes the following characters:
 Symbols for variables ;
 Junctions : not, and, or, if  so, exactly if;
 Quantifiers : for all, there are;
 Equal sign;
 technical symbols: brackets;
 such as
 a) for each possibly empty one () amount of ary relation symbols , all together: ;
 b) for each possibly empty one () amount of ary function symbols , all together: ;
 c) a (possibly empty) set of symbols for constants (see note below on 0digit functions).
The set of characters under points 1 to 5 are the logical characters ; they are the same for all firstorder languages; they are denoted by A.
The amount of characters in item 6 is called set of symbols (including signature ) ; it determines the special language of the first level.
Hints
 In the alphabet (mathematics) the constants from (f) (3) are not listed if the definition is otherwise identical; for this, zerodigit relations and functions are allowed in (f) (1) ( ), the latter correspond to the constants from the above definition (see also zero digit links ).
 The singledigit relations define groups as they correspond to sets or general classes .
Example: group theory
To formalize the concept of the group and the defining axioms, one proceeds as follows:
 The variables stand for elements of the group; there is also a constant .
 A symbol is introduced; this stands for the twodigit link between two elements.
 Associative law:
 Neutral element:
 Inverse elements:
In this case there is a twodigit function symbol and a single constant .
Further examples
Relation symbols  Function symbols  Constants  Surname 

(binary)  (both two digits)  0, 1  Orderly bodies 
(binary)  e  groups  
+, (both twodigit)  0, 1  Rings  
(binary)  Equivalence relation 
Terms
The terms of an elementary language are defined recursively . A term in elementary language is obtained by finitely many applications of the following rules
 Variable symbols are terms.
 Constant symbols are terms.
 If there are a digit function symbol and terms, then there is also a term.
Set of symbols S  Example for terms from 

,  
 Remarks
 There are also notation without brackets, such as the Polish notation ; but these are usually not that easy to read. The third definition line above is in this notation (compare: firstorder predicate logic §Term ):
 o If is an n place function symbol and are terms, then is also a term.
 Occasionally the constants are subsumed as zerodigit functions, which is particularly evident in the bracketfree notation.
Formulas
→ See also: Logical formulas ; Term §expressions ; First order predicate logic § Expressions .
The formulas of language are obtained by a finite number of applications of the following rules:
Atomic formulas
 If and are terms, then is a formula.
 If there are a digit relation symbol and terms, then is a formula.
Propositional links
 If there is a formula, then too .
 If and are formulas, then too
Quantifiers
If is a formula and any variable symbol, then are too
 and
Formulas.
The elementary language for the set of symbols (signature) now consists of all formulas formed according to the above rules.
Connection with Chomsky hierarchy
 The rules for terms correspond to a contextfree language .
 The rules for formulas also correspond to a contextfree language : Elementary languages are therefore contextfree languages and thus a special class of formal languages .
 The rules for evidence correspond to a contextsensitive language . A contextsensitive analysis can decide whether there is a given proof for a formula.
 The rules for deriving a formula from a system of axioms correspond to a semidecidable language . In general there is no algorithm for obtaining a proof that derives a formula from another set of propositions.
swell
 HD Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic. BIWiss. Verlag, Mannheim / Leipzig / Vienna / Zurich 1992, ISBN 3411156031 .
 HansPeter Tuschik, Helmut Wolter: Mathematical logic  in short. Basics, model theory, decidability, set theory. BIWiss. Verlag, Mannheim / Leipzig / Vienna / Zurich 1994, ISBN 3411167319 .
Individual evidence
 ↑ Ebbinghaus u. a., Chapter VII §2: Mathematics as part of the first level.

↑ Occasionally zerodigit relations are allowed, these then appear as logical constants (in principle, identifiers for true or false ).
Stefan Brass: Mathematical Logic with Database Applications . Martin Luther University HalleWittenberg, Institute for Computer Science, Halle 2005, p. 176 , here p. 19 ( informatik.unihalle.de [PDF]).