Lately, I have been thinking a lot about Kripke models of intuitionistic propositional logic for my research. During this time I also played around a bit with the models. Here I would like to write down some of the stuff I played with.
Def. 1. A Kripke model is a tuple \(M = \langle W , \preceq , \mathcal{V} \rangle \), where \(W\) is a non-empty set of objects called worlds, \(\preceq \) is a binary relation on \(W\), and \( \mathcal{V} \) is a unary relation between worlds and sets of atomic propositions. This model has the following conditions:
- \( \preceq \) is a preorder, and
- (Hereditary Condition) For every atomic formula \(p\) and worlds \(w\) and \(w’\), if \(w \leq w’\) and \(p \in \mathcal{V}(w)\), then \(p \in \mathcal{V}(w’)\).
We call the tuple \( F = \langle W, \preceq \rangle\) a Kripke frame.
Categorizing Kripke
Kripke frames are simply preordered sets. Thus, they are categories.
Lemma. 1. Suppose \(F = \langle W, \preceq \rangle\) is a Kripke frame. Then \(F\) is a category.
Proof. Simply take \(W\) as the set of objects. An arrow exists between two worlds \(w\) and \(w’\) if and only if \(w \preceq w’\). Then identity arrows exist by reflexivity of \(\preceq\) and composition is defined using transitivity. It is easy to see that left and right identities behave correctly and composition is associative. \( \Box\)
We denote the category of a Kripke frame \(F\) as \(Cat(F)\). A Kripke model is then a Kripke frame together with an interpretation function \( \mathcal{V} \) from the set of worlds to a set of atomic propositions. We can interpret a model as \(Cat(F)\) for some Kripke frame \(F\) together with the following functor (\(\mathcal{\subseteq}: Cat(F) \to Set\)):
- \( \mathcal{\subseteq}(w) = A\), for some set \(A\) of atomic propositions, and
- \(\mathcal{\subseteq}(f : w \to w’) = g : \mathcal{\subseteq}(w) \to \mathcal{\subseteq}(w’)\), where \(p = g(p)\) (if \(p \in \mathcal{\subseteq}(w)\) then \(p \in \mathcal{\subseteq}(w’)\)).
Therefore, a Kripke model is then the tuple \(\langle Cat(F), \mathcal{\subseteq}\rangle\).
What about the category of Kripke models?
Def. 3. The category of Kripke models, \( Kat \), is defined as follows:
- Objects: The Set of all Kripke models.
- Arrows: The set of homomorphisms from the Kripke frame of one model to the Kripke frame of another. That is for models \(M_1 = \langle W_1,\preceq_1,\mathcal{V}_1\rangle\) and \(M_2 = \langle W_2,\preceq_2,\mathcal{V}_2\rangle\) the arrow from \(M_1\) to \(M_2\) is a homomorphism from \(W_1\) to \(W_2\) such that the preorder structure is preserved.
- Identities: Clearly, identities exists, just take the trivial homomorphism.
- Composition: Homomorphisms are composable, and they respect identities and associativity.
So that is the definition using Def. 1, lets try and give one interms of pure categories. Since a functor is a generalization of a homomorphism between categories we simply move from the arrows being homomorphisms in \(Set\) to functors.
Def. 3. The category of Kripke models, \( Kat_{Cat} \), is defined as follows:
- Objects: The set of all Kripke models \(M = \langle Cat(\langle W, \preceq \rangle),\subseteq\rangle \).
- Arrows: The set of functors between frames.
- Identities: Take the identity functors \( \mathcal{I}_{M} \) for any model \(M\).
- Composition: Composition is well defined for functors. Identities play nice and composition is associative.
Frame it!
We can eliminate the pesky functor \(\subseteq\) and the interpretation mapping \(\mathcal{V}\) all together. Instead of leaving the worlds unspecified we can adopt sets of atomic propositions as worlds. Doing this results in Kripke frames becoming Kripke models. Intuitionistic logic can be interpreted in this configuration in the usual way except instead of interrupting atomic propositions as members of the interpretation of a world they are actual members of the world. Some may have philosophical objections to this style, because the semantics is not completely distinct from the object language, but I do not think this is that far off base from the semantics of type theories. There we interpret types as sets of normal forms which are members of the object language. This is also exactly how worlds are defined in the work on actualism; where this is called possible world semantics. I am a fan of both styles.
. The more we collapse the type universe the more powerful the theory becomes. Think of the difference between stratified system F and system F. We can gain incremental power by making connections between the levels. One way of doing this is adding universe polymorphism. This is like the connections between the mesh layers discussed above. These connections I found to be quite surprising, but also not so surprising. The brain is essentially the worlds most powerful computer. So it makes sense that computer science could help in figuring out how it works. Computation is what we do after all.
-calculus is dual to the call-by-name 
The first thing the reader who has at least a basic understanding of type theory will notice, is that, there is no function type or 
-abstraction! It turns out that these can actually be defined! I hope the reader’s head did not just explode. Here are the definitions:
-reduction rule. As for the remaining syntax of DC it is pretty routine. I only comment on a few aspects of it. I call variables 
input variables and variables 
output variables or output ports. The output ports will be replaced by the output of (co)terms. Statements 
can be viewed as commands where 
is computed with input 
binds the output port 
. Dually, the coterm 
binds the input variable 
indicates that each expression 
,
. Now the right-pointing arrow 
in the typing judgment indicates that 
, dually, in the syntax for the cotyping judgment the second left-pointing arrow indicates that 
he used an arrow pointing to 
which is close to my syntax, but still not as pretty. I find this style syntax to be hard to read, but I do think it makes sense once I understood it. I have this annoying belief that the syntax of a judgment should be sexy enough to make writing out derivations somewhat manageable.
The typing judgment means that when each 
has a value and 
of type 
. Dually, the cotyping judgment means when each 
Lastly, we have the sole rule of the cut judgment, the cut rule:
Well that is the dual calculus. It is a really interesting theory of classical logic. There are quite a few papers on the dual calculus. I sprinkled some throughout the post, but if the reader knows of any I would love to hear about them.