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:
(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 (R) "≤"; if A and B are worlds in W, then "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 pre-order relation - that is, a relation that has the essential properties of arithmetic "≤" 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.)

1. ∀w,u∈W such thatt 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.
2. ∀w∈W, w:-(A∧B) if/f w:-A and w:-B. "A∧B" is provable in w only if both A and B are provable.
3. ∀w∈W, w:-A∨B if/f w:-A or w:-B. "A∨B" is provable in w only if either A or B is probable in w.
4. ∀w*isin;W, w:-(A→B) if/f ∀u∈W 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.
5. There is no contradictory statement (written ⏊) such that w:-⏊.

The last line in there is actually a bit of a cheat: you can think of intuitionistic logic as a logic where at a given point of time, a statement can have three truth values: T (top), which means provably true; ⏊ (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 where: ∀w∈W: ∃!M_w∈M, where M_w is an L-structure for X. (An L-structure 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 and v are both worlds in W, and M_u and M_v are their corresponding L-structures, then:

1. if u≤v, then domain(M_u)⊆domain(M_v)
2. For any function f, in the logic, ∀a∈range(f) in M_u, f(a) in M_u = f(a) in M_v.
3. For any predicate P(a₁,a₂, ..., a_n), if P(a₁,a₂, ..., a_n) is true in M_u, then it is true in M>_v.

Now, finally, we can get to the last step in defining our model of intuitionistic logic: the forces relation based on M. What we need to do to make M work as a forces relation is to separate it into two parts: the truth/validity of concrete statements (that is, statements with all variables bound to specific values), which we write using the old forces notation, :-; 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:

1. w:-P(a₁,...a_n)[e] if/f
   P(a₁[e],...,a_n[e]) is in M_w: Evaluating a
   predicate means the same thing as keeping the predicate unchanged, and evaluating
   each of its parameters separately.
2. w:-(A ∧ B)[e] if/f w:-A[e] and w:-B[e]: a typical and definition.
3. w:-(A ∨ B)[e] if/f w:-A[e] or w:-B[e]: a typical or definition.
4. w:-(A → B)[e] if/f ∀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.)
5. w ¬:-⏊: no w can force a contradiction.
6. w:-(∃x:A)[e] if/f exists a∈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.
7. w:-(∀x:A)[e] if/f ∀u such that w≤u: ∀a∈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.

What we've done now is to define a way of describing the meaning of any statement in intuitionistic logic, and any reasoning step in intuitionistic logic in terms of sets, in a way where if we do the translation of the logical statement down to the sets, the statements about the sets will always be true and correct; and if we reason from the sets that correspond to the logic, anything we can do will produce a well-defined, meaningful, and valid statement in the logic.

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. In fact, the specific meaning of ¬A in this model of intuitionistic logic is that I have a concrete counterexample for A, so that A cannot be proven.

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.