Kripke Semantics and Models for Intuitionistic Logic

To be able to really talk about what a logic (or a calculus) means, you need to
define a model of that logic. A model is a way of associating entities in the
logic/calculus with some kind of real entity in a way where all statements in the logic about
the logical entity will also be true about the real-world entity. Models are incredibly
important, because it's relatively easy to design a logic which looks as if
it's perfectly valid, but which contains some subtle error which leads to it being
essentially meaningless - showing a model for a logic guarantees that that can't happen.

The model for intuitionistic logic is based on something called Kripke Semantics. Kripke semantics is an amazing tool, which make 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.

The basic idea of Kripke semantics is to associate the truth or validity of logical statements with something like a concept of time called a modality (which is very closely related to the idea of modal logics). In a modality, you have a set of states called worlds, with a transition relationship between them called an accessibility relation. 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. These should look familiar from the modal logic posts.

• L (also written as a square) for "necessarily": LP means that P is true in every possible world;
• 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 "∀" and "∃". Just like "∀ x : P(x)" is equivalent to "¬∃x:¬P(x)", in Kripke semantics MP≡¬L¬P.

Kripke models of logics are built from truth assignments; and in turn, truth assignments are derived from something called a forcing relation. Suppose you have a
world w in a Kripke semantics model. The forcing relation for w
forces statements in the logic if those statements are valid (provable) in that world. The forcing
relation is generally written ":-" as in "w :- A" to mean "the world w forces the statement A".

A valid forcing relation needs to have three properties:

1. w :- ¬ A ⇔ ¬(w :- A): if w forces not A, then it cannot also force A.
2. w :- A→B ⇔ ¬(w:-A) or (w :- B). This is very close to one of the inference rules of normal predicate logic: "A→B &har; (¬A)∨B".
3. w :- LA ⇔ ∀u∈W:(R(w,u) ⇒ 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 consists of three things, usually written as a triple (W, R, :-): W is the set of all possible worlds for the logic; R is an accessibility relation between elements of W; and ":-" is a forcing relation from members of W to statements in the logic. 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 ∀ w∈W, w:-A.

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 the logic X
• R(A,B) if/f for all statements s∈X, (Ls)∈A implies s∈B
• ∀A∈R, A:-s if/f s∈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.

Anyway, I think this is enough for today. Tomorrow, we'll get to an actual Kripke model for intuitionistic logic.