Information Technology Reference
In-Depth Information
Theory
PA
is the following theory which expresses Peano's axioms as FOL formulae
(on symbols 0
,
1 for distinct constants and
+
for a binary operation):
¬∃
(
=
+
)
x
0
x
1
∀
(
∀
((
+
=
+
)
→
(
=
)))
x
y
x
1
y
1
x
y
P
(
0
)
∧∀
x
(
P
(
x
)
→
P
(
x
+
1
))
→∀
x
(
P
(
x
))
.
One of the most important results in formal logic, originally due to Kurt G odel es-
tablishes the existence of algorithmically definable logical calculi that can express
completely the FOL logical validity. In fact, let
be a derivation relation over un-
interpreted formulae defined in some algorithmic way (many of such calculi were
found in the last century), such that we write:
Φ
ϕ
to denote that formula
ϕ
is
derivable
from a set of formulae
Φ
,thenGodel's
com-
pleteness theorem
asserts the following equivalence:
Φ
|
=
ϕ
if and only if
Φ
ϕ
.
Some important properties of FOL are briefly reported:
1. The completeness of FOL is related to another important property of this logic
called
compactness
. It asserts that a theory
Φ
has a model (there is a model
has a model.
2. Any sentence of a FOL theory can be transformed into an equivalent formula,
which is called Skolem normal form, where quantifications are all at the begin-
ning of a propositional formula.
3. By introducing suitable operation symbols, any formula can be transformed into
an equisatisfiable formula
where all the sentences of
Φ
hold) iff every finite subset of
Φ
, where only uni-
versal quantifications are, at the beginning of a propositional formula.
4. Herbrand expansions imply that any FOL theory is equisatisfiable with a propo-
sitional theory (which in general may be infinite even if the original FOL theory
is finite).
5. From the propositional representation of FOL theories, it can be derived that any
satisfiable FOL theory has a model with numerable domain. This phenomenon
shows a deep relationship between FOL and natural numbers, and it is related to
the existence of non-standard models of real numbers (Skolem's paradox: Real
numbers that are a non-denumerable set have a denumerable FOL model).
ϕ
, called Herbrand expansion of
ϕ
FOL can be considered the formal language of mathematics because any mathemat-
ical theory can be represented as a FOL theory by using a suitable representation of
its axioms as FOL sentences.
