Information Technology Reference
In-Depth Information
f
(
a
)
,
g
(
a
,
b
)
,
f
(
g
(
a
,
b
))
,
g
(
a
,
f
(
a
))
,
f
(
g
(
a
,
f
(
a
)))
.
An equation such as
g
b
means that by applying the operation
f
to the
constant
a
, we get an element of
D
,say
c
, and by applying
g
to the pair
(
a
,
f
(
a
)) =
(
a
,
c
)
we
(
,
(
))
get
b
.Thismeansthat
g
is considered as the denotation of the element of
D
obtained by applying the operations according to the usual way algebraic expres-
sions are evaluated (in the order specified by parentheses). However, we can also
consider a term as an uninterpreted expression (a tree) constructed from constants,
operations, commas, and parentheses, disregarding its denotation. If we want to be
precise we write
g
a
f
a
(
a
,
f
(
a
))
to mean the element of
D
(if it exists) denoted by the
term, while we write
(or something analogous) to denote the uninter-
preted term. In formal logic this distinction is fundamental and a lot of different
terminologies are used to tell this intrinsic difference. Very often a denoting symbol
is said to be
used
while it is said to be
mentioned
when it refers to itself.
A
first-order logic signature
(FOL signature)
g
(
a
,
f
(
a
))
Σ
is a set of symbols for objects,
operations, and relations. A
-model is a relational structure where objects, opera-
tion and relations are denoted by the symbols of
Σ
Σ
.
We call
Term
(
Σ
)
the uninterpreted terms over the signature
Σ
,and
Term
V
(
Σ
)
the terms over the signature
Σ
and a set
V
of variables.
Terms over a signature
Σ
can be transformed into terms over a model when the
symbols of
are interpreted in the model.
We call
Term
V
(
M
)
Σ
the terms over the model
M
where variables
V
range over
the domain of
, where variables do not occur.
Atomic formulae
(over a signature) are expressions
R
M
,and
Term
(
M
)
the terms of
M
(
t
1
,
t
2
,...,
t
k
)
where
R
is a
k
-ary relation symbol and
t
1
,
t
k
are terms.
First-Order Logic
or FOL formulae are constructed by starting from atomic
formulae by using the First-Order Logical operators (FOL), which are:
1.
connectives
denoted by:
t
2
,...,
; respectively for
negation
(not),
con-
junction
(and),
disjunction
(or),
implication
(if),
equivalence
(iff), and
2.
quantifiers
denoted by
¬,∧,∨,→, ↔
∀
(for all), the
universal quantifier
,and
∃
(there exists),
the
existential quantifier
.
Let us associate connectives with the
boolean functions
described by their
truth
tables
defined by the following boolean equations:
•¬
1
=
0,
¬
0
=
1
•
(
1
∧
0
)=(
0
∧
1
)=(
0
∧
0
)=
0,
(
1
∧
1
)=
1
•
(
1
∨
0
)=(
0
∨
1
)=(
1
∨
1
)=
1,
(
0
∨
0
)=
0
•
(
0
→
1
)=(
1
→
1
)=(
0
→
0
)=
1,
(
1
→
0
)=
0
•
(
1
↔
1
)=(
0
↔
0
)=
1,
(
0
↔
1
)=(
1
↔
0
)=
0.
