Saul Kripke - Intuitionistic Logic

Intuitionistic Logic

Kripke semantics for the intuitionistic logic follows the same principles as the semantics of modal logic, but uses a different definition of satisfaction.

An intuitionistic Kripke model is a triple, where is a partially ordered Kripke frame, and satisfies the following conditions:

• if p is a propositional variable, and, then (persistency condition),
• if and only if and ,
• if and only if or ,
• if and only if for all, implies ,
• not .

Intuitionistic logic is sound and complete with respect to its Kripke semantics, and it has the Finite Model Property.

Intuitionistic first-order logic

Let L be a first-order language. A Kripke model of L is a triple, where is an intuitionistic Kripke frame, M_w is a (classical) L-structure for each node w ∈ W, and the following compatibility conditions hold whenever u ≤ v:

• the domain of M_u is included in the domain of M_v,
• realizations of function symbols in M_u and M_v agree on elements of M_u,
• for each n-ary predicate P and elements a₁,…,a_n ∈ M_u: if P(a₁,…,a_n) holds in M_u, then it holds in M_v.

Given an evaluation e of variables by elements of M_w, we define the satisfaction relation :

• if and only if holds in M_w,
• if and only if and ,
• if and only if or ,
• if and only if for all, implies ,
• not ,
• if and only if there exists an such that ,
• if and only if for every and every, .

Here e(x→a) is the evaluation which gives x the value a, and otherwise agrees with e.