Moving towards models: Kripke Semantics

To get the formal semantics of intuitionistic logic (and thus lambda calculus), we need a tool called Kripke Semantics. Kripke semantics is an amazing tool, which made it possible to define a lot of things in logics that weren't approachable before. In this post, I'm going to explain the basic ideas of Kripke semantics and how they're used for building models of logics; in my next post, I'll describe the Kripke semantics model for intuitionistic logic.

Modality

The basic idea of Kripe semantics is to associate the truth or validity of logical statements with something like a concept of time called a modality. In a modality, you have a set of states called worlds, with a transition relationship between them called accessibility. A world w assigns truth values to logical statements; and the accessibility relation defines what worlds can be reached from w. (For notation, we usually call the accessibility relation R, and write R(a,b) to mean that b is accessible from a.)

With modality, you have a new property in your logic: the truth value of statements can change when you transition from one world to another. To be able to talk about this, Kripke models have two modal operators that behave sort of like quantifiers over worlds.

1. L (also written as a square) for "necessarily": LP means that P is true in every possible world;
2. M (also written as a diamond) for "possible": MP means that P might be true in some world.
   

L and M are duals, very similar to a temporal version of "forall" and "exists". Just like "forall x : P(x)" is equivalent to "not exists x : not P(x)", Mp = not L not p.

Kripke Models

The semantics of Kripke models comes from the ability to make truth assignments; and truth assignments in turn come from something called a forcing relation. A world "w" in a Kripke semantics model forces statements in the logic if those statements are valid (provable) in that world. The forcing relation "w forces A" is usually written: "w ||- A". A valid forcing relation needs to have three properties:

1. w ||- not A if/f not(w ||- A): if w forces not A, then it cannot also force A.
   
2. w ||- A -> B if/f not(w ||- A) or (w ||- B). This is very close to one of the inference rules of normal predicate logic: A -> B if/f (not A) or B.
   
3. w ||- LA if/f forall u in W (R(w,u) implies u ||- A): we can say that a statement is necessarily true in a world w if and only if that statement is true in every world accessible from w.
   

With that, we've now got enough to be able to define what a model is in Kripke semantics: A Kripke model for a logic L consists of three things, usually written as a triple (W, R, ||-): W is a set of worlds; R is an accessibility relation between elements of W; and ||- is a forcing relation from members of W to statements in L. Without the forcing relation, given just the worlds and the accessibility relation, that piece of a model is called a Frame.

A logical statement or formula A is true in a model (W,R,||-) if forall w in W, w ||- A.

Building Kripke Models for Logics

Suppose we have a modal logic, X. What we want in a model for X is a way of saying what statements mean in a way that shows that they're consistent - that is, that the statements that are provable in the logic are really valid inferences from the axioms of the logic.

The basic construct of kripke models for logics is called maximum consistent sets. A set of statements S is consistent in a logic X if there is no way to derive a contradiction from any combination of statements in S, axioms of X, and standard inference (if A->B and A then B) over S and axioms of X. A maximum consistent set MCS for X is a consistent set for X where MCS is not a proper subset of any other consistent set in X.

The Kripke model of a logic X is a standard Kripke model (W,R,||-), where:

• W is the set of all MCSs for X.
  
• R(A,B) if/f for all statements s in X, (L s) in A implies s in B
  
• A ||- s if/f s in A
  

One incredibly cool property of the MCS construction of a Kripke model of a logic X is: for every statement s which can be shown to be unprovable in X, the Kripke model contains a counterexample. This will turn out to be really valuable in the model for intuitionistic logic: it means that in intuitionistic logic, we can enumerate the values for which a statement is true.