Database Reference
In-Depth Information
Each theorem
φ
obtained from the axioms (1 through 11), and by Modus Ponens
(MP) and Substitutions inference rules, is denoted by '
IL
φ
'. We denote by
IPC
the set of all theorems of IL, that is,
IPC
(the set of formulae closed
under MP and substitution) and, analogously, by
CPC
the set of all theorems of
CPL.
We introduce an
intermediate logic
(a consistent superintuitionistic logic) such
that a set
L
of its theorems (closed under MP and substitution) satisfies
IPC
={
φ
|
IL
φ
}
⊆
L
⊆
CPC
. For every intermediate logic
L
and a formula
φ
,
L
+
φ
denotes the smallest
intermediate logic containing
L
∪{
φ
}
. Then we obtain
CPC
=
IPC
+
(φ
∨¬
φ)
=
IPC
+
(
¬¬
φ
⇒
φ).
The topological aspects of intuitionistic logic (IL) were discovered independently
by Alfred Tarski [
75
] and Marshall Stone [
74
]. They have shown that the open sets of
a topological space form an “algebra of sets” in which there are operations satisfying
laws corresponding to the axioms of IL.
In 1965, Saul Kripke published a new formal semantics for IL in which IL-
formulae are interpreted as upward-closed hereditary subsets of a partial order-
ing
(W,
≤
)
. More formally, we introduce an
intuitionistic Kripke frame
as a pair
F
=
and
R
is a binary relation on a set
W
, exactly a partial
order (a reflexive, transitive and anti-symmetric relation). Then we define a subset
S
(W,R)
, where
W
=∅
⊆
W
, called an
upset
of F if for every
a,b
∈
W
,
a
∈
W
and
(a,b)
∈
R
imply
b
S
. Here we will briefly present this semantics, but with a semantics equivalent
(dual) to it, based on downward-closed hereditary subsets of
W
, where a subset
S
∈
⊆
W
is hereditary in
W
if we have:
whenever
a
∈
S
and
b
≤
a,
then
b
∈
S
≤
−
1
). The collection of
hereditary subsets of
W
will be denoted by
H(W)
. A valuation
V
(that is, when
S
is an upset for the binary relation
R
equal to
H(W)
,
for a set
PR
of propositional symbols of IL, is a mapping which assigns to each
propositional symbol
p
:
PR
→
∈
PR
a hereditary subset
V(p)
∈
H(W)
. A Kripke model
on the set of “possible worlds” in
W
is a pair
M
=
(
F
,V)
where
V
is a valuation
and F
=
(W,R)
a Kripke frame with
R
=≤
−
1
) such that
V(p)
is
the set of all possible worlds in which
p
is true. The requirement that
V(p)
be
downward hereditary formalizes (according to Kripke) the “persistence in time of
truth”, satisfying the condition:
a
(i.e.,
R
=≥
V(p)
.
We now extend the notion of truth at a particular possible world
a
∈
V(p)
and
(a,b)
∈
R
implies
b
∈
∈
W
to all IL
formulae, by introducing the expression
M
|=
a
φ
, to be read “a formula
φ
is true in
M
at
a
”, defined inductively as follows:
1.
M
|=
a
p
iff
a
∈
V(p)
;
2.
M
|=
a
φ
∧
ψ
iff
M
|=
a
φ
and
M
|=
a
ψ
;
3.
M
|=
a
φ
∨
ψ
iff
M
|=
a
φ
or
M
|=
a
ψ
;
4.
M
|=
a
φ
⇒
ψ
iff
∀
b(a
≥
b
implies
(
M
|=
b
φ
implies
M
|=
b
ψ))
;
5.
M
|=
a
¬
φ
iff
∀
b(a
≥
b
implies not
M
|=
b
φ)
.
