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
  • AR, 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.

0 thoughts on “Kripke Semantics and Models for Intuitionistic Logic

  1. Jonathan Vos Post

    Slightly different branch of Logic; feel free to move this to another thread.
    Over on Ars Mathematica, Walt says (in part):
    Paul Cohen, 1934-2007
    March 25th, 2007 by Walt
    http://www.arsmathematica.net/archives/2007/03/25/paul-cohen-1934-2007/#comments
    Alexandre Borovik is reporting that Paul Cohen has died. Cohen of course proved that the continuum hypothesis is independent of the axioms of set theory, and that the axiom of choice was independent of the other axioms.
    Gödel had already established that both the continuum hypothesis and axiom of choice were consistent, in the sense if you could derive a contradiction by adding them as axioms then you could derive a contradiction in set theory without them. Gödel accomplished this by defining a certain minimal model of set theory, the constructible universe, and showing that in this model both axioms hold. Cohen then completed the proof of independence by showing that you can construct a model of set theory in which both axioms are false. To do so, he had to invent a new technique: forcing.

    Reply
  2. Bryson Brown

    Mark–
    Just a typo, reallly, but in the canonical model you describe, the third condition must be for A memb W, not A memb R. I assume you’re going to connect this to the completeness result(s) next…

    Reply
  3. Ken Hirsch

    Shouldn’t

    MP means that P might be true in some world.

    read

    MP means that P is true in some world.

    Reply
    1. Michał

      I was thinking about same think and it is look like it is true because of analogy between L and “for all” and M and “exists”.

      Reply
  4. Chad Groft

    Is Paul Cohen’s forcing the same forcing as in the main body of this post?

    It can be seen as a very special case of it, yes. However, it’s not really the best way to approach the question, and Cohen himself was unaware of the connection until fairly recently. (He wasn’t really a logician by trade; he didn’t really even keep up with all the applications of forcing after a couple of years.)
    This Sunday I wrote Mark an email about a possible series of articles on the subject, in honor of Cohen’s passing, but have yet to hear back from him on it (for very good reasons, from what he’s said on the blog). Until I do, I don’t want to go into huge amounts of detail in the comments.

    Reply

Leave a Reply