Database Reference
In-Depth Information
The basic set of axioms of the FOL are that of the propositional logic CPL with
two additional axioms:
(A1)
(
∀
x)(φ
⇒
ψ)
⇒
(φ
⇒
(
∀
x)ψ)
(
x
does not occur in
φ
and it is not bounded
in
ψ
), and
(A2)
(
∀
⇒
[
]
(neither
x
nor any variable in
t
is bounded in
φ
).
For the FOL with identity, we need the
proper
axiom
(A3)
x
1
.
x)φ
φ
x/t
(x
1
.
x
2
.
x
3
)
.
We denote by
R
=
the Tarski's interpretation of identity
=
x
2
⇒
=
x
3
⇒
=
.
=
r
=
I
T
(r
)
is the
built-in
identity relation (equal for any Tarski's interpretation), with,
for example,
, that is,
R
=
=
.
The inference rules are Modus Ponens and generalization (G) “if
φ
is a theorem
and
x
is not bounded in
φ
, then
(
0
,
0
,
1
,
1
∈
R
=
∀
x)φ
is a theorem”.
In what follows, any open-sentence, a formula
φ
with nonempty tuple of free
variables
x
will be called an
m
-ary
virtual predicate
, denoted also
by
φ(x
1
,...,x
m
)
or by
φ(
x
)
. This definition contains the precise method of estab-
lishing the
ordering
of variables in this tuple. The method that will be adopted here
is the ordering of appearance, from left to right, of free variables in
φ
. This method
of composing the tuple of free variables is a unique and canonical way of defining
the virtual predicate from a given formula. The FOL is considered as an extensional
logic because two open-sentences with the same tuple of variables
φ(x
1
,...,x
m
)
and
ψ(x
1
,...,x
m
)
are
equal
ifftheyhavethe
same extension
in a given inter-
pretation
I
T
,thatis,iff
I
T
(φ(x
1
,...,x
m
))
=
x
1
,...,x
m
I
T
(ψ(x
1
,...,x
m
))
, where
I
T
=
is the
unique extension of
I
T
to all formulae, as follows:
1. For a (closed) sentence
φ/g
,
I
T
(φ/g)
=
1iff
g
satisfies
φ
, as recursively defined
above.
2. For an open-sentence
φ
with the tuple of free variables
x
1
,...,x
m
,
I
T
φ(x
1
,...,x
m
)
=
def
g(x
1
),...,g(x
m
)
|
1
.
X
and
I
T
(φ/g)
∈
U
=
g
It is easy to verify that for a formula
φ
with the tuple of free variables
x
1
,...,x
m
,
I
T
φ(x
1
,...,x
m
)/g
=
1 f
g(x
1
),...,g(x
m
)
∈
I
T
φ(x
1
,...,x
m
)
.
1.3.1 Extensions of the FOL for Database Theory
One of the most important issues of mathematical logic is that our understanding of
mathematical phenomena is enriched by elevating the languages we use to describe
mathematical structures to objects of explicit study. It is this aspect of logic which is
most prominent in model theory which deals with the relation between a formal lan-
guage and its interpretations. The specialization of model theory to finite structures
should find manifold applications in computer science, particularly in the frame-
work of specifying programs to query databases: phenomena whose understanding
requires close attention to the interaction between language and structure. Beginning
with connection to automata theory, the
finite model
theory has developed through a
range of applications to problems in graph theory, database and complexity theory
and artificial intelligence.
