, where P is a P.O.G.-set with partial ordering <= and maximal element p_0, and w is a function with domain P x F and range the set {O,1} such that for all p \in P: (i) For an atomic formula A_i,w(p,A_i)=1 iff, for all p'<=p, w(p',A_i)=1. (ii) w(p,U \and V)=1 iff w(p,U)=l and w(p,V)=1. (iii) w(p,U \or V)=1 iff w(p,U)=l or w(p,v)=1. (iv) w(p \implies V)=1 iff, for all p'<=p, w(p',U)=O or w(p',V)=1. (v) w(p, \not U)=1 iff, for all p'<=p, w(p',U)=0. Remark. (i) is assumed only for atomic formulas, but can be proven thence for all formulas by using (ii)-(v). The following completeness theorem can be proten by using semantic tableaux or from the theory of pseudo-Boolean algebras: Th.1.1. For all formulas U, U is a theorem of P_p (1) iff, for all I-valuations for all P.O.G.-sets

w(p_0,U)=l, or (2) iff, for all I-valuations on finite P.O.G.-sets, w(p_0,U)=1. In [14] Kripke also describes an intuitive interpretation of l-valuations. The P.O.G.â€”set is taken as a set of possible situations (stages), where the partial ordering plays the role of time, i.e. if q>=p, then q is supposed to be a possible future situation as seen from p. Time is seen as discreet, one can move from an earlier stage to any possible later one, but one can stay at any stage for an unlimited amount of time. The stages can be represented by certain sets of axioms, certain methods of derivation or in a special application of ours in Chapter VI, by the computability of certain functions. We can extend the concept of I-valuation to the predicate calculus. There an I-valuation is a sextuple

, where P,<=,p_O and w have the same meaning as before, D is a non-empty set (interpreted as a set of individuals) and d is a function from P into P(D) (the power set of D) such that, if p'<=p, the d(p) \subseteq d(p'). The domain of w is now the set of couples

, where U is a formula without free variables built from atoms A_i,A_j( ),A_k( , ),... (i,j,k=l,....\infty), individual constantsâ€™ from d(p), variables and quantifiers. And w has to fulfill the additional properties: (vi) w(p,\forall x U(x))=1 iff for all p'<=p and u \in d(p') w(p',U(u))=1. (vii) w(p,\exists x U(x))=1 iff for some u \in d(p) w(p,U(u))=1.