As promised, today, I’m going to show the Kripke semantics model for intuitionistic logic.

Remember from yesterday that a Kripke model has three parts:

(**W**, **R**, **:-**), where **W** is a set of worlds; **R** is a transition relation between worlds; and “**:-**” is a forces relation that defines what’s true in a particular world.

To model intuitionistic logic, we need to add some required properties to the transition and forcing relations. With these additional properties, we call the transition relation (R) “≤”; if A and B are worlds in **W**, then “A≤B” means that B *is accessible from* A. For an intuitionistic Kripke model, the transition relation “≤” must be both reflexive (A ≤ A) and transitive (if A≤B and B≤C, then A≤C), making it a pre-order relation – that is, a relation that has the essential properties of arithmetic “≤” that is necessary to define a partial order over its domain. The forces relation, “:-” also needs some additional conditions: (these conditions are based on the definitions from the wikipedia article on Kripke models; I can’t remember them without help, so I used the article as a reference.)

- ∀w,u∈W such thatt w≤u, for all statements s if w:-p, then u:-p. This condition basically says that if a statement is true/valid in a particular world w, then it must be true in all worlds accessible from w – meaning that in intuitionistic logic, once a statement is proven, it can’t be taken back.
- ∀w∈W, w:-(A∧B) if/f w:-A and w:-B. “A∧B” is provable in w only if both A and B are provable.
- ∀w∈W, w:-A∨B if/f w:-A or w:-B. “A∨B” is provable in w only if either A or B is probable in w.
- ∀w*isin;W, w:-(A→B) if/f ∀u∈W such that w≤u, (u:-A) implies (u :-B). Being able to prove that “A implies B” in w means that in every world accessible from w, if you can prove A, then you can prove B.
- There is no contradictory statement (written ⏊) such that w:-⏊.

The last line in there is actually a bit of a cheat: you can think of intuitionistic logic as a logic where at a given point of time, a statement can have three truth values: T (top), which means provably true; ⏊ (bottom) which means provably false, and unproved. The last property of the forces relationship means that under no conditions can the “forces” relation say that a proposition is true if it is provably false.

So: suppose we have an intuitionistic logic consisting of a set of statements, which we’ll call X. The Kripke model for X is the triple (W,≤M), where W is the set of worlds related by a “≤” relation that has the intuitionistic properties that we just discussed. M is a set of sets where: ∀w∈W: ∃!M_{w}∈M, where M_{w} is an L-structure for X. (An L-structure is a formal way of defining what statements are proved true – and for statements with variables, the bindings of those variables to values for which the statement has been proved true. For the purposes of understanding, you can think of M_{w} as a function that takes a logical statement, and a list of values for the variables in that statement, and returns “true” if the statement is proved true, and false if the statement is proved false; and the statement is not in the domain of the function if it’s truth value hasn’t been proved.) The M_{w}‘s for intuitionistic logic have a set of properties that come from the meaning of statements in the logic. If u and v are both worlds in W, and M_{u} and M_{v} are their corresponding L-structures, then:

- if u≤v, then domain(M
_{u})⊆domain(M_{v}) - For any function f, in the logic, ∀a∈range(f) in M
_{u}, f(a) in M_{u}= f(a) in M_{v}. - For any predicate P(a
_{1},a_{2}, …, a_{n}), if P(a_{1},a_{2}, …, a_{n}) is true in M_{u}, then it is true in M>_{v}.

Now, finally, we can get to the last step in defining our model of intuitionistic logic: the forces relation based on M. What we need to do to make M work as a forces relation is to separate it into two parts: the truth/validity of concrete statements (that is, statements with all variables bound to specific values), which we write using the old forces notation, :-; and the mapping of variables and functions to values. We call that mapping an evaluation function; for a statement A in X, we write A[e] for A with variables bound by e.

So: given an evaluation e of variables from M_{w}, w:-A[e] is defined by:

- w:-P(a
_{1},…a_{n})[e] if/f

P(a_{1}[e],…,a_{n}[e]) is in M_{w}: Evaluating a

predicate means the same thing as keeping the predicate unchanged, and evaluating

each of its parameters separately. - w:-(A ∧ B)[e] if/f w:-A[e] and w:-B[e]: a typical and definition.
- w:-(A ∨ B)[e] if/f w:-A[e] or w:-B[e]: a typical or definition.
- w:-(A → B)[e] if/f ∀w≤u: u:-A[e] implies u:-B[e]: an implication is true if, in the model, you can prove its constituents in the next step. (This is the opposite of its definition in the logic: in logic, we’d say that given A implies B and A, you can conclude B. In the model, we go the other way, and say that you can conclude that A implies B if, for all possible transitions, the next world allows you to conclude either A or not B.)
- w ¬:-⏊: no w can force a contradiction.
- w:-(∃x:A)[e] if/f exists a∈M
_{w}such that w:-A[e], and e maps x to a: An exists statement is provable only if we can show a concrete, specific value for which the statement is true. - w:-(∀x:A)[e] if/f ∀u such that w≤u: ∀a∈M
_{u}: u:-A[e] where e maps x to A: a universal statement is provable if every possible next world can prove that the statement with all possible bindings of variables are true.

What we’ve done now is to define a way of describing the meaning of any statement in intuitionistic logic, and any reasoning step in intuitionistic logic in terms of sets, in a way where if we do the translation of the logical statement down to the sets, the statements about the sets will always be true and correct; and if we reason from the sets that correspond to the logic, anything we can do will produce a well-defined, meaningful, and valid statement in the logic.

The particularly nice thing about an intuitionistic logic with a Kripke model is that for any statement which is provably true, we can use the model to find specific values for the variables in the statement for which its true; and if a statement is false, we can find specific values for the variables in the statement that produce a concrete counterexample. In fact, the *specific meaning* of ¬A in this model of intuitionistic logic is that I have a *concrete counterexample* for A, so that A cannot be proven.

We can’t always do that in regular predicate logic: regular predicate logic allows us to do inferences from things like “exists” statements if we know that some value must exist for which the statement is true, even if there’s no way for us to figure out what that value is. Likewise, in regular predicate logic, we can infer that a forall statement is false if we know that there must be some value for which it’s false; in intuitionist logic, we need to be able to show a specific example for which it’s false.

clemSince you are doing modal logics, it might be good to discuss how modal schema correspond to mathematical properties and how one gets from one to the other. To me at least, it is far from immediately obvious that the schema Lx -> LLx implies transitivity or Mx -> LMx represents the Euclidean property.

Chad GroftActually, you can do this in intuitionism too, because the interpretation of “∃x:A” in intuitionism is stronger, not weaker. Essentially, it says “I know of some particular c where A[c] holds”, but doesn’t tell you what c is. This is stronger than the statement “I know that A[c] must hold for some c”.

What you can’t do is

conclude“∃x:A” by arguing from contradiction, as you might in classical logic. You also couldn’t conclude its truth intuitively without having a candidate in mind, as one might with (for example) the Axiom of Choice.This one’s not true either. Negated statements in intuitionism tend to be “weak” in a certain sense. I’ll elaborate later when I have time.

Chad GroftOkay, back. I’ll give you a specific example where a condition forces ¬∀x:P(x) but not ∃x:¬P(x).

Let P(x) be a unary relation symbol. To build the Kripke model, we start with the set of conditions {0,1} with the usual [pre]order. At 0, the universe is {a}; at 1, we expand the universe to {a,b}. We have 0 ¬:- P(a), 1 :- P(a), and 1 ¬:- P(b).

Both 0 and 1 fail to force ∀x:P(x) (0 because of a, 1 because of b), so 0 :- ¬∀x:P(x). 1 :- P(a), so 0 ¬:- ¬P(a), so 0 ¬:- ∃x:¬P(x).

The trick, as I hinted before, is that ¬∀x:P(x) says something negative about the assertion P, while ∃x:¬P(x) says something positive about the assertion ¬P. In classical logic, these are equivalent; in intuitionism, negative statements are weaker than positive ones. You see this also with A versus ¬¬A; the first is a positive statement, the second is negative and weaker.

blaisorbladeThe problems start here:

> In fact, the specific meaning of ¬A in this model of intuitionistic logic is that I have a concrete counterexample for A, so that A cannot be proven.

In fact in intuitionism, ¬A just means A → ⊥ and is interpreted using the standard rules. That means that, to prove ¬A, you just derive a contradiction (constructively) from A, however you like. Proof by contradiction is only forbidden for positive statements, because in intuitionistic logic you can’t derive ¬¬A → A, only ¬¬¬A → ¬A. If you read ¬A as “A is inconsistent”, this means that the ¬¬A is the inconsistency of the inconsistency of A.

Chad GroftOne final technicality: It’s fairly important in a number of cases to have “two” elements of a universe which may be equal, but are not yet known to be equal. This can’t happen if we assume that u ≤ v implies domain(M_u)⊆domain(M_v). What we really want is an arbitrary functor from the preorder to the category of sets. The function f_{uv} (which is the target of the unique morphism u -> v if u ≤ v) need not be onto, as you’ve noted, but it also need not be one-to-one. Some of the definitions should be altered accordingly.

Jonathan Vos PostarXiv:0704.1886

Title: An algebraic generalization of Kripke structures

Authors: Sérgio Marcelino, Pedro Resende

Comments: 39 pages

MSC-class: 03B45 (Primary) 03G25, 06F07 (Secondary)

The Kripke semantics of classical propositional normal modal logic is made algebraic via an embedding of Kripke structures into the larger class of pointed stably supported quantales. This algebraic semantics subsumes the traditional algebraic semantics based on lattices with unary operators, and it suggests natural interpretations of modal logic, of possible interest in the applications, in structures that arise in geometry and analysis, such as foliated manifolds and operator algebras, via topological groupoids and inverse semigroups. We study completeness properties of the quantale based semantics for the systems K, T, K4, S4, and S5, in particular obtaining an axiomatization for S5 which does not use negation or the modal necessity operator. As additional examples we describe intuitionistic propositional modal logic, the logic of programs PDL, and the ramified temporal logic CTL.

blaisorbladeI have a technical quibble with the definition of forall and exists — when the evaluation function recurses, evaluation does not assume that e maps x to a (what would that mean?), but it _extends_ e with a new mapping x to a — so e.g. instead of

“w:-(∃x:A)[e] if/f exists a∈Mw such that w:-A[e], and e maps x to a”

you need

“w:-(∃x:A)[e] if/f exists a∈Mw such that w:-A[e(x -> a)]”

and similarly you need

“w:-(∀x:A)[e] if/f ∀u such that w≤u: ∀a∈Mu: u:-A[e(x -> a)]”

I even guess that’s what you wanted to write anyway. Compare with https://en.wikipedia.org/wiki/Kripke_semantics#Intuitionistic_first-order_logic — I’ve taken the notation e(x -> a) from there.