Actually, we could have introduced intuitionistic logic starting with a proof system like this,

with a Gansen proof system, and then put some strange or maybe not so strange restrictions

on the shape of the rules.

And this is something that I was originally planning to do, but then I thought that it's

not so obvious why you want to put those restrictions.

What is the motivation, computer science, application, philosophical behind such restrictions.

So we start in the same way as we did with model logic.

And we first going to talk about semantics.

But we will return to all this, maybe even to the proof of misability of contraction

in this more complicated setting.

And indeed, then you want your rules to be, that you want to invert this trick with the

inversion of the rules and high preservation.

It's not going to be as symmetric and you will have more rules to take care of.

This is for you.

So we are going to start again with Kripke frames.

But this time, this will be very special ones.

You remember that we spent a lot of time talking about posets, partially ordered sets, and

threes.

And now they are our intended semantics.

And the logic that we will talk about will have no funny connectives like boxes, diamonds,

or whatever.

It will have exactly the same connectives as you know from classical logic.

They were just interpreted in a funny way.

I should perhaps have this intuitionistic propositional logic in all of our lectures

when we are studying propositional systems.

So intuitionistic Kripke frame is just of this form where this thing is just partial

order and w.

And you remember the notion of partial order at the House of Capp and from analogic.

So this is what we call such a pair with universe and partial ordering on it is normally called

poset, partially ordered set.

And just like before, we have the notion of valuation.

But now something funny will happen to those valuations.

So if you recall how it worked in model logic, if you did not add any connectives like boxes,

diamonds, or what else to the standard syntax, you will have the same logic as usual, the

classical logic of our Kripke frame.

So it's clear that we must put some restrictions and also change the way some of the connectives

are interpreted to obtain something interesting, something new.

So first let's say that we are only restricting attention to the upward closed subsets.

So this is a proper, this is well most of the time proper subset or subfamily of the

collection of all posets of w.

And I should perhaps write what it means to be a path closed.

So let's say x containing w is upward closed if x in x, x below y implies y belongs to

w.

So now the new thing, because those guys could be as well Kripke frames for normal logic,

but valuations have to have some special features.

So the set of atoms was written as atoms or propositional variables or var, how did we

write it?

Atoms?

It's intuitionistic valuation.

So if you said that a given atom is true at a given point, then in all future stages of