SAFFER Zsolt: Die Seite wurde neu angelegt: „ = 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 $2 < 4$ is $True$ . ''' $\mathrm{\…“$

2025-03-04T23:06:47Z

Die Seite wurde neu angelegt: „<span id="logic"></span> = Logic = <span id="mathematical-logic"></span> == Mathematical logic == Mathematical logic is the study of logic in mathematics. <span id="propositional-logic"></span> === Propositional logic === Propositional logic deals with logical statements, which are directly decidable. For example the logical statement <math display="inline">2 < 4</math> is <math display="inline">True</math>. <span>'''<math display="inline">\mathrm{\…“

Neue Seite

<span id="logic"></span>
= Logic =

<span id="mathematical-logic"></span>
== Mathematical logic ==

Mathematical logic is the study of logic in mathematics.

<span id="propositional-logic"></span>
=== Propositional logic ===

Propositional logic deals with logical statements, which are directly decidable. For example the logical statement <math display="inline">2 < 4</math> is <math display="inline">True</math>.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Logical operators'''</span>

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 <math display="inline">True</math> if the statement is <math display="inline">False</math>. Negation is also called as NOT operator and it is denoted in mathematical logic as <math display="inline">\neg</math>. For example if <math display="inline">A</math> stands for a statement then <math display="inline">\neg A</math> is <math display="inline">True</math> whenever <math display="inline">A</math> is <math display="inline">False</math> and vice versa.

Th conjunction and disjunction as logical operators have two arguments. Conjunction is also known as AND operator and denoted by <math display="inline">\land</math>. Disjunction is also known as OR operator and denoted by <math display="inline">\lor</math>.

Implication as logical operator has two arguments. It is also known as conditional operator and it is denoted by <math display="inline">\implies</math>. Implication (e.g. <math display="inline">A \implies B</math>) is <math display="inline">True</math> if truth of first argument (<math display="inline">A</math>) implies truth of second argument (<math display="inline">B</math>) or the first argument (<math display="inline">A</math>) is <math display="inline">False</math>.

Double implication as logical operator has two arguments. It is also known as biconditional operator and it is denoted by <math display="inline">\iff</math>. <math display="inline">A \iff B</math> is <math display="inline">True</math> either if both <math display="inline">A</math> and <math display="inline">B</math> are <math display="inline">True</math> or if both are <math display="inline">False</math>. <math display="inline">A \iff B</math> is to be read as <math display="inline">A</math> iff <math display="inline">B</math> or <math display="inline">B</math> if and only if <math display="inline">A</math>.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Truth tables'''</span>

Logical operators can be also given by their truth tables specifying the logical value (<math display="inline">True</math> or <math display="inline">False</math>) 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 [[#tab:log_neg|3]].

<div class="center">

<div id="tab:log_neg">

{| class="wikitable"
|+ Logical negation
|-
! style="text-align: center;"| <math display="inline">A</math>
! style="text-align: center;"| <math display="inline">\neg A</math>
|-
| style="text-align: center;"| True
| style="text-align: center;"| False
|-
| style="text-align: center;"| False
| style="text-align: center;"| True
|}

</div>

</div>
The truth tables for logical conjunction (and) and for logical disjunction (or) are given below by Tables [[#tab:log_and|[tab:log_and]]] and [[#tab:log_or|5]].

<div class="center">

<div id="tab:log_or">

{| class="wikitable"
|+ Logical disjunction
|-
! style="text-align: center;"| <math display="inline">A</math>
! style="text-align: center;"| <math display="inline">B</math>
! style="text-align: center;"| <math display="inline">A \land B</math>
|-
| style="text-align: center;"| True
| style="text-align: center;"| True
| style="text-align: center;"| True
|-
| style="text-align: center;"| True
| style="text-align: center;"| False
| style="text-align: center;"| False
|-
| style="text-align: center;"| False
| style="text-align: center;"| True
| style="text-align: center;"| False
|-
| style="text-align: center;"| False
| style="text-align: center;"| False
| style="text-align: center;"| False
|}

</div>

</div>
<div class="center">

<div id="tab:log_or">

{| class="wikitable"
|+ Logical disjunction
|-
! style="text-align: center;"| <math display="inline">A</math>
! style="text-align: center;"| <math display="inline">B</math>
! style="text-align: center;"| <math display="inline">A \lor B</math>
|-
| style="text-align: center;"| True
| style="text-align: center;"| True
| style="text-align: center;"| True
|-
| style="text-align: center;"| True
| style="text-align: center;"| False
| style="text-align: center;"| True
|-
| style="text-align: center;"| False
| style="text-align: center;"| True
| style="text-align: center;"| True
|-
| style="text-align: center;"| False
| style="text-align: center;"| False
| style="text-align: center;"| False
|}

</div>

</div>
The truth table for logical implication and logical double implication is shown in Table [[#tab:log_impl|[tab:log_impl]]] and [[#tab:log_doub_impl|7]], respectively.

<div class="center">

<div id="tab:log_doub_impl">

{| class="wikitable"
|+ Logical double implication
|-
! style="text-align: center;"| <math display="inline">A</math>
! style="text-align: center;"| <math display="inline">B</math>
! style="text-align: center;"| <math display="inline">A \implies B</math>
|-
| style="text-align: center;"| True
| style="text-align: center;"| True
| style="text-align: center;"| True
|-
| style="text-align: center;"| True
| style="text-align: center;"| False
| style="text-align: center;"| False
|-
| style="text-align: center;"| False
| style="text-align: center;"| True
| style="text-align: center;"| True
|-
| style="text-align: center;"| False
| style="text-align: center;"| False
| style="text-align: center;"| True
|}

</div>

</div>
<div class="center">

<div id="tab:log_doub_impl">

{| class="wikitable"
|+ Logical double implication
|-
! style="text-align: center;"| <math display="inline">A</math>
! style="text-align: center;"| <math display="inline">B</math>
! style="text-align: center;"| <math display="inline">A \iff B</math>
|-
| style="text-align: center;"| True
| style="text-align: center;"| True
| style="text-align: center;"| True
|-
| style="text-align: center;"| True
| style="text-align: center;"| False
| style="text-align: center;"| False
|-
| style="text-align: center;"| False
| style="text-align: center;"| True
| style="text-align: center;"| False
|-
| style="text-align: center;"| False
| style="text-align: center;"| False
| style="text-align: center;"| True
|}

</div>

</div>
<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Logic formulas'''</span>

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 <math display="inline">\equiv</math> stands for the equivalence relation.

* Double negation law <math display="block">\begin{aligned}
&\neg (\neg A) \equiv A \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}

\end{aligned}</math>
* Identity laws <math display="block">\begin{aligned}
&(A \land True) \equiv A \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&(A \lor False) \equiv A

\end{aligned}</math>
* Domination laws <math display="block">\begin{aligned}
&(A \land False ) \equiv False \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&(A \lor True) \equiv True

\end{aligned}</math>
* Idempotent laws <math display="block">\begin{aligned}
&(A \land A) \equiv A \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&(A \lor A) \equiv A

\end{aligned}</math>
* Commutative laws <math display="block">\begin{aligned}
&(A \land B) \equiv (B \land A) \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&(A \lor B) \equiv (B \lor A)

\end{aligned}</math>
* Associative laws <math display="block">\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}</math>
* De Morgan laws <math display="block">\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}</math>
* Absorption laws <math display="block">\begin{aligned}
&A \land (A \lor B) \equiv A \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&A \lor (A \land B) \equiv A

\end{aligned}</math>
* Negation laws <math display="block">\begin{aligned}
&A \land \neg A \equiv False \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&A \lor \neg A \equiv True

\end{aligned}</math>

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Examples'''</span>

<span>''Example 1''</span>

Given the statement <math display="inline">P</math>: The USA is a democratic country. The negation of <math display="inline">P = \neg P</math>: The USA is not a democratic country.<br />
<span>''Example 2''</span>

Given the statement <math display="inline">S</math>: <math display="inline">x > 3 \implies x - 4 > -2</math>. Is the statement <math display="inline">S</math> <math display="inline">True</math> or <math display="inline">False</math> ?<br />
If <math display="inline">x > 3</math> then <math display="inline">x-4 > -2</math> is also <math display="inline">True</math>. So the statement <math display="inline">S</math> is <math display="inline">True</math>.

<span id="predicate-logic-in-mathematics"></span>
=== Predicate logic in mathematics ===

Propositional logic deals with statements, whose logical value <math display="inline">True</math> or <math display="inline">False</math> 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

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Predicate'''</span>

A predicate is a logical statement whose logical value (<math display="inline">True</math> or <math display="inline">False</math>) depends on one or more variables. Thus formally a predicate is a function with codomain <math display="inline">\{True,False\}</math> and with any set as domain. For predicates tipically a function like notation is used with uppercase letter, like e.g. <math display="inline">P(x)</math>, where <math display="inline">x</math> is the variable it depends on. The predicate is defined by giving a statement involving the variables. For example the predicate <math display="inline">P(x)</math> can be defined as "<math display="inline">P(x)</math> is the statement: x can be divided by 3". Then <math display="inline">P(9)</math> is <math display="inline">True</math> while <math display="inline">P(8)</math> is <math display="inline">False</math>. Just like functions, predicates can also depend on more variables. For example for the predicate <math display="inline">Q(x,y)</math> "defined as <math display="inline">y = x^3+1</math>" <math display="inline">Q(3,28)</math> is <math display="inline">True</math>, since <math display="inline">3^3+1 = 28</math>.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Variable domain'''</span>

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 <math display="inline">P(x)</math> can be completed as <math display="block">P(x): x \mathrm{~can~be~divided~by~} 3, \mathrm{~where~} x \in \mathbb{N}.</math>

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Quantifier'''</span>

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 <math display="inline">x</math> satisfies the inequality <math display="inline">x^3-3x^2+3x-1 < 0</math>" is not a statement for one specific value of <math display="inline">x</math>, but rather about all possible values of negative <math display="inline">x</math>-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

<span>'''''<math display="inline">\mathrm{\ \ \ \ \ \ }</math> Existential quantifier'''''</span><br />
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 <math display="inline">\exists</math>.<br />
<span>''Example''</span> The statement <math display="inline">\exists x \in \mathbb{Z}, x < 0</math> is to be interpreted as "there exists an integer number x which is less than zero" . This statement is <math display="inline">True</math>, since for example for <math display="inline">x_0 = -1</math> holds that <math display="inline">x_0 < 0</math>.

The formalism <math display="inline">\exists x \in \mathbb{Z}, x < 0</math> can be also interpreted as an abbreviation for a big OR, which runs over every possible values for <math display="inline">x</math> in the set <math display="inline">\mathbb{Z}</math> and tests <math display="inline">x < 0</math>, in other words

<math display="block">\ldots \lor (-2 < 0) \lor (-1 < 0) \lor (0 < 0) \lor (1 < 0) \lor (2 < 0) \lor \ldots</math>

In Python there is an in-built function any() which realizes the existential quantifier. For example <math display="block">\begin{aligned}
&\mathrm{strs~}=[\mathrm{'Monday}, \mathrm{'Friday'}, \mathrm{'Sunday'}] \\
&\mathrm{any}([s[0] == \mathrm{'F'~for~}s\mathrm{~in~strs}])
\end{aligned}</math> would return <math display="inline">True</math>, due to the string ’Friday’.

<span>'''''<math display="inline">\mathrm{\ \ \ \ \ \ }</math> Universal quantifier'''''</span><br />
The universal quantifier represents the concept "every element in the domain of the variable fulfils the given predicate". The existential quantifier is denoted by <math display="inline">\forall</math>.<br />
<span>''Example''</span> The statement <math display="inline">\forall x \in \mathbb{Z}, x < 0</math> is to be interpreted as "every integer number x is less than zero" . This statement is <math display="inline">False</math>, since for example for <math display="inline">x_1 = 1</math> does not hold that <math display="inline">x_1 < 0</math>.

The formalism <math display="inline">\forall x \in \mathbb{Z}, x < 0</math> can be also interpreted as an abbreviation for a big AND, which runs over every possible values for <math display="inline">x</math> in the set <math display="inline">\mathbb{Z}</math> and tests <math display="inline">x < 0</math>, in other words

<math display="block">\ldots \land (-2 < 0) \land (-1 < 0) \land (0 < 0) \land (1 < 0) \land (2 < 0) \land \ldots</math>

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 <math display="inline">s[3]</math> as <math display="block">\begin{aligned}
&\mathrm{strs~}=[\mathrm{'Monday}, \mathrm{'Friday'}, \mathrm{'Sunday'}] \\
&\mathrm{any}([s[3] == \mathrm{'d'~for~}s\mathrm{~in~strs}])
\end{aligned}</math> would return <math display="inline">True</math>, since the fourth letter of all the three strings in the list is ’d’.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Formula and sentence'''</span>

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

* predicates (including the domains of the involved variables)
* propositional operators <math display="inline">\neg</math>, <math display="inline">\land</math>, <math display="inline">\lor</math>, <math display="inline">\implies</math> and <math display="inline">\iff</math>
* 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 <math display="block">\forall x \in \mathbb{N}, x^4 < y</math> is not a sentence, since the variable <math display="inline">y</math> is not quantified. After quantifying also <math display="inline">y</math> we get the sentence <math display="block">\forall x,y \in \mathbb{N}, x^4 < y</math>

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 <math display="block">\forall x,y \in \mathbb{N}, \exists z \in \mathbb{Z} , P(x,y) \implies R(x,y,z)</math>

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Simplification rules'''</span> <span id="simpl_rules" label="simpl_rules"></span>

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 <math display="block">\begin{aligned}
&\neg (\neg P) \equiv P \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}

\end{aligned}</math>
* De Morgan laws <math display="block">\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}</math>
* Negation rules for <math display="inline">\implies</math> and <math display="inline">iff</math> <math display="block">\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}</math>
* Negation rules for quantifiers <math display="block">\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}</math>

<span id="first-order-logic"></span>
== 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".

<span id="description-of-first-order-formulas"></span>
=== 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.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Elements of first-order logic'''</span>

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 <math display="inline">n</math> arguments are called <math display="inline">n</math>-ary functions.
* Predicates, where predicates with <math display="inline">n</math> arguments are called <math display="inline">n</math>-ary predicates.
* Equality
* Logical operators or logical connectives

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Terms'''</span>

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

* <math display="inline">{\bf T1.}</math> Variables. Any variable symbol itself is a term.
* <math display="inline">{\bf T2.}</math> Functions. If <math display="inline">f()</math> is a n-ary function and <math display="inline">t_1,\ldots, t_n</math> are terms then applying <math display="inline">f()</math> to these terms, <math display="inline">f(t_1,\ldots, t_n)</math> is also a term.

Terms are only the expressions, which can be obtained by finite many application of rules <math display="inline">{\bf T1.}</math> and <math display="inline">{\bf T2.}</math> are terms.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Formulas'''</span>

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

* <math display="inline">{\bf F1.}</math> Predicate. If <math display="inline">P()</math> is a n-ary predicate and <math display="inline">t_1,\ldots, t_n</math> are terms then applying <math display="inline">P()</math> to these terms, <math display="inline">P(t_1,\ldots, t_n)</math> is a formula
* <math display="inline">{\bf F2.}</math> Equality. If <math display="inline">t_1</math> and <math display="inline">t_1</math> are terms then the equality symbol applied to them, <math display="inline">t_1=t_2</math> is a formula.
* <math display="inline">{\bf F3.}</math> Negation. If <math display="inline">\Psi</math> is a formula then <math display="inline">\neg \Psi</math> is also a formula.
* <math display="inline">{\bf F4.}</math> Binary logical operators. If <math display="inline">\Psi</math> and <math display="inline">\Phi</math> are formulas then any binary logical functions of them (like e.g. <math display="inline">\Psi \land \Phi</math>, <math display="inline">\Psi \implies \Phi</math>, etc. ) is also a formula.
* <math display="inline">{\bf F5.}</math> Quantifiers. If <math display="inline">\Psi</math> is a formula and x is a variable then <math display="inline">\forall x \Psi</math> and <math display="inline">\exists x \Psi</math> are also formulas.

The expressions obtained by finite many applications of only rules <math display="inline">{\bf F1.}</math> and <math display="inline">{\bf F2.}</math> are called atomic formulas. Formulas are only the expressions, which can be obtained by finite many applications of the rules <math display="inline">{\bf F1.}</math> - <math display="inline">{\bf F5.}</math>.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Precedence of the logical operators'''</span>

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.

<span id="formal-description-of-first-order-logic"></span>
=== 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.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Alphabet'''</span>

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. <math display="inline">P^2_i</math>, <math display="inline">i \geq 0</math> for binary predicate symbols) and the infinite set of n-ary function symbols (like e.g. <math display="inline">f^3_i</math>, <math display="inline">i \geq 0</math> for ternary function symbols)

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Language of syntactically valid first-order formulas'''</span>

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 [[#fig:Lang_folf_cfg_BNF|15]].

<div id="fig:Lang_folf_cfg_BNF" class="figure">

[[File:./figs/Language_first_order_logic_BNF_grammar.pdf]]

</div>
<span id="semantics"></span>
=== 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.

<span id="deductive-systems"></span>
=== 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.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Rule of inference'''</span>

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 <math display="inline">t</math> and <math display="inline">\Psi(x)</math> be a term and a formula containing the variable <math display="inline">x</math> respectively. Then replacing all free instances of <math display="inline">x</math> by <math display="inline">t</math> in the formula <math display="inline">\Psi(x)</math> is denoted by <math display="inline">\Psi[t/x]</math>. The rule of substitutions states that for any <math display="inline">\Psi(x)</math> and <math display="inline">t</math> it can be concluded that <math display="inline">\Psi[t/x]</math>, given the condition that no free variable of <math display="inline">t</math> becomes bound during the substitution process.

<span>'''<math display="inline">\mathrm{\ \ \ \ }</math> Formula identities'''</span>

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

* Commutativity of the same quantifier <math display="block">\begin{aligned}
&\forall x \forall y P(x,y) \equiv \forall y \forall x P(x,y) \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\
&\exists x \exists y P(x,y) \equiv \exists y \exists x P(x,y)

\end{aligned}</math>
* Quantifier with disjunction and conjunction - distributivity <math display="block">\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}</math>
* Quantifier with disjunction and conjunction - exchangeability <math display="block">\begin{aligned}
&P \land \exists x Q(x) \equiv \exists x (P \land Q(x)) \mathrm{~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}\\ %\mathrm{~~where~}x\mathrm{~must~not ~occur~free~in}P
&P \lor \forall x Q(x) \equiv \forall x (P \lor Q(x)) %\mathrm{~~where~}x\mathrm{~must~not ~occur~free~in}P

\end{aligned}</math>

<span id="applications-of-first-order-logic"></span>
=== 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.

← Nächstältere Version		Version vom 13. März 2025, 21:12 Uhr
Zeile 424:		Zeile 424:
	<div id="fig:Lang_folf_cfg_BNF" class="figure">		<div id="fig:Lang_folf_cfg_BNF" class="figure">

	[[Datei:Language_first_order_logic_BNF_gramma.jpg\|460px\|thumb\|center\|Figure 15: Language of syntactically valid first order logic formulas as context-free grammar in BNF}]]		[[Datei:Language_first_order_logic_BNF_gramma.jpg\|460px\|thumb\|center\|Figure 15: Language of syntactically valid first order logic formulas as context-free grammar in BNF]]

	</div>		</div>

← Nächstältere Version		Version vom 13. März 2025, 21:09 Uhr
Zeile 424:		Zeile 424:
	<div id="fig:Lang_folf_cfg_BNF" class="figure">		<div id="fig:Lang_folf_cfg_BNF" class="figure">

	[[Datei:~~Language_first_order_logic_BNF_grammar~~.jpg\|460px\|thumb\|center\|Figure 15: Language of syntactically valid first order logic formulas as context-free grammar in BNF}]]		[[Datei:Language_first_order_logic_BNF_gramma.jpg\|460px\|thumb\|center\|Figure 15: Language of syntactically valid first order logic formulas as context-free grammar in BNF}]]

	</div>		</div>

← Nächstältere Version		Version vom 13. März 2025, 20:49 Uhr
Zeile 424:		Zeile 424:
	<div id="fig:Lang_folf_cfg_BNF" class="figure">		<div id="fig:Lang_folf_cfg_BNF" class="figure">

	[[~~File~~:~~./figs/~~Language_first_order_logic_BNF_grammar.~~pdf~~]]		[[Datei:Language_first_order_logic_BNF_grammar.jpg\|460px\|thumb\|center\|Figure 15: Language of syntactically valid first order logic formulas as context-free grammar in BNF}]]

	</div>		</div>

Logic - Versionsgeschichte

SAFFER Zsolt am 13. März 2025 um 21:12 Uhr

SAFFER Zsolt am 13. März 2025 um 21:11 Uhr

SAFFER Zsolt am 13. März 2025 um 21:09 Uhr

SAFFER Zsolt am 13. März 2025 um 20:49 Uhr

← Nächstältere Version		Version vom 13. März 2025, 21:11 Uhr
Zeile 66:		Zeile 66:

	{\| class="wikitable"		{\| class="wikitable"
	\|+ Logical ~~disjunction~~		\|+ Logical conjunction
	\|-		\|-
	! style="text-align: center;"\| <math display="inline">A</math>		! style="text-align: center;"\| <math display="inline">A</math>
Zeile 132:		Zeile 132:

	{\| class="wikitable"		{\| class="wikitable"
	\|+ Logical ~~double~~ implication		\|+ Logical implication
	\|-		\|-
	! style="text-align: center;"\| <math display="inline">A</math>		! style="text-align: center;"\| <math display="inline">A</math>