A game for testing the equivalence of Kripke models with respect to finitary and infinitary intuitionistic predicate logic is inr and applied to discuss a concept of eategoricity for intuitionistie theories.
We introduce a method-similar to Ehrenfeucht~Fraiss~-gamesfor testing whether two Kripke models for intuitionistie predicate logic are equivalent with respect to this logic. Then a corresponding generalization of a well-known theorem of Karp (theorem u of [1] ) characterizing equivalence of models with respect to infinitary logic is proved. These results are applied to obtain a concept of eategorieity for intuitionistic theories. We mention without proof that modal logics can be treated in a similar (but easier) way (see [3], [6]).
The reader is assumed to be familiar with the usual Kripke semantics for intuitionistic logic, lt:ripke models are denoted by pairs (9~, lI) where 9X = (A, R, 2) with tt c A s, _p ~ A is the frame and lI is a function assigning to every a e A a classical model ll(a) such that the well-known conditions arc satisfied, aIk~ means that the sentence ~ (possibly with parameters from IlI(a)l) is true at the "possible world" a.
The letter i will always denote 0 or 1, j is always 1--i. The superscripts i or j are used to refer to the model ~t or 92~ j, respectively. For every a eA i we put At(a)--= {b e Ai: at~ib}. A 1partial homomor19hism between the models 93~ ~ and 9~ is a quadruple (i, a ~ a 1, 19) such that a ~ e A ~ a 1 e A 1, 19 c IlIO(aO)] x tlIl(al)] such that for all atomic formulas ~(x~, ... ..., z.), all (c ~ ..., (c ~ 19.
lI~(a i) k~(e~, .I vi) implies lIi(aJ)I=~ (e{, ..., o~). ~[i(ai)[ ' then for some c i ~ ]lF(aJ)] and for some q ___ ~o w {c ~ v 1) we have (i~ a~ a% q) e 3) if (i, a~ al, p)e~, bJeAJ(aJ), vie IlIi(bJ)], then there are b i eA~(a~), # e IlIi(bi)] and a relation q ~_ 19w{(c ~ e~)) such that (0~ b ~ b ~, q) ~ and (1, b~ b~ q) e~. In this e~se we write ~:9~%-%92~ ~. 9~~ ~+~!}~ ~ means that there is an intuitionistic homomorphism from 9tt o to ~1.
The following" lemmata are easily verified.