Database Reference
In-Depth Information
where for any two equivalence classes
[
φ
]
,
[
ψ
]∈
IPC
∼
IL
,
[
φ
][
ψ
]
iff
IL
φ
⇒
ψ
,
with
[
][
][
∧
]
[
][
][
∨
]
φ
ψ
φ
ψ
,
φ
ψ
φ
ψ
,
[
φ
]
[
ψ
][
φ
⇒
ψ
]
,
¬[
φ
][¬
φ
]
.
Then the valuation
v(φ)
=[
φ
]
can be used to show
IL
φ
iff
H
IL
|=
φ
, hence any
HA
-valid sentence will be
H
IL
-valid and so an IL-theorem.
We can extend the algebraic semantics of
IPC
to all intermediate logics. With
every intermediate logic
L
IPC
we associate the class
V
L
of Heyting algebras
in which all the theorems of
L
are valid. It is well known that
V
L
is a variety. For
example,
V
IPC
=
HA
⊇
denotes the variety of all Heyting algebras. For every variety
V
HA
=
IPC
. The Lindenbaum-Tarski construction shows that every intermediate logic is
complete w.r.t. its algebraic semantics. In fact, it was shown that every intermediate
logic
L
(an extension of
IPC
) is sound and complete w.r.t. the variety
V
L
.
⊆
HA
,
let
L
V
be the logic of all formulae valid in
V
, so that, for example,
L
1.3
Introduction to First-Order Logic (FOL)
We will shortly introduce the syntax of the First-order Logic language
,asan
extension of the propositional logic, and its semantics based on Tarski's interpreta-
tions:
L
Definition 1
The syntax of the First-order Logic (FOL) language
L
is as follows:
•
Logical operators
(
∧
,
¬
,
∃
)
over the bounded lattice of truth values
2
={
0
,
1
}
,0
for falsity and 1 for truth;
•
Predicate letters
r
1
,r
2
,...
with a given finite arity
k
i
=
ar(r
i
)
≥
1,
i
=
1
,
2
,...
in
R
;
•
Functiona
l
l
et
ters
f
1
,
f
2
,...
with a given arity
k
i
=
(language
constants 0
,
1
,...,c,d,...
are considered as a particular case of nullary func-
tional letters);
ar(f
i
)
≥
0in
F
•
Variables
x,y,z,...
in
X
, and punctuation symbols (comma, parenthesis);
•
Aset
PR
, with
truth r
∅
∈
PR
∩R
, of propositional letters (nullary predicates);
•
The following simultaneous inductive definition of
term
and
formulae
:
1. All variables and constants are terms. All propositional letters are formulae.
2. If
t
1
,...,t
k
are terms and
f
i
∈F
is a k-ary functional symbol then
f
i
(t
1
,...,t
k
)
is a term, while
r
i
(t
1
,...,t
k
)
is a formula for a k-ary predicate letter
r
i
∈R
.
¬
φ
, and
(
∃
x
i
)φ
for
x
i
∈
X
are formulae.
An interpretation (Tarski)
I
T
consists of a nonempty domain
3. If
φ
and
ψ
are formulae then
(φ
∧
ψ)
,
U
and a mapping that
assigns to any predicate letter
r
i
∈R
with
k
=
ar(r
i
)
≥
1, a relation
r
i
=
I
T
(r
i
)
⊆
k
, to any k-ary f
u
nctional letter
f
i
∈ F
k
U
a fun
ct
ion
I
T
(f
i
)
:
U
→
U
, to e
ac
h in-
dividual constant
c
∈
F
one given element
I
T
(c)
∈
U
, with
I
T
(
0
)
=
0
,I
T
(
1
)
=
1
for natural numbers
N
={
0
,
1
,
2
,...
}
, and to any propositional letter
p
∈
PR
one
truth value
I
T
(p)
. We assume the countable infinite set of Skolem
constants (marked null values)
SK
={
ω
0
,ω
1
,...
}
∈
2
={
0
,
1
}⊆
N
to be a subset of the universe
U
.
