Investigations on the Intuitionistic Propositional Calculus
Dick de Jongh

Abstract:
The first investigations in the field of semantics of intuitionistic logic were by Beth with the aid of his semantic tableaux.  His completeness results for the predicate calculus were improved by Dyson and Kreisel. Later Kripke built on this work, and with slightly changed semantic tableaux and a different interpretation reached more easily completeness results closely related to the earlier ones. Independently Beth in his last publications and de Jongh worked on these methods. Later Aczel gave a Henkin-type completeness proof built on the same principles.
  We will start out with a description of a completeness theorem for the propositional calculus which is slightly different from but obviously equivalent to Kripke's.
  In our propositional calculus we will study formulas U,V,W,Ul,U2,...,V1,V2,...,Wl,W2,...,  built from atomic formulas A1,A2,..., by means of the connectives \and, \or, \implies and \not.  For a system of axiom schemas for the intuitionistic propositional calculus Pp, and for the classical propositional calculus PC, see e.g. [11]
  Def. A 'P.0.G.-set' is a partially ordered set with one maximal element (the greatest element).
  We will write F for the set of all formulas.
  Def. An 'I-valuation' is a quadruple <P,<=,p_0,w>, 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 <P,<=,p_0> 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 <P,<=,p_O,d,D,w>,  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 <p,U>, 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.