Database Reference
In-Depth Information
and
X
are empty, this definition reduces to the Classical
Propositional Logic CPL, where
I
T
is its valuation.
In a formula
(
Notice that, when
R
,
F
x)
.
A variable
y
inaformula
ψ
is called a bounded variable iff it is the variable of a
quantifier
(
∃
x)φ
, the formula
φ
is called “action field” for the quantifier
(
∃
y)
in the formula
ψ
.
A variable
x
is free in
ψ
if it is not bounded. The universal quantifier is defined by
∀=¬∃¬
∃
y)
in
ψ
, or it is in the action field of a quantifier
(
∃
.
Disjunction
φ
∨
⇒
¬
¬
∧¬
ψ
and implication
φ
ψ
are expressed by
(
φ
ψ)
and
.
=
¬
φ
∨
ψ
, respectively. In FOL with the identity
, the formula
(
∃
1
x)φ(x)
denotes
.
=
the formula
(
y))
. We use the built-in
binary identity relational symbol (predicate)
r
, with
r
(x,y)
for
x
∃
x)φ(x)
∧
(
∀
x)(
∀
y)(φ(x)
∧
φ(y)
⇒
(x
.
=
y
, as well.
We can introduce the sorts in order to be able to assign each variable
x
i
toasort
S
i
⊆
U
is a given domain for the FOL (for example, for natural numbers,
for reals, for dates, etc., as used for some attributes in database relations). An as-
signment
g
where
U
for variables in
X
is applied only to free variables in terms and
formulae. If we use sorts for variables then for each sorted variable
x
i
∈
:
X
→
U
X
an assign-
X
ment
g
must satisfy the auxiliary condition
g(x
i
)
∈
S
i
. Such an assignment
g
∈
U
can be recursively and uniquely extended into the assignment
g
∗
:
T
→
U
X
, where
T
X
denotes the set of all terms with variables in
X
,by
1.
g
∗
(t)
=
g(x
)
∈
U
if the term
t
is a variable
x
∈
X
.
2.
g
∗
(t)
=
I
T
(c)
∈
U
if the term
t
is a constant
c
∈
F
.
3. If a term
t
is
f
i
(t
1
,...,t
k
)
, where
f
i
∈ F
is a
k
-ary functional symbol and
I
T
(f
i
)(g
∗
(t
1
),...,g
∗
(t
k
))
.
We denote by
t/g
(or
φ/g
) the ground term (or formula) without free variables,
obtained by assignment
g
from a term
t
(or a formula
φ
), and by
φ
t
1
,...,t
k
are terms, then
g
∗
(f
i
(t
1
,...,t
k
))
=
the
formula obtained by uniformly replacing
x
by a term
t
in
φ
.A
sentence
is a
formula having no free variables. A Herbrand base of a logic
[
x/t
]
L
is defined by
={
|
r
i
∈R
}
H
r
i
(t
1
,...,t
k
)
and
t
1
,...,t
k
are ground terms
. We define the satisfac-
tion for the logical formulae in
L
and a given assignment
g
:
X
→
U
inductively, as
follows:
•
If a formula
φ
is an atomic formula
r
i
(t
1
,...,t
k
)
, then this assignment
g
satisfies
φ
iff
(g
∗
(t
1
),...,g
∗
(t
k
))
∈
I
T
(r
i
)
;
•
If a formula
φ
is a propositional letter, then
g
satisfies
φ
iff
I
T
(φ)
=
1;
•
φ
iff it does not satisfy
φ
;
•
g
satisfies
φ
∧
ψ
iff
g
satisfies
φ
and
g
satisfies
ψ
;
•
g
satisfies
¬
x
i
)φ
iff there exists an assignment
g
∈
U
X
that may differ from
g
g
satisfies
(
∃
X
, and
g
satisfies
φ
.
Aformula
φ
is
true
for a given interpretation
I
T
iff
φ
is satisfied by every assign-
ment
g
∈
U
only for the variable
x
i
∈
X
. A formula
φ
is
valid
(i.e., tautology) iff
φ
is true for every Tarski's
interpretation
I
T
∈
I
T
(for example,
r
and, for each propositional letter
p
∈
PR
,
∅
p
p
are valid). An interpretation
I
T
is a
model
of a set of formulae
Γ
iff every
formula
φ
∈
Γ
is true in this interpretation. We denote by FOL
(Γ )
the FOL with a
set of assumptions
Γ
, and by I
T
(Γ )
the subset of Tarski's interpretations that are
models of
Γ
, with I
T
(
⇒
=
I
T
. A formula
φ
is said to be a
logical consequence
of
Γ
, denoted by
Γ
φ
,iff
φ
is true in all interpretations in I
T
(Γ )
. Thus,
∅
)
φ
iff
φ
is
a tautology.
