Second order predicate logic

The second-order logic is a branch of the mathematical logic . It extends the first-order logic to the possibility of all relations to quantify . The second level predicate logic is therefore genuinely more expressive than that of the first level, but certain important sentences no longer apply, such as the compactness theorem .

The language of second order predicate logic

This article uses the terms and designations introduced in the first-order predicate logic article .

Symbols

The symbols of the second level predicate logic contain besides those of the first level

• logical symbols:
  • Quantifiers :  , ${\displaystyle \forall ,\exists }$
  • Connectives :  , ${\displaystyle \land ,\lor ,\rightarrow ,\leftrightarrow ,\neg }$
  • Technical characters:  , ${\displaystyle (,),\equiv }$
• Variable symbols : , , , ..., ${\displaystyle v_{0}}$ ${\displaystyle v_{1}}$ ${\displaystyle v_{2}}$
• a (possibly empty) set of constant symbols, ${\displaystyle {\mathcal {C}}}$
• a (possibly empty) set of function symbols, ${\displaystyle {\mathcal {F}}}$
• a (possibly empty) set of relation symbols ${\displaystyle {\mathcal {R}}}$

in addition

• Relations variable symbols , , , ... ${\displaystyle V_{0}}$ ${\displaystyle V_{1}}$ ${\displaystyle V_{2}}$

the arity of which is noted as the upper index if necessary. You step next to the variable symbols . Even if the intended application, namely the quantification of all relations, is already in the name, we want to refrain from it at this point, as in the first-order predicate logic, and initially see the symbols and the following laws of formation purely syntactically . The constant, function and relation symbols , and are again combined into a set , which is then called the signature of the language. Note that the relation symbols belong to the signature, the relation variable symbols, however, do not. ${\displaystyle v_{0},v_{1},v_{2},\ldots }$ ${\displaystyle {\mathcal {C}}}$ ${\displaystyle {\mathcal {F}}}$ ${\displaystyle {\mathcal {R}}}$ ${\displaystyle S}$

Terms and expressions

As in first-order predicate logic, terms, more precisely - terms, are explained by the formation laws specified there. With this, expressions were defined by means of further education laws. We add two more rules to this: ${\displaystyle S}$ ${\displaystyle S}$

• If an n-place relational variable symbol and are terms, then is an -expression. ${\displaystyle X}$ ${\displaystyle t_{1},\ldots ,t_{n}}$ ${\displaystyle Xt_{1}\ldots t_{n}}$ ${\displaystyle S}$
• Are a -expression and a relational variables symbol, are and also expressions. ${\displaystyle \varphi }$ ${\displaystyle S}$ ${\displaystyle X}$ ${\displaystyle \exists X\varphi }$ ${\displaystyle \forall X\varphi }$ ${\displaystyle S}$

2nd stage

All expressions that can be created according to the rules given above form the language marked with , where the Roman stands for the second level. This expresses that here one can not only quantify over all variables, but also over all relation variables in accordance with the second law of formation given above. With this we can form more expressions than in the first-level predicate logic, while, for example, the Peano axioms cannot be formulated in the first-level predicate logic, we will see below that the second level has sufficient expressiveness. ${\displaystyle S}$ ${\displaystyle L_{II}^{S}}$ ${\displaystyle II}$

Metalinguistic expressions

In the following we will use metalinguistic expressions for formulas from , i. H. spellings are used in the formulas that are not covered by the rules given above. Instead of using small letters like and instead of capital letters like and make sure that there are no conflicts with the elements of the signature. We also allow ourselves suggestive abbreviations such as for . The only reason for this is to make the formulas that appear easier to read; in any case it is clear which syntactically correct expression is meant by such a formula. ${\displaystyle L_{II}^{S}}$ ${\displaystyle v_{0},v_{1},\ldots }$ ${\displaystyle x,y,z}$ ${\displaystyle V_{0},V_{1},\ldots }$ ${\displaystyle X,Y,Z}$ ${\displaystyle \forall xyz}$ ${\displaystyle \forall x\forall y\forall z}$

semantics

Structures and interpretations

Based on a language , the symbols introduced above are now assigned a meaning. As in the first level predicate logic, structures are defined above the signature in order to then assign constants, functions, and relations of the object world to the symbols. An interpretation is a pair consisting of a structure over a set and a so-called occupancy function which assigns an element to each variable and a relation of equal arity to each relation variable . If such an assignment is a variable and , then it is precisely that assignment which, with the exception of , agrees in all places and only has the possibly different value at that point . Is analogously a relation variable of arity and an n -place relation on , i. H. , then the assignment which, with the exception of , corresponds to at all points , only has the possibly different value at that point . Note that the variable symbol and the relation as an object must have the same arity if the relation symbols are tied to fixed arenas. If, alternatively, a common pool of relation symbols is provided for all arity and the symbols used are assigned an arity by declaration (a partial mapping) , this restriction can be omitted. The assignment variant is then associated with a declaration variant (which is also called a local declaration ), whereby the following must then apply: The relation symbol is locally redeclared to the possibly different arity. One writes and . ${\displaystyle L_{II}^{S}}$ ${\displaystyle S}$ ${\displaystyle ({\mathcal {A}},\beta )}$ ${\displaystyle S}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle A}$ ${\displaystyle \beta }$ ${\displaystyle v_{i}}$ ${\displaystyle A}$ ${\displaystyle V_{i}}$ ${\displaystyle A}$ ${\displaystyle \beta }$ ${\displaystyle x}$ ${\displaystyle a\in A}$ ${\displaystyle \beta '=\beta {\frac {a}{x}}}$ ${\displaystyle x}$ ${\displaystyle \beta }$ ${\displaystyle x}$ ${\displaystyle a}$ ${\displaystyle X}$ ${\displaystyle n}$ ${\displaystyle B}$ ${\displaystyle A}$ ${\displaystyle R\subseteq A^{n}}$ ${\displaystyle \beta {\frac {B}{X}}}$ ${\displaystyle X}$ ${\displaystyle \beta }$ ${\displaystyle X}$ ${\displaystyle B}$ ${\displaystyle X}$ ${\displaystyle R}$ ${\displaystyle n}$
${\displaystyle {\mathrel {Rel}}}$ ${\displaystyle \nu :{\mathrel {Rel}}\not \to \mathbb {N} _{0}}$ ${\displaystyle \beta {\frac {R}{X}}}$ ${\displaystyle \nu {\frac {n}{X}}}$ ${\displaystyle R\subseteq A^{n}}$ ${\displaystyle X}$ ${\displaystyle n}$
${\displaystyle {\mathcal {I}}{\frac {a}{x}}:=({\mathcal {A}},\beta {\frac {a}{x}})}$ ${\displaystyle {\mathcal {I}}{\frac {B}{X}}:=({\mathcal {A}},\beta {\frac {B}{X}})}$

Models

An interpretation is called a model for an expression , written if this results from the following rules, whereby the regular structure of the language is used: ${\displaystyle {\mathcal {I}}=({\mathcal {A}},\beta )}$ ${\displaystyle \varphi }$ ${\displaystyle {\mathcal {I}}\vDash \varphi }$ ${\displaystyle L_{II}^{S}}$

${\displaystyle {\begin{matrix}{\mathcal {I}}\vDash t_{1}\equiv t_{2}&:\Leftrightarrow &{\mathcal {I}}(t_{1})={\mathcal {I}}(t_{2})\\{\mathcal {I}}\vDash Xt_{1}\ldots t_{n}&:\Leftrightarrow &\beta (X){\text{ trifft auf }}({\mathcal {I}}(t_{1}),\ldots ,{\mathcal {I}}(t_{n})){\text{ zu.}}\\{\mathcal {I}}\vDash Rt_{1}\ldots t_{n}&:\Leftrightarrow &R^{\mathcal {A}}{\text{ trifft auf }}({\mathcal {I}}(t_{1}),\ldots ,{\mathcal {I}}(t_{n})){\text{ zu.}}\\{\mathcal {I}}\vDash \neg \varphi &:\Leftrightarrow &{\text{nicht }}{\mathcal {I}}\vDash \varphi \\{\mathcal {I}}\vDash (\varphi \land \psi )&:\Leftrightarrow &{\mathcal {I}}\vDash \varphi {\text{ und }}{\mathcal {I}}\vDash \psi \\{\mathcal {I}}\vDash (\varphi \lor \psi )&:\Leftrightarrow &{\mathcal {I}}\vDash \varphi {\text{ oder }}{\mathcal {I}}\vDash \psi \\{\mathcal {I}}\vDash (\varphi \rightarrow \psi )&:\Leftrightarrow &{\text{wenn }}{\mathcal {I}}\vDash \varphi {\text{ dann auch }}{\mathcal {I}}\vDash \psi \\{\mathcal {I}}\vDash (\varphi \leftrightarrow \psi )&:\Leftrightarrow &{\mathcal {I}}\vDash \varphi {\text{ genau dann, wenn }}{\mathcal {I}}\vDash \psi \\{\mathcal {I}}\vDash \forall x\varphi &:\Leftrightarrow &{\mathcal {I}}{\frac {a}{x}}\vDash \varphi {\mbox{ für alle }}a\in A\\{\mathcal {I}}\vDash \exists x\varphi &:\Leftrightarrow &{\text{es gibt ein }}a\in A{\text{ mit }}{\mathcal {I}}{\frac {a}{x}}\vDash \varphi \\{\mathcal {I}}\vDash \forall X\varphi &:\Leftrightarrow &{\text{für alle Relationen }}B{\text{ auf }}A{\text{ gilt }}{\mathcal {I}}{\frac {B}{X}}\vDash \varphi \\{\mathcal {I}}\vDash \exists X\varphi &:\Leftrightarrow &{\text{es gibt eine Relation }}B{\text{ auf }}A{\text{ mit }}{\mathcal {I}}{\frac {B}{X}}\vDash \varphi \end{matrix}}}$

In the last two lines, any fixed arity of the relation symbols and the relations is usually assumed: which is sometimes indicated by an index n of the type . ${\displaystyle n}$ ${\displaystyle X\in {\mathrel {Rel}}_{n},R\subseteq A^{n}}$ ${\displaystyle X_{n}}$

This gives the symbols a meaning in terms of content. If a set of expressions is of the language under consideration and is for everyone , we will write again in abbreviated form . If there is a set of sentences, that is , they do not contain any free variables, then one also says that a model is of, because in this case the model relationship does not depend on the specific assignment. ${\displaystyle \Phi }$ ${\displaystyle {\mathcal {I}}\vDash \varphi }$ ${\displaystyle \varphi \in \Phi }$ ${\displaystyle {\mathcal {I}}\vDash \Phi }$ ${\displaystyle \Phi }$ ${\displaystyle \varphi \in \Phi }$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle \Phi }$

Peano axioms

As is well known, the Peano axioms cannot be formulated in the first-order predicate logic, since the induction axiom makes a statement about all subsets of the basic set under consideration, but cannot be quantified for all subsets. Since subsets are nothing more than single-digit relations , the following expressions can be formed with the signature , where 0 is a constant symbol, called a zero element, and a single-digit function symbol, called a successor function: ${\displaystyle S=\{0,\sigma \}}$ ${\displaystyle \sigma }$

• ${\displaystyle \forall x\,\neg \sigma x\equiv 0}$
• ${\displaystyle \forall x\forall y\,(\sigma x\equiv \sigma y\rightarrow x\equiv y)}$
• ${\displaystyle \forall X((X0\land \forall x(Xx\rightarrow X\sigma x))\rightarrow \forall x\,Xx)}$

If we consider interpretations, i.e. structures in which the symbol 0 is then an element of a set and a function defined on this, the first expression says that 0 is not a successor, because 0 is different from all images . The second line expresses the injectivity of the successor function. Finally, the third line says that every single-digit relation (that is, a subset of the considered basic range) that applies to 0 and every one to which it applies also applies to the successor, applies to all variables , thus formulating the induction axiom. The second level predicate logic is thus genuinely more expressive than that of the first level. ${\displaystyle S}$ ${\displaystyle \sigma }$ ${\displaystyle \sigma x}$ ${\displaystyle X}$ ${\displaystyle x}$ ${\displaystyle \sigma x}$ ${\displaystyle x}$

Finally, one can show that every two structures that are models of the above expressions are isomorphic. So in second order predicate logic there are no non-standard models of the natural numbers. ${\displaystyle S}$ ${\displaystyle L_{II}^{S}}$

Real numbers

The theory of ordered bodies , which can be formulated in language with the signature , does not allow any unambiguous identification of the real numbers except for isomorphism, because the axiom of completeness , according to which every non-empty, upwardly restricted set has a supremum , can be in not formulate. This lack of expressiveness in first order predicate logic leads to nonstandard analysis . In the second level predicate logic dealt with here, the following symbolization of completeness succeeds: ${\displaystyle S=\{0,1,+,\cdot ,<\}}$ ${\displaystyle L_{I}^{S}}$ ${\displaystyle L_{I}^{S}}$

${\displaystyle \forall X:((\exists x\,Xx\land \exists y\forall z(Xz\rightarrow z<y))\rightarrow }$  ${\displaystyle \exists y(\forall z(Xz\rightarrow (z<y\lor z\equiv y))\land \forall x(x<y\rightarrow \exists z\,(x<z\land Xz))))}$

To explain this formula, note that the one-digit relation again stands for subsets of the population of an interpretation. For all subsets so shall apply: If it is not empty, and if it is bounded above, then there is one so that this upper bound on the amount, and each smaller element is not upper bound . With that the completeness axiom is formulated in. ${\displaystyle X}$ ${\displaystyle \exists x\,Xx}$ ${\displaystyle \exists y\forall z(Xz\rightarrow z<y)}$ ${\displaystyle y}$ ${\displaystyle \forall z(Xz\rightarrow (z<y\lor z\equiv y))}$ ${\displaystyle \forall x(x<y\rightarrow \exists z\,(x<z\land Xz))}$ ${\displaystyle L_{II}^{S}}$

Powers

The second level predicate logic offers possibilities to talk about the cardinalities of sets that go far beyond the first level predicate logic. In the following we use the abbreviation

${\displaystyle \exists ^{1}x\,\varphi }$ For ${\displaystyle \exists x\,(\varphi \,\land \,\forall y\,(\varphi {\frac {y}{x}}\rightarrow y\equiv x)),}$

which in every interpretation obviously means that there is exactly one with . ${\displaystyle x}$ ${\displaystyle \varphi }$

Finite quantities

It is well known that in first order predicate logic one cannot express that a set is finite . One can only use sentences of Art

${\displaystyle \varphi _{\geq n}=\exists v_{1}\ldots \exists v_{n}\,(\neg v_{1}\equiv v_{2}\land \neg v_{1}\equiv v_{3}\land \ldots \land \neg v_{n-1}\equiv v_{n})}$

say that a set (i.e. the base area of ​​an interpretation) has at least elements. then only applies to sets with exactly elements. The finiteness of a set would then be an infinite disjunction ${\displaystyle n}$ ${\displaystyle \varphi _{\geq n}\land \neg \varphi _{\geq n+1}}$ ${\displaystyle n}$

${\displaystyle \neg \varphi _{\geq 1}\lor \neg \varphi _{\geq 2}\lor \neg \varphi _{\geq 3}\lor \ldots ,}$

which can be formed neither in the first nor in the second stage. In the second level predicate logic, however, one has

${\displaystyle \varphi _{endl}=\forall X\,((\forall x\,\exists ^{1}y\,Xxy\,\land \,\forall xyz\,(Xxz\land Xyz\rightarrow x\equiv y))\rightarrow \forall y\,\exists x\,Xxy)}$.

In every model of this theorem, means that the two-digit relation is a function of the fundamental domain in itself, says that it is injective and that it is surjective. The above formula says that every injective function of the basic domain is automatically surjective in itself, a statement that, as is well known, exactly applies to finite sets. Hence, the formula actually means that all models that satisfy it are finite. This again shows that the second level predicate logic is genuinely more expressive than the first level. ${\displaystyle \forall x\,\exists ^{1}y\,Xxy}$ ${\displaystyle X}$ ${\displaystyle \forall xyz\,(Xxz\land Xyz\rightarrow x\equiv y)}$ ${\displaystyle \forall y\,\exists x\,Xxy}$ ${\displaystyle \varphi _{endl}}$

Countable sets

In second-order predicate logic one can even express that a set is at most countable , because a set is at most countable if and only if there is a linear order relation on it in which every initial section is finite. That there is a linear order is evident from ${\displaystyle X}$

${\displaystyle \varphi _{ord}=\forall x\,\neg Xxx\land \forall xyz\,((Xxy\land Xyz)\rightarrow Xxz)\land \forall xy\,(Xxy\lor x\equiv y\lor Xyx)}$

because this formula means from left to right that the two-digit relation is irreflexive, transitive and linear. A one-digit relation that stands for a subset of the basic area is finite if and only if every injective function of this subset is already surjective in itself, which can be symbolized in analogy to the above as follows: ${\displaystyle Y}$ ${\displaystyle \varphi _{endl}}$

${\displaystyle \psi _{endl}=\forall X\,(\forall xy\,(Xxy\rightarrow Yx\land Yy)\land \forall x\,(Yx\rightarrow \exists ^{1}y\,Xxy\land \forall xyz\,(Xxz\land Xyz\rightarrow x\equiv y))\rightarrow }$  ${\displaystyle \forall y\,(Yy\rightarrow \exists x\,Xxy))}$.

The following formula then symbolizes that there is a linear order on a set in which every initial section is finite, and this is equivalent to the fact that the set is at most countable:

${\displaystyle \varphi _{\leq abz}=\exists X\,(\varphi _{ord}\land (\forall Y(\exists x\,(Yy\leftrightarrow Xyx)\rightarrow \psi _{endl})))}$

Deficiencies in second order predicate logic

As the following discussion shows, the greater expressiveness of the second-order predicate logic means that many important sentences of the first-order predicate logic no longer apply.

Invalidity of compactness theorem

With the formulas and introduced above, it can easily be shown that no compactness theorem can apply to the second level predicate logic . Obviously every finite subset of the formula set is ${\displaystyle \varphi _{\geq n}}$ ${\displaystyle \varphi _{endl}}$

${\displaystyle \{\varphi _{endl}\}\cup \{\varphi _{\geq n}|\,n\in \mathbb {N} \}}$

satisfiable, that is, it has a model, because a finite subset of this formula set is suitable for in ${\displaystyle m\in \mathbb {N} }$

${\displaystyle \{\varphi _{endl}\}\cup \{\varphi _{\geq n}|\,n\leq m\}}$

which is why every finite set with at least elements is a model. On the other hand, there is no model for the entire set of formulas, because a model of must be a finite set and therefore cannot satisfy all of them . ${\displaystyle m}$ ${\displaystyle \varphi _{endl}}$ ${\displaystyle \varphi _{\geq n}}$

But since the compactness theorem applies to the first-level predicate logic, this consideration shows once again that it cannot be formulated in the first-level predicate logic. ${\displaystyle \varphi _{endl}}$

Invalidity of the Löwenheim-Skolem theorem

In the cardinality section, we created a formula whose models are precisely the most countable sets. If the Löwenheim-Skolem theorem were also valid for the second order predicate logic, there would have to be a countable model for the formula set , but this cannot be, because every model of is necessarily uncountable . ${\displaystyle L_{II}^{\emptyset }}$ ${\displaystyle \varphi _{\leq abz}}$ ${\displaystyle \{\neg \varphi _{\leq abz}\}}$ ${\displaystyle \neg \varphi _{\leq abz}}$

Second level predicate logic incompleteness

In the first-level predicate logic one can set up a sequential calculus and prove from this that it is sufficient for all derivations in a language of the first-level predicate logic, this is the so-called Gödel completeness theorem . One could now try to expand such a sequence calculus by elements that define the handling of relational variable symbols in order to be able to carry out all derivations in a purely syntactic way in such a calculus for the second level predicate logic. Such an attempt must fail, because with a complete sequential calculus for the second-order predicate logic one could transfer the proof that in the first-order predicate logic inferred from this to the compactness theorem to the second-order predicate logic, but we already know that the compactness theorem here does not apply.

If one denotes the inference in such a sequence calculus with , it means that the expression can be derived from the set of formulas by applying the rules of the sequence calculus . As above, the notation means that every model that fulfills must also fulfill. The consideration just given shows that there is no such thing as a sequence calculus, so that for all formula sets and expressions the equivalence ${\displaystyle K}$ ${\displaystyle \vdash _{K}}$ ${\displaystyle \Phi \vdash _{K}\varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \Phi }$ ${\displaystyle \Phi \vDash \varphi }$ ${\displaystyle \Phi }$ ${\displaystyle \varphi }$ ${\displaystyle K}$ ${\displaystyle \Phi }$ ${\displaystyle \varphi }$

${\displaystyle \Phi \vDash \varphi }$ exactly when ${\displaystyle \Phi \vdash _{K}\varphi }$

applies. That does not rule out that there could be a sequence calculus that fulfills this equivalence for , then one would at least have a sequence calculus for general statements, but that is also not the case, as Kurt Gödel was able to show. This statement is called the incompleteness of the second order predicate logic . It should be noted that this is not Gödel's incompleteness theorem . ${\displaystyle \Phi =\emptyset }$

Fragments of second order predicate logic

For applications, certain restrictions of the expressions of the second level predicate logic are considered; one speaks of fragments of the second level predicate logic and one is interested in their expressiveness.

∃SO and ∀SO

In existential predicate logic of the second level , one restricts oneself to expressions of the form

${\displaystyle \exists X_{1}\ldots \exists X_{n}\varphi }$,

where an expression of the first-level predicate logic is in a signature extended by. In particular, no universal quantifiers are allowed over relation symbols. Because of the English term existential second order logic , this fragment is referred to as ∃SO. The class of structures that can be defined by means of ∃SO expressions is closely linked to the languages ​​of the complexity class NP via Fagin's theorem , so that ∃SO can be identified with NP with suitable coding. ${\displaystyle \varphi }$ ${\displaystyle X_{1},\ldots ,X_{n}}$

Analogously, the universal second order predicate logic consists of expressions of the form

${\displaystyle \forall X_{1}\ldots \forall X_{n}\varphi }$,

with an expression of first order predicate logic as above. This fragment is called SO. In complexity theory, ∀SO belongs to the complexity class coNP , because the ∀SO-expressions are exactly the negations of the ∃SO-expressions and vice versa. ${\displaystyle \varphi }$

More generally, fragments can be seen as a set of expressions of form ${\displaystyle \Sigma _{k}^{1}}$

${\displaystyle \underbrace {(\exists \ldots \exists )(\forall \ldots \forall )(\exists \ldots \exists )\ldots } _{k{\text{ Blöcke}}}\varphi }$

define and analogously as the set of negations of . So is and . The fragments and then describe the complexity classes of the polynomial hierarchy . ${\displaystyle \Pi _{k}^{1}}$ ${\displaystyle \Sigma _{k}^{1}}$ ${\displaystyle \exists SO=\Sigma _{1}^{1}}$ ${\displaystyle \forall SO=\Pi _{1}^{1}}$ ${\displaystyle \Sigma _{k}^{1}}$ ${\displaystyle \Pi _{k}^{1}}$

MSO

Another important fragment is obtained if one restricts the quantification via relations to single-digit relations, that is, in every interpretation to subsets of the universe. This is called the second order monadic predicate logic or, for short, after the English monadic second order logic , MSO. Here, too, one is interested in the expressiveness and also goes over to smaller fragments such as ∃MSO, which consists of expressions that lie in MSO and in ∃SO. This, too, can be expanded in an obvious way to create hierarchies marked with and . ${\displaystyle M\Sigma _{k}^{1}}$ ${\displaystyle M\Pi _{k}^{1}}$

See also

• Fagin's theorem
• Set of traditional bread
• Higher level predicate logic

literature

• H.-D. Ebbinghaus, J. Flum, W. Thomas: Finite Model Theory. Springer Verlag, 1995, ISBN 3-540-28787-6 .
• H.-D. Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic . Spectrum Academic Publishing House, 1996, ISBN 3-8274-0130-5 .
• Leonid Libkin: Elements of Finite Model Theory. Springer-Verlag, 2004, ISBN 3-540-21202-7 .
• Stefan Brass: Mathematical Logic with Database Applications . Martin Luther University Halle-Wittenberg, Institute for Computer Science, Halle 2005, p. 176 ( informatik.uni-halle.de [PDF]). Alternative notation for a locally modified variable declaration and assignment.
  
• Klaus Grue: Object Oriented Mathematics . University of Copenhagen, Department of Computer Science (Datalogisk Institute), 1995, p. 21 ( diku.dk [PDF]). General maplet notation, also a notation for locally modified variable declaration and assignment.
  
• Carsten Lutz: Logic Part 4: Second level predicate logic . University of Bremen, AG Theory of Artificial Intelligence, 2010, p. 65 ( informatik.uni-bremen.de [PDF] lecture in the winter semester 2010).
• François Bry: 2.10 Excursus: Second order predicate logic . LMU, Institute for Computer Science, teaching and research unit for programming and modeling languages, Munich 1999 ( en.pms.ifi.lmu.de ).
• Esther Ramharter, Günther Eder: Second level predicate logic. SE modal logic and other philosophically relevant logics . WS 2015/2016. University of Vienna, S. 22 ( homepage.univie.ac.at [PDF]).

Notes and individual references

1. ↑ Ramharter, Eder (2015/16) also allow function variables. B. be designated with. Relation variables of arity 0 represent statement variables; Function variables of arity 0 correspond to ordinary variables. ${\displaystyle \chi _{0},\chi _{1},\chi _{2},\dots }$
2. ↑ If function variables are allowed (Ramharter, Eder 2015/16), then the following is added to the formation laws for terms:
   • If an n-place function variable symbol and are terms, then is a -term. ${\displaystyle \chi }$ ${\displaystyle t_{1},\ldots ,t_{n}}$ ${\displaystyle \chi t_{1}\ldots t_{n}}$ ${\displaystyle S}$
3. ↑ For this purpose, a separate set of n -place relational variable symbols is usually provided for each arity . Examples of this can be found in F. Bry (1999) Def. 2.10.1, C. Lutz (2010) p. 6 and 8, and Ramharter, Eder (2015/16) p. 17 (the latter denote the fixed arity of relational variables with an index). Another possibility is to work with a single set of relational symbols (as in the first level logic) and to assign arity to the relational variable symbols used via a (partial) mapping ( variable declaration ). ${\displaystyle n\in \mathbb {N} _{0}}$ ${\displaystyle {\mathrel {Rel}}_{n}}$
   ${\displaystyle {\mathrel {Rel}}}$ ${\displaystyle \nu :{\mathrel {Rel}}\not \to \mathbb {N} _{0}}$
4. ↑ With any (set of variable symbols), (value range), the locally modified variable assignment (also called ( -) variant ) is a (possibly only partial) mapping from to with ${\displaystyle x\in {\mathcal {V}}}$ ${\displaystyle a\in A}$ ${\displaystyle x}$ ${\displaystyle \beta '=\beta {\frac {a}{x}}}$ ${\displaystyle {\mathcal {V}}}$ ${\displaystyle A}$

   ${\displaystyle \beta '(y)=\beta {\frac {a}{x}}:={\begin{cases}a&{\text{wenn}}\ y=x,\\\beta (y)&{\text{sonst (auf dem ursprünglichen Definitionsbereich von}}\ \beta {\text{)}};\end{cases}}}$

   Alternative spellings for are ${\displaystyle \beta {\frac {a}{x}}}$
   • ${\displaystyle \beta [{x/a}]}$ - Carsten Lutz (2010) p. 8,
   • ${\displaystyle \beta \langle {x/a}\rangle }$ - Stefan Brass (2005) p. 56, given there for a variable declaration instead of -assignment and
   • ${\displaystyle \beta _{\langle x\mapsto a\rangle }}$(or ) - Klaus Grue (1995), p. 11, there given general maplet notation. ${\displaystyle \beta {\langle x\mapsto a\rangle }}$
   Ramharter, Eder (2015/16) p. 17 denote the variable assignment with instead . In the event that it already belongs to the domain of definition , the original image value is overwritten. ${\displaystyle s}$ ${\displaystyle \beta }$
   ${\displaystyle x}$ ${\displaystyle \beta }$
5. ↑ A corresponding procedure in the multi-varietal predicate logic of the first order (i.e. with varieties instead of arithmetic) can be found in S. Brass (2005) pp. 54–56.
6. ↑ When working alternatively with a single amount of relation symbols and a Stelligeitsdeklaration, the last two lines could be: It is for use in an area ( Mount Scopus , a local variant of the Stelligkeitsdeklaation) of quantifiers effective. In the multi-site case, the arity only needs to be expanded to include an argument type with the sorts , the sorts being symbols for the object areas - for single- sorts logic see Brass (2005). ${\displaystyle {\begin{matrix}{\mathcal {I}}\vDash \forall X:n\ \varphi :\Leftrightarrow {\text{für alle Relationen }}B\subseteq A^{n}{\text{ auf }}A{\text{ gilt }}{\mathcal {I}}{\frac {B}{X}}\vDash \varphi \\{\mathcal {I}}\vDash \exists X:n\ \varphi :\Leftrightarrow {\text{es gibt eine Relation }}B\subseteq A^{n}{\text{ auf }}A{\text{ mit }}{\mathcal {I}}{\frac {B}{X}}\vDash \varphi \end{matrix}}}$ ${\displaystyle X}$ ${\displaystyle \nu '=\nu {\frac {n}{X}}}$ ${\displaystyle n}$ ${\displaystyle t=(t_{1},\dots t_{n})}$ ${\displaystyle t_{1},\dots t_{n}\in T}$ ${\displaystyle s\in T}$ ${\displaystyle A_{s}}$
7. ^ Leonid Libkin (2004), p. 173
8. ↑ H.-D. Ebbinghaus, J. Flum, W. Thomas (1995), p. 40.