1Proof theory and constructive logic
III Logic
1.3 Possible world semantics
For classical logic, semantics was easy. We had a collection of propositions
P
,
and a model is just a function
P → {>, ⊥}
. We can then define truth in this
model recursively in the obvious way.
It turns out to get a sensible model theory of constructive logic, we need to
consider many such objects.
Definition
(Possible world semantics)
.
Let
P
be a collection of propositions.
A world is a subset
w ⊆ P
. A model is a collection
W
of worlds, and a partial
order ≥ on W called accessibility, satisfying the persistence property:
– If p ∈ P is such that p ∈ w and w
0
≥ w, then p ∈ w
0
.
Given any proposition ϕ, we define the relation w ϕ by
– w 6 ⊥
– If ϕ is atomic (and not ⊥), then then w ϕ iff ϕ ∈ w.
– w ϕ ∧ ψ iff w ϕ and w ψ.
– w ϕ ∨ ψ iff w ϕ or w ψ.
– w ϕ → ψ iff (for all w
0
≥ w, if w
0
ϕ, then w
0
ψ).
We will say that w “believes” ϕ if w ϕ, and that w “sees” w
0
if w
0
≥ w.
We also require that there is a designated minimum element under
≤
, known
as the root world . We can think of a possible world model as a poset decorated
with worlds, and such a poset is called a frame.
All but the last rule are obvious. The idea is that each world can have some
beliefs, namely the subset
w ⊆ p
. The important idea is that if a world
w
does
not believe in
p
, it does not mean it believes that
p
is false. It just that
w
remains ignorant about whether p is true.
Now we have w
0
≥ w if w
0
a more knowledgable version of w that has more
beliefs. Alternatively,
w
0
is a world whose beliefs are compatible with that of
w
. It is easy to show by induction that if
ϕ
is any formula that
w
believes, and
w
0
≥ w
, then
w
0
also believes in
ϕ
. Then we can interpret the law of implication
as saying “
w
believes that
p → q
iff for any possible thinkable world where
p
is
true, then q is also true”.
Note that if we only have one world, then we recover models of classical logic.
What happens to negation? By definition, we have
w ¬A
iff
w A → ⊥
.
Expanding the definition, believing that
¬A
means there is no possible world
compatible with
w
in which
A
is true. This is much stronger than just saying
w 6 A, which just says we do not hold any opinion on whether A is true.
Example.
We want to construct a world
w
where
w 6 A ∨ ¬A
. So we need a
W such that w neither believes A nor believes ¬A.
We can achieve the former by just making the world not believe in
A
. To
make the world not believe
¬A
, it needs to be able to see a world
w
0
such that
w
0
A. So we can consider the following world:
w
0
A
w
6 A
Example.
This time consider the statement
w ¬¬A → A
. This takes some
work to unravel.
We need a world
w
such that for all
w
0
≥ w
, if
w
0
¬¬A
, then
w
0
A
. If
we unravel a bit more, we find that
w
0
¬¬A
means for any
w
00
≥ w
0
, we can
find some w
000
≥ w
00
such that w
000
A.
It is easy to see that actually in the model of the previous question,
w 6
¬¬A → A, since w ¬¬A, but w 6 A.
Example. The following model is a counter-model for ¬¬A ∨ ¬A:
6 A
A
6 A
where the bottom world believes in neither
¬¬A
nor
¬A
, since it sees worlds
where ¬A is true and also worlds where A is true.
Usually, we don’t talk about a particular world believing in something. We
talk about an entire structure of possible worlds believing something.
Notation. If the root world of our model is w, then we write
ϕ ⇐⇒ w ϕ.
Almost by definition, if ϕ, then for any world w
0
, we have w
0
ϕ.
Exercise. Find a possible world model that does not believe Peirce’s law.
One can readily verify that classically, we have (
A → B
)
→ B
is equivalent
to A ∨ B, but they are not constructively equivalent.
Exercise.
Find a possible world model that
(
A → B
)
→ B
, but does not
A ∨ B.
Exercise.
Find a possible world model that
(
A → B
)
→ B
but does not
believe (B → A) → A.
Exercise.
Find a possible world model that does not believe in
(
A → B
)
∨
(B → A).
Possible world semantics can be used for all sorts of logical systems, not just
propositional logic. In general, the notion of accessibility need not be a partial
order, but can be anything we want. Also, we do not necessarily have to require
persistence. Of course, we also need to modify the according notion of a world.
Example.
If we want to produce possible world semantics for constructive
first-order logic, we need to modify our definition of worlds so that they have
“elements”. Assuming we have done so, we can encode
∀
and
∃
using the following
rules:
– w ∃
x
, F (x) if there is some y ∈ w for which w F (y).
– w ∀
x
, F (x) if for all w
0
≥ w and x ∈ w
0
, we have w
0
F (x).
The second condition is much stronger than the naive “for all
x ∈ w
, we have
w F
(
x
)”, because the
w
00
≥ w
may have many more elements. What our
condition say is that
w
somehow has a “global” way of showing that everything
satisfies F .
Example. The proposition A → ¬¬A is valid all possible world models.
For classical logic, we had semantics given by truth tables. This easily shows
that classical truth is decidable. Similarly, given any formula, it involves only
finitely many variables, there are only finitely many distinct possible world
models one has to check. So whether something is refuted by possible world
models is again a decidable problem.
Now suppose we have a possible world model in front of us. Then given a
formula
ϕ
, the set of worlds that believe
ϕ
is an upward-closed subset of the
frame. So we can think of the truth value of ϕ as these upward-closed set.
Example. Suppose we have the following worlds:
w
2
w
1
Then the possible truth values are
∅, {w
2
}, {w
1
, w
2
}.
Suppose the top world believes
A
, but the bottom world does not. Then we say
that
A
has truth value
{w
2
}
. This is indeed the three-valued algebra we used to
disprove Peirce’s law.
What can we say about the collection of upward-closed subset of frames, i.e.
our truth values? Under inclusion, it is easy to see that these are complete and
co-complete, i.e. we have all infinite unions and intersections. More importantly,
we can do “implications”.
Definition
(Heyting algebra)
.
A Heyting algebra is a poset with
>
,
⊥
,
∧
and
∨ and an operator ⇒ such that A ⇒ B is the largest C such that
C ∧ A ≤ B.
If a poset is complete co-complete, then we would expect the implication to
be given by
A ⇒ B =
_
{C : C ∧ A ≤ B}.
Indeed, if the poset is a Heyting algebra, then it must be given by this. So we
just have to check that this works.
The thought is that Heyting algebras would “validate” all constructive theses,
by interpreting
∧
with
∧
,
∨
with
∨
and
→
with
⇒
. In other words, if we try to
build a truth table for a formula with values in a Heyting algebra, we will get
the top element
>
all the time iff the formula is constructively valid. So we have
a parallel between the relation between classical logic and boolean algebras, and
constructive logic and Heyting algebras.
It is an easy inductive proof that any constructively valid statement is “true”
in all Heyting algebras, and the other direction is also true, but takes more work
to prove.
Note that in classical logic, we only ever use the two-element boolean algebra.
If we use the 4-element Boolean algebra, then we would detect the same set of
tautologies. However, in the case of constructive logic we genuinely need all
Heyting algebras.
Finally, we prove half the completeness theorem for possible world models.
Lemma.
Any formula with a natural deduction proof not using the rule for
classical negation is true in all possible world models.
For any frame
F
, every such formula is satisfied by every possible world
model on that frame. We say it is valid on
F
. Such formulae are valid on all
posets with a bottom element.
Proof.
The hard case is implication. Suppose we have a natural deduction
proof of
A → B
. The last rule is a
→
-introduction. So by the induction
hypothesis, every world that believes
A
also believes
B
. Now let
w
be a world
that believes all the other undischarged assumptions in
A → B
. By persistence,
every
w
0
≥ w
believes similarly. So any
w
0
≥ w
that believes
A
also believes
B
.
So w A → B.