Kripke ModelsFri, 23 Sep 2016 18:35:42 GMT

And again, a talk for the best mathematics club of the multiverse. This time, I thought I'd have a slightly more abstract topic, namely Kripke models. As always, this is not a scientific talk, and it focuses on breadth rather than depth, and neglects formality in favour of comprehensibility. Its audience will mainly consist of young students who will probably not have experience in mathematical logic for the largest part.

Anyway, feel free to drop a comment if you notice any mistakes.

A simply-typed lambda calculus

The lambda calculus is the prototype of all functional programming languages. We will give a short informal introduction to it.

A lambda term is inductively defined as

• There are variables, as the ones known from programming languages. Every variable is a lambda-term. Thus, is a lambda-term.
• If are lambda-terms, then the application is a lambda-term. It regards as a function, and as its first argument. A more usual notation would be , but there are reasons why is preferred.
• If is a lambda-term and is a variable, then the abstraction is a lambda-term. The variable will usually occur in . The intuition is that is the function that maps to some value the term , where every occurence of in is replaced by . For example, if , then . Another notation that is more common in some other parts of mathematics would be .

The idea of the untyped lambda calculus is that everything is a function. Functions map functions to functions. Lambda terms are the only objects one talks about.

A problem that arises from the above definition is that you might have a lambda term . If we just replaced , we would have , which is obviously not what we want. Actually, the inner is bound by the inner , and will not be replaced. It is possible to define this formally, but for this talk we just forbid that this occurs.

Another problem arises when we substitute with a term that itself contains a variable. Say, we have . This is obviously not intended, and we forbid this to happen, instead of handling it formally.

A variable is bound in a term, when it is captured by some lambda. It is free otherwise. A term is closed when it does not contain free variables. For example, contains freely, while is a closed term.

As for most functional programming languages, we can assign types to terms. In the simply-typed lambda calculus, there are atomic types and arrow types, which are of the form , where are types. Variables will be assigned a type. We write to denote that the term has the type . The intuition is that this term is a function from objects of type to objects of type . We therefore define the typing rule . Furthermore, we only allow applications when the types fit, that is, . Of course, we can leave out type annotations when they are clear or not important. This is a very simple type system, but most other type systems are based on this.

We now ask ourselves the question whether there is a closed term of type . Well, of course there is none, otherwise we wouldn't ask. Kripke models are a way of answering this kind of questions.

Kripke Models for the simply-typed lambda calculus

We are given a rooted tree , where is the set of nodes, and is the "is parent" relation for this tree. The tree need not be finite.

Now, for every atomic type , let a monotone function be given, that is, .

A triple is called a Kripke model (well, at least a very simple form of a Kripke model). We now define a so-called forcing relation (where is the set of simple types).

We define

• if and only if .
• if and only if for all , implies .

We say that (" models ") if and only if .

Lemma (Monotonicity): Let be a Kripke model, and with , and be some type. If , then .

Proof: We prove this by structural induction on . If for some atomic type , this holds by the monotonicity of .

Now Let , and assume , that is, for all , implies . But then the same holds especially forall , hence .

Q.E.D.

Lemma (Correctness): Let a closed simply-typed lambda term exist. Then every model satisfies .

Proof: We slightly generalize the Lemma. We actually prove: If there exists a term with free variables , then for every , if we have for all , we also have . We prove this by structural induction.

Our induction hypothesis is that the current entailment holds for all Kripke models. Notice that if , then is (trivially) also a Kripke model.

Obviously, it holds for variables .

Assume , where has the free variables and has the free variables (notice that both sets of free variables need not be disjoint). Assume that for all we have . Then by induction, we have and . But means that implies . Hence, the claim follows.

Assume , and . Besides , let have the free variables , and let again for all . We now have to show that implies for all . By our monotonicity lemma, implies . By our induction hypothesis for is that this holds for all Kripke models, especially for . Hence, for all , implies . Therefore, , and therefore, .

Q.E.D.

Now that we have shown correctness, we can answer our above question.

Lemma: There is no closed simply-typed lambda term of type .

Proof: Consider the tree of words matching the regular expression 0*1?. Define , and . That is:

                   ⋮
P→1 Q→0 001   000 P→0 Q→0
\ /
P→1 Q→0 01   00 P→0 Q→0
\ /
0 P→0 Q→0


Let for some node . That means that implies . For every , there is some such that but , and therefore , and therefore, . So for all , , and therefore, for all , regardles of whether or not . But then again, if , we have , so does not imply . Therefore, our Kripke model does not force . According to our correctness lemma, there cannot be a closed lambda term with this type.

Q.E.D.

This example is called the Peirce formula. You might wonder why this is interesting. In fact, it is just an introductory example. However, if you know functional programming languages, especially Scheme, you might be familiar with the concept of continuations. The type of call/cc is the Peirce formula. In Haskell's standard library, there is also a callCC routine with a similar type. However, this routine has a slightly different type: It uses the continuation translation of (see the type constructor cont). The reason is that Haskell is pure, and in a pure setting, it is not possible to derive the Peirce formula, which can be shown in a similar way as we just did.

Intuitionistic Propositional Logic

So far, our lambda terms only have atomic types and arrow types. We add a few new type constructors:

• If and are types, then so is , the product type (or pair type).
• If and are types, then so is , the sum type (or union type – it corresponds to unions in programming languages like C++).
• There is a distinguished type , the empty type or falsum. It must be impossible to create a closed term with this type.

There are additional axiomatic lambda terms for all types :

• Product type introduction : This term gets two arguments and returns their pair.
• Product type destruction : This term gets a term of the product type, and a term that maps the two elements of this pair to some other type, and returns this type. For example, the projection to the second coordinate of a pair is .
• Sum type introduction and .
• Sum type destruction . This corresponds to if … then … else ….
• Ex falso quodlibet: .

Except for the empty type, all of these are concepts that occur similarily in most modern programming languages, maybe written in a somewhat less intuitive way. We can give terms that do simple stuff like

From that perspective, empty types make no sense: They have no computational content. However, we can as well interpret these types as predicates: The atomic types become atomic predicates, will mean "or" , will mean "implies" , and will mean "and" . In this interpretation, is the predicate that is always wrong, and means "not ". We therefore define the abbrevitation . In this interpretation, closed lambda terms become formal proofs. For example, we can prove the introduction of contraposition:

However, the other direction cannot be derived. We can show this with a slightly extended definition of Kripke Models: We have to add interpretations for , and :

• not for all .
• if and only if and .
• if and only if or .

The above proof of correctness can be extended, but it is more technical. We will therefore not do this here. In this system, the Peirce formula is not derivable as well, as can be shown by the same Kripke model as above. Also, in the same Kripke model as above, contraposition and the law of excluded middle do not hold (exercise).

First-order Predicate Logic

We now extend our type system with objects and relations. We define a special type of objects. A relation is a "type with object arguments". For example, the set theoretic -relation is a relation with two object arguments. Remember, we are in metatheory, the object type is not specified and must be defined by axioms.

To get the full mathematical strength, we need to introduce quantors:

• means "for all objects , holds".
• means "there exists an object , such that holds".

The type is similar to , and is similar to , except that may depend on .

Introducing a universal quantifier is therefore done by abstraction , and it is eliminated by application .

The introduction of an existential quantifier reflects sum introduction: . Its elimination is where must not occur freely in .

We now have the full expressivity of first-order predicate logic. For example, we can prove :

However, as before the type system we just defined only allows for intuitionistic logic. The advantage of intuitionistic logic is that if you prove the existence of something, you get an algorithm that calculates it. The disadvantage is that things that cannot be calculated cannot be shown to exist. The following is the so-called Drinker formula (or Drinker problem, or sometimes Drinker paradox):

It is not derivable in intuitionistic logic. We can show this using a Kripke model, but we first have to extend our semantic:

Firstly, every node gets a domain of objects, such that . The relation now depends on an assignment , which is a function from object variables to elements of the domain of the corresponding node. For every relation with arguments, now, becomes a function . This corresponds to our former function in the sense that predicates become relations with zero arguments. We then say if and only if . For , the definition is similar to our former definition, where decomposes to and .

For the interpretation of the quantors, we must define , which is , except for the variable , where it is :

• if and only if there exists an such that .
• if for all , for all , .

We again omit the correctness proof. But we show that the Drinker formula cannot be derivable. We set with the canonical ordering. We set and for . (This model is taken from here.)

⋮
3 D={0,1,2,3} b={0→1,1→1,2→1,3→0}
|
2 D={0,1,2} b={0→1,1→1,2→0}
|
1 D={0,1} b={0→1,1→0}
|
0 D={0} b={0→0}


We set . Obviously, if , then . However, , but . Therefore, .

Similar Concepts

Beth Models

A similar concept for first-order logic you might see is the concept of Beth models. Their definition is slightly different but similar, and their properties are similar. See here for example.

Presheaf Models

There is a generalization of Kripke models, the so-called presheaf models. Here, the domains are given by a presheaf on a category .

For every relation with arguments and every object from we have an interpretation such that if there is a morphism in , we have . An assignment is, as before, a map from variable symbols into objects. The definition is now similar to the one for Kripke models: For relations, we define . For implications we define if and only if for every morphism , implies .

It is also possible to define this (even more general) in terms of morphisms between classical models instead of explicitly giving interpretations for all relations and domains. You might also find a more intricate version of implication for arrow types, a version that includes computational content, as an interpretation of type theory.

A Kripke model is a special case where is a poset.

Semantic Forcing in Set Theory

The following part is kept very short and only for older audiences. Paul Joseph Cohen proved that the continuum hypothesis is independent of Zermelo-Fraenckel Set Theory (ZFC). He uses a concept inspired by Kripke models. We will only look at the parts related to Kripke models here. For an explanation of the proof see here, here and here.

This is a relative consistency result, so we can assume that there is a classical transitive countable model of ZFC. (It can be proved that the existence of such a set is unprovable, by Gödel's second incompleteness theorem.)

That is a set for which the ZFC axioms hold when relativizing all quantors to it (that is, replacing with , etc). Transitivity means that . This can be proved by the Löwenheim-Skolem theorem and the Mostowsky collapse lemma.

We write if the formula holds in when relativizing all quantors to it. Notice that we already used the character for Kripke models. It is generally used for semantic entailment. is a so-called classical model, while Kripke models are intuitionistic models.

A forcing poset is a triple completely defined in where is a preorder with the largest element and the splitting condition that for all there exist such that there is no , that is, they form no diamond, that is, the ordering is similar to a tree.

A -name is, roughly speaking, a set with an element of attached, in which every element itself is a -name. That is, for example, for .

We define , the valuation map.

We now define

where is the set of -names in . We now define a forcing relation on elements of .

• .
• .
• .
• .

One can show that if satisfies some conditions, holds there is a such that .