Information Technology Reference
In-Depth Information
Let us define
universal
and
existential quantifications
in the following way, where
P
stands for any unary predicate,
D
for the domain of a given model, and
x
for
a variable ranging over
D
(1 stands for
true
, 0 stands for
false
and assume that
0
<
1):
∀
(
)=
{
(
)
|
∈
}
D
P
x
min
P
x
x
D
∃
D
P
(
x
)=
max
{
P
(
x
)
|
x
∈
D
}.
If we apply connectives and quantifiers to atomic formulae over a model
M
and
variables
V
, then we generate the
formulae
over
and over a set of variables
V
.A
variable occurrence is free if it is not quantified. Formulae denote
k
-ary predicates
if
k
different free variables occur in them, while they denote a truth value if no free
variable occurs in them. Formulae without free variables are called
sentences
over
M
M
(over its signature). A FOL
theory
is a set of sentences over a FOL signature.
We say that a sentence
ϕ
over
M
holds in
M
if it denotes the
true
value (say 1)
and we write:
M |
=
ϕ
.
We can obtain a definition of logical validity by means of the following notion of
interpretation
of FOL formulae over FOL models.
Let
M
be a model of signature
Σ
and domain
D
,and
F
(
Σ
,
V
)
the FOL formulae
over the signature
Σ
and the set
V
of variables. An
interpretation
of
F
(
Σ
,
V
)
in
M
is defined by giving to the constant, operation, and relation symbols of
Σ
their
meaning in the model
, that is, by giving to the terms their denotation in
D
with
the variables in
V
ranging over
D
. Then, for an atomic formula
M
ϕ
=
R
(
t
1
,
t
2
,...,
t
k
)
where no variable occurs, the interpretation
τ
is defined by stating
τ
(
ϕ
)=
1ifand
only if the relation
R
holds on the terms
t
1
,
t
2
,...,
t
k
of
M
. The interpretation
τ
is
extended to all the sentences of
F
, by requiring the following conditions for
the truth values of all non-atomic sentences of
F
(
Σ
,
V
)
(
Σ
,
V
)
:
•
τ
(
ϕ
∧
ψ
)=
τ
(
ϕ
)
∧
τ
(
ψ
)
•
τ
(
ϕ
∨
ψ
)=
τ
(
ϕ
)
∨
τ
(
ψ
)
•
τ
(
¬
ϕ
)=
¬
τ
(
ϕ
)
•
τ
(
ϕ
→
ψ
)=
τ
(
ϕ
)
→
τ
(
ψ
)
•
τ
(
ϕ
↔
ψ
)=
τ
(
ϕ
)
↔
τ
(
ψ
)
•
τ
(
∀
P
(
x
)) =
∀
D
τ
(
P
(
x
))
•
τ
(
∃
P
(
x
)) =
∃
D
τ
(
P
(
x
))
.
Asentenceof
F
(
Σ
,
V
)
is
logically valid
iff it is true in every FOL model of signature
Σ
.Itis
satisfiable
if it is has a FOL model.
Given a FOL theory
Φ
and a FOL sentence
ϕ
we say that
ϕ
is a
logical conse-
quence
of
Φ
, by writing:
Φ
|
=
ϕ
when
are true.
The discovery of the first (informal) counter-model proof, showing the indepen-
dence of the
fifth Euclidean axiom
(on the unicity of the parallel line) from the
remaining Euclidean axioms was essentially based on the notion of interpretation.
ϕ
is true in all models where all the sentences of
Φ
