First-order logic

The first-order predicate logic is a branch of mathematical logic. It deals with the structure of certain math expressions and the logical closing, with the leads of such expressions to others. It is possible to define both the language and the Close purely syntactic, ie without reference to mathematical meanings. The thus gained interplay of purely syntactic considerations on the one hand and semantic considerations on the other hand leads to important insights that have meaning for all of mathematics, because these can be formulated by means of the Zermelo -Fraenkel set theory in the first order predicate logic.

  • 3.1 structures
  • 3.2 interpretations
  • 3.3 models
  • 3.4 equality
  • 4.1 Conclusions
  • 4.2 sequent calculus
  • 4.3 Completeness and correctness
  • 5.1 Erfüllbarkeitssatz
  • 5.2 compactness theorem
  • 5.3 isomorphisms
  • 5.4 Löwenheim - Skolem theorem
  • 5.5 set of Lindström

A motivating example

The below definitions drawn up should be motivated by the example of the theory of ordered abelian groups. An ordered abelian group initially consists of an abelian group, that is, one has the following properties

  • Associative law: For all true:.
  • Commutative: For all true:.
  • Neutral Element 0: For all true:.
  • Inverse element: For all there is, so that:.

In short math notation can be also referred to as

Play. We write instead of the often used, since we here already intend to say about nothing more than the elements of the group. Furthermore, we have a relation for order on the group, which must satisfy the following axioms, which are given here in the same shorthand notation:

  • Reflexivity:
  • Transitivity:
  • Group compatibility:

Examples of ordered abelian groups are about or that can not be isomorphic already made ​​cardinality reasons.

Overall, we have some of the so-called logical symbols used brackets as auxiliary symbols, and also the equal sign and variables for the elements. The characteristic of the theory of ordered abelian groups symbols are the constant 0, the functions and - as well as the relation which the customary in mathematics spellings were used, ie instead or take. The two functions have different arity, 2 digits, the inverse form - is 1 digit, the contemplated order relation is 2 digits. Thus, the symbols of a particular language are described, in which one can formulate the theory of ordered abelian groups. Some of the strings formed from the symbols are "reasonable", ie formed according to certain laws, and some of these press beyond " true statements " from. This is generalized in the following, in particular the difference between the formed according to rules "reasonable" strings and a possible " truth " of such strings is worked out and resulting consequences. These have implications for the whole of mathematics.

The language of first-order predicate logic

We describe here the language used in a purely syntactic way, that is, we place the considered strings, which we will call expressions of the language, determined without reference to their meaning.

Symbols

A first-order language is made ​​up of the following symbols:

  • So-called variable symbols,
  • A (possibly empty ) set of constant symbols,
  • A (possibly empty ) set of function symbols,
  • A (possibly empty ) set of relation symbols.

The comma is used here only as a separator for the list of symbols, it is not a symbol of the language.

Terme

The constructed according to the following rules strings hot Terme:

  • If a variable symbol, then a Term
  • Is a constant symbol, it is a Term
  • Is a 1- ary function symbol and is a term, then a Term
  • If a 2 - ary function symbol and are terms, so is a Term
  • Is a 3 - ary function symbol and are terms, so is a Term
  • And so on for 4,5,6, ... - ary function symbols.

For example, if a constant and and 1 - or 2- ary function symbols, so is a term because it can be created by use of the above rules: is a term, hence; and are terms, therefore, and thus eventually also.

We do not here on brackets and commas as delimiters, that is, we write and not. We rely so implicitly assume that our symbols are such that a unique legibility is ensured.

The rules for function symbols are often summarizes thus:

  • Is an n- ary function symbol and are terms, so is a Term

This means nothing else than the above indicated infinite sequence of rules, as the three points are not part of the agreed symbols. Nevertheless, it is sometimes made ​​use of this notation.

About the structure of terms, further properties can be defined. How we define clearly by the following three rules recursively which variables occur in a term:

  • If a variable symbol, it should be.
  • Is a constant symbol, it should be.
  • Is an n- ary function symbol and are terms, it should be.

Expressions

We now explain through education laws which strings we want to see as expressions of the language.

Atomic expressions

  • Are terms and, as an expression.
  • 1 is a binary relation symbol and is a term that is an expression.
  • If a 2 - ary relation symbol and are terms, so is an expression.
  • And so on for 3,4,5, ... - digit relation symbols.

The remarks made ​​above on the spelling in terms apply.

Compound expressions

We describe here how to win more from expressions.

  • Is an expression, it is also an expression.
  • Are and expressions, so are, , and expressions.
  • Is an expression and is a variable, so are and expressions.

This means that all expressions of our language are defined. For example, if a 1- ary function symbol and a 2- ary relation symbol, then

An expression, because it can be constructed by use of the above rules. It should again be noted that we create expressions using the above rules purely mechanical, without the expressions would necessarily denote anything.

1st stage

Different languages ​​of first order differ only in the amounts, and which is called usually summarizes the set of symbols and the signature of the language. It also talks specifically from -terms or expressions. The language, that is the set of all expressions formed according to the above rules is denoted by, or. In the latter case is the Roman for 1 -th stage. This refers to the fact that can be quantified according to the last generation rule only variable. does not intend to quantify over all subsets of a set or of all functions. Thus the usual Peano axioms can not be expressed in as the induction axiom makes a statement about all subsets of natural numbers. This can be viewed as a weakness of this language, however, the axioms of Zermelo -Fraenkel set theory are all in the first stage with the single symbol formulated, so that the first stage is sufficient in principle for mathematics.

Free variables

Other properties of expressions of the language can also be defined purely syntactically. According to the above structure by formation rules, we define the set of variables occurring free in the expression as follows:

  • And the same for

Non - free variable called bound variable. Expressions without free variables, ie, those with are called sentences. All indicated in the above motivating example axioms of ordered abelian groups, with the appropriate translation into the language sets, such as for the commutative.

Metalinguistic expressions

The example given just as symbolizing the commutative in the language shows that the resulting expressions are often difficult to read. Therefore, the mathematician, and often the logician, returns like the classical notation. But the latter is not an expression of the language but only a notification of such an expression using other symbols of another language, here the so-called meta-language, that is, those language in which you talk about. For the sake of readability, you can also list continues superfluous parentheses. This does not cause problems as long as remains clear that one could re-translate the strings easier to read at any time.

Substitutions

In mathematics variables are often replaced by terms. This can also be here purely syntactic explain on the basis of our symbols. By following the rules, we specify what it should mean to use the term for a variable. We follow again the rule-based structure of terms and expressions. The substitution is as quoted, where the square brackets may be omitted.

For the establishment of terms is defined as follows:

  • If a variable symbol, is equal if and else
  • Is a constant symbol, then.
  • If an n- ary function symbol and expressions as is.

For expressions we write brackets around the expression, in which the substitution is to be made. We commit:

  • And the same for
  • ; analogously for the quantifier
  • And if; analogously for the quantifier
  • And optionally, wherein a variable is not occurring in or, for example, the first of the variable which satisfies this condition. The analogous definition is made for.

This definition has been taken to ensure that variables do not accidentally fall into the sphere of influence of a quantifier. If the bound variable occurs in the term, so it is replaced by another previously, so as to avoid the collision tags.

Semantics

We start from a language. The expressions formed in this language according to the above rules would be brought in connection with mathematical structures. In these structures, one can then examine the expressions on the veracity of what is specified in the following.

Structures

A structure over a signature is a non- empty set together with

  • One element for each constant symbol,
  • A function for each binary function symbol,
  • A relation for each digit relation symbol.

In the example given at the outset of ordered abelian groups is a structure. By structures so the symbols are made ​​associated with "real" constants, functions and relations.

Interpretations

An interpretation of a pair consisting of a structure, and an image.

It thus combines the idea that the structure is the mathematical object which is to be described with the language, while the variables assigned values ​​from the base set, which is why this figure also called occupancy. The assignment of an interpretation can be easily extended to terms, this expansion depends on the interpretation of the constant symbols and function symbols and is therefore also referred to as; one defines:

  • If a variable, it should be.
  • Is a constant symbol, it should be.
  • Is an n- ary function symbol and are terms, it should be.

If, for example, then such an interpretation. Then we have.

If we change a booking from only at the site and make this up down, we write for the assignment and as amended. Often, the assignment of the variables is clear or unimportant; then we call something unclean but practical, the structure an interpretation.

Models

We will say that an interpretation is and write for it, if this arises due to the following rules a model for a term:

This definition is based again on the rule-based structure of the expressions of the language. The dot notation in the second rule is here again for a list of rules for each arity a.

Through the concept of interpretation of the variables and the symbols from were provided with a meaning. The straight model defined relationship, the logical symbols are interpreted for the first time.

For a lot of expressions we write if for all, and say is a model of. Identifies about the above axioms of ordered abelian groups, as accurately applies if an ordered abelian group. The assignment seems to play no role, since there is only of sentences, ie contains no free variables. This is indeed the case, as the so-called Koinzidenzlemma says. In such a case, you can omit it and typing. This is then testified that for each assignment is a model of all expressions.

Equality

To use the equality is to be noted that we have introduced the symbol in the first order language. An expression of the form is not an expression of first-order language but the metalinguistic assertion of the equality of two expressions and. The latter can be in the first stage of language does not symbolize, there can only terms to be equal. Parallel to the construction considered here there is also the first-order predicate logic without equality, to removed the symbol and it formation rule in question. Although you can then bring into play the equality via a relation of again, these sets but then interpretations, so that you do not receive the same as a logic with equality. The logical equality, however, means in every interpretation of equality of individuals, and that is the reason why we consider logics with equality.

Mathematical Close

Conclusions

It should be a given set of expressions, for example, the above axioms of ordered abelian groups. The mathematician is interested in what conclusions can be drawn from them. We say that the expression follows from and write for it, if every model of is also a model of. This is the so-called semantic reasoning of, because it refers to all possible interpretations of the symbols.

Sequent calculus

In general, the mathematician does not semantically, but it applies certain rules of inference, with whom he starts to work on a statement to the next until the claim. Starting from a given sequence of expressions, he goes to new episodes to have "proven" end up with a result that follows. The "proof" is a finite list of such consequences. Here are some such inference rules are introduced, illuminated their content, background and then compared with the final semantic way. In is called the antecedent and the following expressions the Sukzedenz.

Prerequisite rule: is a lawful order when. This is based on the simple fact that one can use one of the requirements of any time.

Antezedenzregel: If you already have, so you can go on if. If you can that is close by, so you can do right under even stronger conditions the first.

Case distinction: If you and already has, so you can pass. One can, in the case of close up, and also in the case of. Therefore, it can be concluded in each case of at.

Contradiction. If you and already has, so you can pass. Taking namely in terms of a proof by contradiction, that it follows from the conditions as well as, for a total contradiction. Therefore, the assumption was wrong and you can connect to.

Or launch in the antecedent: If you and already has, so you can pass. Under the conditions resulting from both as well. Therefore, it is already apparent when or applies.

Or launch in Sukzedenz: If you already have, so you can pass. This is clear, since a fortiori applies to. Accordingly, one can also to go.

Equality: You can always write down the expression, where an arbitrary term. This rule needs no explanation.

The remaining three rules of inference using the above-defined substitution of variables by terms:

Substitution: If you already have, so you can pass. If one can be made on, that is, the replacement in place of, close, as also with the replacement in place of, if equal.

Existence launch in Antezendenz: If you already have, so you can pass. In order to work with the existence condition, you may use one, then for the. In evidence, the use of this rule, means then the existence condition: Be as a ...

Existence launch in Sukzendenz: If you already have, so you can pass. Also, this rule is obvious because if one has with an example found, then one can infer the existence statement and no longer mention the example here.

The rules presented here, which form the so-called sequent calculus are logically conclusive, as was pointed out as an addition to every rule entries. Mathematicians use some other inference rules, one of which can also be shown that they all can be derived from the above, that is, their application can be replaced by a finite chain of the above rules. If one is starting to come after a finite number of applications of these rules, so that is derived from logically conclusive, we write it.

In contrast to the above-explained semantic reasoning of the "evidence" purely syntactic nature, they can be viewed as manipulation of character strings of the considered language. To apply the final rules, one does not know what the symbols mean.

Completeness and correctness

If the interpretation of a model for a set of expressions of the language and is, as a model for, because with accompanying proof can be carried out directly in the model so without further notice. It applies the so-called correctness theorem that follows from always.

Conversely, it is quite conceivable that there is an expression amount of only a few models who happen to have a squeezable in the first order language property in common, without it this was a way to be able to deduce by the above syntactic string operations. That this is not the case, but that semantic and syntactic of inference are equivalent, known as Gödel's completeness theorem and a central result of the first-order predicate logic. One can show that, no can find the semantic reasoning of equivalent sequent calculus to a predicate logic second stage in which one allows quantification over relations.

Properties

Erfüllbarkeitssatz

A set of expressions of the language is called consistent if there is no expression of the form can be derived from. This consistency is a purely syntactic notion. We have the following Erfüllbarkeitssatz which can be derived from the set of Henkin and is closely related to the Gödel's completeness theorem:

  • There is a model for every consistent set.

Compactness theorem

  • Compactness theorem: If a set of expressions of the language and gives it to every finite subset of a model, it is also a model for.

If there were not a model for, it would be after the Erfüllbarkeitssatz not consistent, and there would be a derivation. As a proof but only has a finite length and hence only a finite number of terms can involve from, there must already be a finite subset give with. After the completeness theorem follows, that is to say it can not model for giving, in contradiction to the assumption.

The finiteness theorem is also called the compactness theorem: One chooses at any consistent set of sentences a model and summarize the models found in this way to a lot together. Is for a set. Then the sets form the basis of a topology and the finiteness theorem is equivalent to the compactness of this space.

Isomorphisms

From the finiteness theorem follows:

  • Is there a set of expressions of the language an infinite model, so there are models of arbitrarily large cardinality.

Indeed, if given, is a cardinal number, it should be a lot of not contained in constant symbols. Every finite subset of then has a model in the language, where the new constant symbols to the extended symbol set is. Because of the finite set, there is then a model, and having at least the thickness. With a little more precise argument you can even find a model of cardinality, if the thickness of less than or equal.

This shows a weakness of the first-order predicate logic. By means of the first stage of language can express quantities with infinite models never succeed in a characterization up to isomorphism, as the class of all models to such a consistent set of expressions always contains models of arbitrarily large cardinality, that is not isomorphic models. We call two models elementary equivalent if the quantities of expressions, for which they are models match. The first-level languages ​​can therefore characterize infinite structures or models only up to elementary equivalence.

Löwenheim - Skolem theorem

Also from the set of Henkin can be derived the Löwenheim - Skolem theorem:

  • Is there a most countable set of expressions of the language an infinite model, so there is a countable model.

In the introductory example is a countable model. In many mathematical theories can these be found very easily in the model theory but has the Löwenheim - Skolem theorem in-depth applications.

Set of Lindström

Because of the above-mentioned weaknesses of the first-level language you can search for appropriate extensions. If you find this way really more expressive languages, which would of course be specified yet, so show the sets of Lindström, that you then have to do without the finiteness theorem or the Löwenheim - Skolem. If one wishes to maintain both sets, the first-order predicate logic is thus "the best ", what you can achieve.

Metalanguage Interpretation (logic) Soundness Base (topology) Wolfgang Rautenberg 2008
86623
de