Finally: the Kripke Model for Intuitionistic Logic
As promised, today, I'm going to show the Kripke semantics model for intuitionistic logic.
Remember from yesterday that a Kripke model has three parts:
To model intuitionistic logic, we need to add some required properties to the transition and forcing relations. With these additional properties, we call the transition relation "<="; "A <= B" means that B is accessible from A. For an intuitionistic Kripke model, the transition relation "<=" must be both reflexive (A <= A) and transitive (if A <= B and B <= C, then A <= C), making it a preorder relation  that is, a relation that has the essential properties of "<=" that is necessary to define a partial order over its domain. The forces relation, "
So: suppose we have an intuitionistic logic consisting of a set of statements, which we'll call X. The Kripke model for X is the triple
So: given an evaluation
The particularly nice thing about an intuitionistic logic with a Kripke model is that for any statement which is provably true, we can use the model to find specific values for the variables in the statement for which its true; and if a statement is false, we can find specific values for the variables in the statement that produce a concrete counterexample. We can't always do that in regular predicate logic: regular predicate logic allows us to do inferences from things like "exists" statements if we know that some value must exist for which the statement is true, even if there's no way for us to figure out what that value is. Likewise, in regular predicate logic, we can infer that a forall statement is false if we know that there must be some value for which it's false; in intuitionist logic, we need to be able to show a specific example for which it's false.
Remember from yesterday that a Kripke model has three parts:
(W, R, )
, where W is a set of worlds; R is a transition relation between worlds; and "" is a forces relation that defines what's true in a particular world.To model intuitionistic logic, we need to add some required properties to the transition and forcing relations. With these additional properties, we call the transition relation "<="; "A <= B" means that B is accessible from A. For an intuitionistic Kripke model, the transition relation "<=" must be both reflexive (A <= A) and transitive (if A <= B and B <= C, then A <= C), making it a preorder relation  that is, a relation that has the essential properties of "<=" that is necessary to define a partial order over its domain. The forces relation, "

" also needs some additional conditions: (these conditions are based on the definitions from the wikipedia article on Kripke models; I can't remember them without help, so I used the article as a reference.)
for all w,u in W such that w <= u, for all statements s if w  p, then u  p
. This condition basically says that if a statement is true/valid in a particular world w, then it must be true in all worlds accessible from w  meaning that in intuitionistic logic, once a statement is proven, it can't be taken back.

for all w in W, w  A and B if/f w  and w  B
. "A and B" is provable in w only if both A and B are provable.

for all w in W, w  A or B if/f w  A or w  B
. "A or B" is provable in w only if either A or B is probable in w.

w  A implies B if/f for all u such that w <= u, (u  A) implies (u  B)
. Being able to prove that "A implies B" in w means that in every world accessible from w, if you can prove A, then you can prove B.
 There is no contradictory statement (written __) such that
w  __
.
__
(bottom) which means provably false, and unproved. The last property of the forces relationship means that under no conditions can the "forces" relation say that a proposition is true if it is provably false.So: suppose we have an intuitionistic logic consisting of a set of statements, which we'll call X. The Kripke model for X is the triple
(W, <=, M)
, where W is the set of worlds related by a "<=" relation that has the intuitionistic properties that we just discussed. M
is a set of sets: for all w in W: exists one M_w in M
, where M_w is an Lstructure for X. (An Lstructure is a formal way of defining what statements are proved true  and for statements with variables, the bindings of those variables to values for which the statement has been proved true. For the purposes of understanding, you can think of M_w as a function that takes a logical statement, and a list of values for the variables in that statement, and returns "true" if the statement is proved true, and false if the statement is proved false; and the statement is not in the domain of the function if it's truth value hasn't been proved.) The M_w's for intuitionistic logic have a set of properties that come from the meaning of statements in the logic: if
u <= v
, thendomain(M_u) subset domain(M_v)
 For any function f, in the logic,
for all a in domain(f) in M_u, f(a) in M_u = f(a) = M_v
.
 For any predicate
P(a_1,a_2, ..., a_n)
, ifP(a_1,a_2, ..., a_n)
is true in M_u, then it is true in M_v.

; and the mapping of variables and functions to values. We call that mapping an evaluation function; for a statement A in X, we write A[e] for A with variables bound by e.So: given an evaluation
e
of variables from M_w, w  A[e]
is defined by:
w  P(a_1,...a_n)[e] if/f P(a_1[e],...,a_n[e])
is inM_w
: Evaluating a predicate means the same thing as keeping the predicate unchanged, and evaluating each of its parameters separately.

w  (A and B)[e] if/f w  A[e] and w  B[e]
: a typical and definition.

w  (A or B)[e] if/f w  A[e] or w  B[e]
: a typical or definition.

w  (A implies B)[e] if/f forall w <= u: u  A[e] implies u  B[e]
: an implication is true if, in the model, you can prove its constituents in the next step. (This is the opposite of its definition in the logic: in logic, we'd say that given A implies B and A, you can conclude B. In the model, we go the other way, and say that you can conclude that A implies B if, for all possible transitions, the next world allows you to conclude either A or not B.)

w NOT  __
: no w can force a contradiction.

w  (exists x : A)[e] if/f exists a in M_w such that w  A[e], and e maps x to a
. An exists statement is provable only if we can show a concrete, specific value for which the statement is true.

w  (forall x : A)[e] if/f forall u such that w <= u: forall a in M_u: u  A[e] where e maps x to A
: a universal statement is provable if every possible next world can prove that the statement with all possible bindings of variables are true.
The particularly nice thing about an intuitionistic logic with a Kripke model is that for any statement which is provably true, we can use the model to find specific values for the variables in the statement for which its true; and if a statement is false, we can find specific values for the variables in the statement that produce a concrete counterexample. We can't always do that in regular predicate logic: regular predicate logic allows us to do inferences from things like "exists" statements if we know that some value must exist for which the statement is true, even if there's no way for us to figure out what that value is. Likewise, in regular predicate logic, we can infer that a forall statement is false if we know that there must be some value for which it's false; in intuitionist logic, we need to be able to show a specific example for which it's false.
2 Comments:
"In the model, we go the other way, and say that you can conclude that A implies B if, for all possible transitions, the next world allows you to conclude either A or not B." Surely the last bit should read "not A or B"?
And don't you need a definition for w  NOT A[e]?
(I'm a bit groggy right now, so it's possible I'm missing something.)
By Adam, at 5:25 PM
adam:
Yes, you're right  it should be "not A or B", instead of "A or not B".
For question about forcing not: remember that in intuitionistic logic, "not B" means "I can prove that there is no proof of B"; and that the fact that there is no proof of a statement can only be done by creating a positive instance  that is, a provable statement that implies the falsehood of B. So you only need the positive rules, plus the fact that you can't force a contradiction.
By MarkCC, at 7:06 PM
Post a Comment
<< Home