Logic

Logic

Mathematical logic

Mathematical logic is the study of logic in mathematics.

Propositional logic

Propositional logic deals with logical statements, which are directly decidable. For example the logical statement ${\textstyle 2<4}$ is ${\textstyle True}$.

${\textstyle \mathrm {\ \ \ \ } }$ Logical operators

The mathematical logical operators are listed as

• Negation
• Conjunction
• Disjunction
• Implication
• Double implication

The logical operators are also called as logical connectives.

Negation as logical operator has only one argument, i.e. it concerns only one statement. Negation of a statement is ${\textstyle True}$ if the statement is ${\textstyle False}$. Negation is also called as NOT operator and it is denoted in mathematical logic as ${\textstyle \neg }$. For example if ${\textstyle A}$ stands for a statement then ${\textstyle \neg A}$ is ${\textstyle True}$ whenever ${\textstyle A}$ is ${\textstyle False}$ and vice versa.

Th conjunction and disjunction as logical operators have two arguments. Conjunction is also known as AND operator and denoted by ${\textstyle \land }$. Disjunction is also known as OR operator and denoted by ${\textstyle \lor }$.

Implication as logical operator has two arguments. It is also known as conditional operator and it is denoted by ${\textstyle \implies }$. Implication (e.g. ${\textstyle A\implies B}$) is ${\textstyle True}$ if truth of first argument (${\textstyle A}$) implies truth of second argument (${\textstyle B}$) or the first argument (${\textstyle A}$) is ${\textstyle False}$.

Double implication as logical operator has two arguments. It is also known as biconditional operator and it is denoted by ${\textstyle \iff }$. ${\textstyle A\iff B}$ is ${\textstyle True}$ either if both ${\textstyle A}$ and ${\textstyle B}$ are ${\textstyle True}$ or if both are ${\textstyle False}$. ${\textstyle A\iff B}$ is to be read as ${\textstyle A}$ iff ${\textstyle B}$ or ${\textstyle B}$ if and only if ${\textstyle A}$.

${\textstyle \mathrm {\ \ \ \ } }$ Truth tables

Logical operators can be also given by their truth tables specifying the logical value (${\textstyle True}$ or ${\textstyle False}$) of the operator for each possible combinations of the logical values of the arguments of the operator.

The truth table of logical negation is given by Table 3.

Logical negation

${\textstyle A}$	${\textstyle \neg A}$
True	False
False	True

The truth tables for logical conjunction (and) and for logical disjunction (or) are given below by Tables [tab:log_and] and 5.

Logical disjunction

${\textstyle A}$	${\textstyle B}$	${\textstyle A\land B}$
True	True	True
True	False	False
False	True	False
False	False	False

Logical disjunction

${\textstyle A}$	${\textstyle B}$	${\textstyle A\lor B}$
True	True	True
True	False	True
False	True	True
False	False	False

The truth table for logical implication and logical double implication is shown in Table [tab:log_impl] and 7, respectively.

Logical double implication

${\textstyle A}$	${\textstyle B}$	${\textstyle A\implies B}$
True	True	True
True	False	False
False	True	True
False	False	True

Logical double implication

${\textstyle A}$	${\textstyle B}$	${\textstyle A\iff B}$
True	True	True
True	False	False
False	True	False
False	False	True

${\textstyle \mathrm {\ \ \ \ } }$ Logic formulas

Logical operators satisfy several laws, which can be formulated as logic formula. They can be proven either directly based on the interpretations of the arising logical operators or by using the truth tables of the arising logical operators.

Below is a list of the fundamental logic formulas. Here ${\textstyle \equiv }$ stands for the equivalence relation.

• Double negation law
  $${\begin{aligned}&\neg (\neg A)\equiv A\mathrm {~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~} \end{aligned}}$$
• Identity laws Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &(A \land True) \equiv A \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ &(A \lor False) \equiv A \end{aligned}}
• Domination laws
  $${\begin{aligned}&(A\land False)\equiv False\mathrm {~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~} \\&(A\lor True)\equiv True\end{aligned}}$$
• Idempotent laws Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &(A \land A) \equiv A \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ &(A \lor A) \equiv A \end{aligned}}
• Commutative laws
  $${\begin{aligned}&(A\land B)\equiv (B\land A)\mathrm {~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~} \\&(A\lor B)\equiv (B\lor A)\end{aligned}}$$
• Associative laws Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &(A \land B) \land C \equiv A \land (B \land C) \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ &(A \lor B) \lor C \equiv A \lor (B \lor C) \end{aligned}}
• De Morgan laws
  $${\begin{aligned}&\neg (A\land B)\equiv \neg A\lor \neg B\mathrm {~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~} \\&\neg (A\lor B)\equiv \neg A\land \neg B\end{aligned}}$$
• Absorption laws Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &A \land (A \lor B) \equiv A \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ &A \lor (A \land B) \equiv A \end{aligned}}
• Negation laws Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &A \land \neg A \equiv False \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ &A \lor \neg A \equiv True \end{aligned}}

${\textstyle \mathrm {\ \ \ \ } }$ Examples

Example 1

Given the statement ${\textstyle P}$: The USA is a democratic country. The negation of Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle P = \neg P} : The USA is not a democratic country.
Example 2

Given the statement Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle S} : Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle x > 3 \implies x - 4 > -2} . Is the statement ${\textstyle S}$ ${\textstyle True}$ or Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle False}  ?
If Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle x > 3} then ${\textstyle x-4>-2}$ is also Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle True} . So the statement ${\textstyle S}$ is Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle True} .

Predicate logic in mathematics

Propositional logic deals with statements, whose logical value ${\textstyle True}$ or Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle False} is directly decidable. More interesting are the statements, whose logical value depends on variables. Predicate logic deals with logical statements over a set of variables.

The elements of predicate logic are given as

• Predicate
• Variable domain
• Quantifier

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \mathrm{\ \ \ \ }} Predicate

A predicate is a logical statement whose logical value (${\textstyle True}$ or ${\textstyle False}$) depends on one or more variables. Thus formally a predicate is a function with codomain Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \{True,False\}} and with any set as domain. For predicates tipically a function like notation is used with uppercase letter, like e.g. Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle P(x)} , where Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle x} is the variable it depends on. The predicate is defined by giving a statement involving the variables. For example the predicate ${\textstyle P(x)}$ can be defined as "${\textstyle P(x)}$ is the statement: x can be divided by 3". Then ${\textstyle P(9)}$ is Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle True} while Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle P(8)} is Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle False} . Just like functions, predicates can also depend on more variables. For example for the predicate ${\textstyle Q(x,y)}$ "defined as Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle y = x^3+1} " ${\textstyle Q(3,28)}$ is ${\textstyle True}$, since Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle 3^3+1 = 28} .

${\textstyle \mathrm {\ \ \ \ } }$ Variable domain

Besides of involving variables, the definition of a predicate, just like in case of functions, must involve also the domains of the involved variables. So the definition of predicate ${\textstyle P(x)}$ can be completed as

$$P(x):x\mathrm {~can~be~divided~by~} 3,\mathrm {~where~} x\in \mathbb {N} .$$

${\textstyle \mathrm {\ \ \ \ } }$ Quantifier

Often rather a kind of aggregation of the predicate’s truth values is interesting, instead of the concrete logical value of a predicate for a specific value. For example "every negative real number ${\textstyle x}$ satisfies the inequality Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle x^3-3x^2+3x-1 < 0} " is not a statement for one specific value of ${\textstyle x}$, but rather about all possible values of negative ${\textstyle x}$-s.

Such aggregations of the predicate’s truth values are represented by the quantifier of a variable. Thus the quantifier modifies the statement of the predicate by specifying the way of interpretation of the variable, to which the quantifier refers to. The two types of quantifiers are called as

• Existential quantifier,
• Universal quantifier

${\textstyle \mathrm {\ \ \ \ \ \ } }$ Existential quantifier
The existential quantifier specifies the interpretation of the variable by the concept "there exist an element in the domain of the variable which fulfils the given predicate". The existential quantifier is denoted by ${\textstyle \exists }$.
Example The statement ${\textstyle \exists x\in \mathbb {Z} ,x<0}$ is to be interpreted as "there exists an integer number x which is less than zero" . This statement is ${\textstyle True}$, since for example for ${\textstyle x_{0}=-1}$ holds that Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle x_0 < 0} .

The formalism ${\textstyle \exists x\in \mathbb {Z} ,x<0}$ can be also interpreted as an abbreviation for a big OR, which runs over every possible values for Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle x} in the set Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \mathbb{Z}} and tests Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle x < 0} , in other words

$$\ldots \lor (-2<0)\lor (-1<0)\lor (0<0)\lor (1<0)\lor (2<0)\lor \ldots$$

In Python there is an in-built function any() which realizes the existential quantifier. For example Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &\mathrm{strs~}=[\mathrm{'Monday}, \mathrm{'Friday'}, \mathrm{'Sunday'}] \\ &\mathrm{any}([s[0] == \mathrm{'F'~for~}s\mathrm{~in~strs}]) \end{aligned}} would return Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle True} , due to the string ’Friday’.

${\textstyle \mathrm {\ \ \ \ \ \ } }$ Universal quantifier
The universal quantifier represents the concept "every element in the domain of the variable fulfils the given predicate". The existential quantifier is denoted by ${\textstyle \forall }$.
Example The statement ${\textstyle \forall x\in \mathbb {Z} ,x<0}$ is to be interpreted as "every integer number x is less than zero" . This statement is Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle False} , since for example for Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle x_1 = 1} does not hold that ${\textstyle x_{1}<0}$.

The formalism Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \forall x \in \mathbb{Z}, x < 0} can be also interpreted as an abbreviation for a big AND, which runs over every possible values for ${\textstyle x}$ in the set ${\textstyle \mathbb {Z} }$ and tests ${\textstyle x<0}$, in other words

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \ldots \land (-2 < 0) \land (-1 < 0) \land (0 < 0) \land (1 < 0) \land (2 < 0) \land \ldots}

In Python there is an in-built function also for all() which realizes the universal quantifier. For example, for the previously defined list of strings one can test Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle s[3]} as

$${\begin{aligned}&\mathrm {strs~} =[\mathrm {'Monday} ,\mathrm {'Friday'} ,\mathrm {'Sunday'} ]\\&\mathrm {any} ([s[3]==\mathrm {'d'~for~} s\mathrm {~in~strs} ])\end{aligned}}$$

would return ${\textstyle True}$, since the fourth letter of all the three strings in the list is ’d’.

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \mathrm{\ \ \ \ }} Formula and sentence

The general formula in the predicate logic is built up from the following elements

• predicates (including the domains of the involved variables)
• propositional operators ${\textstyle \neg }$, Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \land} , ${\textstyle \lor }$, ${\textstyle \implies }$ and Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \iff}
• the existential and universal quantifiers

A variable is quantified if there is a quantifier referring to it. A sentence is a special case of formula, in which all variables are quantified. The quantified and unquantified variables are also referred as bound and free variables, respectively.

For example the formula Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall x \in \mathbb{N}, x^4 < y} is not a sentence, since the variable ${\textstyle y}$ is not quantified. After quantifying also ${\textstyle y}$ we get the sentence

$$\forall x,y\in \mathbb {N} ,x^{4}<y$$

Valid places for comma for arising in predicate formulas are given as

• separating variables in the same quantification,
• immediatly after the quantification and
• seperating arguments in predicate function.

An example for a predicate formula built up from all the three types of elements is given as

$$\forall x,y\in \mathbb {N} ,\exists z\in \mathbb {Z} ,P(x,y)\implies R(x,y,z)$$

${\textstyle \mathrm {\ \ \ \ } }$ Simplification rules

Taking a negation of a statement is very common in practice. However usually it is not easy to interpret and understand negation of formulas. In this case simplification rules can be applied in order to push the negation to right. Below is a list of useful simplification rules with negation.

• Double negation law Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &\neg (\neg P) \equiv P \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~} \end{aligned}}
• De Morgan laws Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &\neg (P \land Q) \equiv \neg P \lor \neg Q \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ &\neg (P \lor Q) \equiv \neg P \land \neg Q \end{aligned}}
• Negation rules for ${\textstyle \implies }$ and ${\textstyle iff}$
  $${\begin{aligned}&\neg (P\implies Q)\equiv P\land (\neg Q)\mathrm {~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~} \\&\neg (P\iff Q)\equiv (P\land (\neg Q))\lor ((\neg P)\land Q)\end{aligned}}$$
• Negation rules for quantifiers Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &\neg (\exists x \in \mathbb{S}, P(x)) \equiv \forall x \in \mathbb{S}, \neg P(x) \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ &\neg (\forall x \in \mathbb{S}, P(x)) \equiv \exists x \in \mathbb{S}, \neg P(x) \end{aligned}}

First-order logic

First-order logic, also called predicate logic, is used not only in mathematics, but also in philosophy, linguistics and computer science. First-order logic allows sentences containing quantified variables. In first-order logic sentences are formulated by means of predicate, like e.g. "For every x, if x has a son, then x is parent".

Description of first-order formulas

In this subsection we give a brief overview on the description of the first-order logic. The description of first-order logic requires the introduction of infinite sets like terms and formulas, which are defined inductively.

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \mathrm{\ \ \ \ }} Elements of first-order logic

The elements of first-order formulas are given as

• Variables, like x,y, representing any objects, i.e. whose meaning is determined by the semantic.
• Functions, where function with ${\textstyle n}$ arguments are called ${\textstyle n}$-ary functions.
• Predicates, where predicates with Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle n} arguments are called ${\textstyle n}$-ary predicates.
• Equality
• Logical operators or logical connectives

${\textstyle \mathrm {\ \ \ \ } }$ Terms

The infinite set of terms is defined by applying the following rules

• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle {\bf T1.}} Variables. Any variable symbol itself is a term.
• ${\textstyle {\bf {T2.}}}$ Functions. If Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle f()} is a n-ary function and ${\textstyle t_{1},\ldots ,t_{n}}$ are terms then applying Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle f()} to these terms, ${\textstyle f(t_{1},\ldots ,t_{n})}$ is also a term.

Terms are only the expressions, which can be obtained by finite many application of rules ${\textstyle {\bf {T1.}}}$ and ${\textstyle {\bf {T2.}}}$ are terms.

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \mathrm{\ \ \ \ }} Formulas

The infinite set of formulas is defined by applying the following rules

• ${\textstyle {\bf {F1.}}}$ Predicate. If Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle P()} is a n-ary predicate and ${\textstyle t_{1},\ldots ,t_{n}}$ are terms then applying ${\textstyle P()}$ to these terms, ${\textstyle P(t_{1},\ldots ,t_{n})}$ is a formula
• ${\textstyle {\bf {F2.}}}$ Equality. If ${\textstyle t_{1}}$ and Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle t_1} are terms then the equality symbol applied to them, ${\textstyle t_{1}=t_{2}}$ is a formula.
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle {\bf F3.}} Negation. If ${\textstyle \Psi }$ is a formula then Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \neg \Psi} is also a formula.
• Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle {\bf F4.}} Binary logical operators. If ${\textstyle \Psi }$ and ${\textstyle \Phi }$ are formulas then any binary logical functions of them (like e.g. Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \Psi \land \Phi} , Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \Psi \implies \Phi} , etc. ) is also a formula.
• ${\textstyle {\bf {F5.}}}$ Quantifiers. If ${\textstyle \Psi }$ is a formula and x is a variable then ${\textstyle \forall x\Psi }$ and Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle \exists x \Psi} are also formulas.

The expressions obtained by finite many applications of only rules Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle {\bf F1.}} and ${\textstyle {\bf {F2.}}}$ are called atomic formulas. Formulas are only the expressions, which can be obtained by finite many applications of the rules Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle {\bf F1.}} - ${\textstyle {\bf {F5.}}}$.

${\textstyle \mathrm {\ \ \ \ } }$ Precedence of the logical operators

Precedence of the logical operators enables to interpret a formula without placing any parentheses into it. The precedence of the logical operators in decreasing order is given by

• Negation
• Disjunction and conjunction
• Quantifiers
• Implication

Nevertheless extra parentheses can be inserted into formulas.

Formal description of first-order logic

Description of first-order logic as language is completely formal. The terms and formulas are strings of symbols, the symbols together forms the alphabet of the language.

${\textstyle \mathrm {\ \ \ \ } }$ Alphabet

The alphabet of symbols can be divided into the following two groups:

• Logical symbols
• Non-logical symbols

The logical symbols include the infinite set of variables, the logical operators, the quantifier symbols, parenthesis, brackets and other punctuation sybols as well as the equality symbol.

The non-logical symbols include the infinite set of n-ary predicate symbols (like e.g. Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle P^2_i} , ${\textstyle i\geq 0}$ for binary predicate symbols) and the infinite set of n-ary function symbols (like e.g. ${\textstyle f_{i}^{3}}$, ${\textstyle i\geq 0}$ for ternary function symbols)

${\textstyle \mathrm {\ \ \ \ } }$ Language of syntactically valid first-order formulas

Based on the alphabet, the inductive definition of terms, atomic formulas and formulas the language of syntactically valid first-order formulas can be defined as a cntext-free grammar. This can be seen in Backus-Naur form in Figure 15.

Figure 15: Language of syntactically valid first order logic formulas as context-free grammar in BNF}

Semantics

Semantic meaning of a first-order language is determined by its interpretation. This interpretation - assigns a way of interpretation to each non-logical symbol in that language and - determines the domains of variables.

Deductive systems

Deductive system is to show on syntactic level, that one formula logically follows from another formula.

The deductive system is sound if every formula which can be derived in the system is logically valid. On the other hand a deductive system is complete if every logically valid formula can be derived in it.

An important property of the deductive systems that they are completely syntactic, so no any interpretation is utilized for the derivations in such system. This means that if the deductive system is sound, than it holds in every possible interpretation of the language describing the system.

${\textstyle \mathrm {\ \ \ \ } }$ Rule of inference

The rule of inference represents the concept that from a given formula (set of formulas) another formula (set of formulas) can be derived as a conclusion.

One commonly used rule of inference is the rule of substitution. Let ${\textstyle t}$ and ${\textstyle \Psi (x)}$ be a term and a formula containing the variable ${\textstyle x}$ respectively. Then replacing all free instances of ${\textstyle x}$ by ${\textstyle t}$ in the formula ${\textstyle \Psi (x)}$ is denoted by ${\textstyle \Psi [t/x]}$. The rule of substitutions states that for any ${\textstyle \Psi (x)}$ and Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\textstyle t} it can be concluded that ${\textstyle \Psi [t/x]}$, given the condition that no free variable of ${\textstyle t}$ becomes bound during the substitution process.

${\textstyle \mathrm {\ \ \ \ } }$ Formula identities

Besides of the simplification rules provided in [simpl_rules] several further useful formula identities are listed below.

• Commutativity of the same quantifier
  $${\begin{aligned}&\forall x\forall yP(x,y)\equiv \forall y\forall xP(x,y)\mathrm {~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~} \\&\exists x\exists yP(x,y)\equiv \exists y\exists xP(x,y)\end{aligned}}$$
• Quantifier with disjunction and conjunction - distributivity Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{aligned} &\forall x P(x) \land \forall x Q(x) \equiv \forall x (P(x) \land Q(x)) \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ &\exists x P(x) \lor \exists x Q(x) \equiv \exists x (P(x) \lor Q(x)) \end{aligned}}
• Quantifier with disjunction and conjunction - exchangeability
  $${\begin{aligned}&P\land \exists xQ(x)\equiv \exists x(P\land Q(x))\mathrm {~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~} \\\%\mathrm {~~where~} x\mathrm {~must~not~occur~free~in} P&P\lor \forall xQ(x)\equiv \forall x(P\lor Q(x))\%\mathrm {~~where~} x\mathrm {~must~not~occur~free~in} P\end{aligned}}$$

Applications of first-order logic

First-order logic has applications in different scientific fields. Some of them are given below.

• In mathematics it is used for formalizing and provides proof techniques for mathematical theorems.
• In computer science it is used for logical reasoning and verifying computer programs.
• In linguistic it is used for formalizing simple quantifier construction in natural language, which serves a basis for knowledge representation languages.