Database Reference
In-Depth Information
Given a set of formulae
Δ
and a formula
φ
,for
IPC
(as for
CPC
) the Deduction
theorem is valid: if
Δ,φ
ψ
.A
theory
is a set of formulae
Δ
that is closed under
IPC
-consequence. A set of formulae
Δ
has the
disjunction
property
if
φ
IL
ψ
then
Δ
IL
φ
⇒
Δ
.
The method of canonical models used in modal logics can be adapted to the
case of intuitionistic logic. Instead of considering the maximal consistent sets of
formulae, we consider theories with the disjunction property. The
canonical model
(or Henkin model) of
IPC
is a Kripke model
∨
ψ
∈
Δ
implies
φ
∈
Δ
or
ψ
∈
C
(
F
C
,V)
based on a frame F
C
=
(W
C
,R
C
)
, where the set of possible worlds
W
C
is equal to the set of all consistent
theories with the disjunction property, and the binary accessibility relation
R
C
M
=
⊂
W
C
W
C
H(W
C
)
on F
C
×
is the inclusion. The canonical valuation
V
:
PR
→
is
W
C
,
Δ
C
defined by putting for each
Δ
Δ
.
The point of completeness proof lies in showing that, for each formula
φ
and
each
Δ
∈
∈
V(p)
(i.e.,
M
|=
Δ
p
)iff
p
∈
W
C
,
C
C
∈
M
|=
Δ
φ
)iff
φ
∈
Δ
, or in a different notation,
M
|=
Δ
φ
)iff
Δ
∈
V(φ)
.
The canonical frame F
C
is isomorphic to the frame
(
H
IL
)
∗
obtained from the
Lindenbaum-Tarski quotient Heyting algebra
H
IL
=
(
IPC
IL
,
,
,
,,
¬
)
(in-
∼
troduced in Sect.
1.2
), with a mapping
σ
:
W
C
∼
IL
defined for each consis-
tent theory (with disjunction property)
Δ
∈
W
C
,
F
=
σ(Δ)
={[
φ
]|
φ
∈
Δ
}
→
IPC
. In fact,
F
is a prime filter:
1. If
φ,ψ
∈
Δ
(i.e.,
[
φ
]
,
[
ψ
]∈
F
) then
φ
∧
ψ
∈
Δ
(i.e.,
[
φ
][
ψ
]=[
φ
∧
ψ
]∈
F
);
2. If
φ
∈
Δ
(i.e.,
[
φ
]∈
F
) and
IL
φ
⇒
ψ
(i.e.,
[
φ
][
ψ
]
) then (by MP)
ψ
∈
Δ
[
]∈
(i.e.,
ψ
F
);
∨
∈
[
][
]=[
∨
]∈
∈
∈
[
]∈
3. If
φ
ψ
Δ
(i.e.,
φ
ψ
φ
ψ
F
) then
φ
Δ
or
ψ
Δ
(i.e.
φ
F
[
]∈
F
).
The complex Heyting algebra of this frame is
F
C
∗
=
H
W
C
,
or
ψ
,W
C
,
⊆
,
∩
,
∪
,
⇒
h
,
¬
h
,
∅
which, in the case when
PR
is an infinite set, is an infinite complete Heyting alge-
bra. It is well known that a canonical model is complete for
IPC
(that is,
IL
φ
iff
[
is valid in
H
IL
).
Another example of single infinite complete Heyting algebra which is complete
for
IPC
is given by well known topological interpretation of
IPC
based on the
family of open sets
φ
]
O
(W)
(which generalize the power-set of
W
).
A pair
(W,
O
(W))
is called a
topological space
if
W
=∅
and
O
(W)
is the set of
subsets of
W
such that
∅
,W
∈
O
(W)
and:
1. If
V
1
,V
2
∈
O
(W)
then
V
1
∩
V
2
∈
O
(W)
; (finite intersection closure)
, then
i
∈
N
2. If
V
i
∈
O
(W)
, for every
i
∈
N
V
i
∈
O
(W)
. (infinite union closure).
For example, when
W
is a set of real numbers
R
,
O
(
R
)
is the family of all open sets
of real numbers. We denote by
φ
the open set of
R
assigned to a formula
φ
,so
that we obtain a valuation
_
:
PR
→
O
(
R
)
extended inductively for all formulae
by:
1.
φ
∧
ψ
=
φ
∩
ψ
;
2.
φ
∨
ψ
=
φ
∪
ψ
;
