 Kripke’s 1959a “A Completeness Theorem in Modal Logic” contains a model theoretic completeness result for a quantified version of S5 with identity. In Kripke’s semantic treatment of quantified S5, which he calls S5*\(^=\), an assignment of values to a formula \(A\) in a domain of individuals \(D\) assigns a member of \(D\) to each free individual variable of \(A\), a truth value \(T\) or \(F\) to each propositional variable of \(A\), and a set of ordered \(n\)-tuples of members of \(D\) to each \(n\)-place predicate variable of \(A\) (the language for the system contains no non-logical constants). Kripke defines a model over a non-empty domain \(D\) of individuals as an ordered pair \((G, K)\), such that \(G\in K, K\) is an arbitrary subset of assignments of values to the formulas of S5*\(^=\), and all \(H\in K\) agree on the assignments to individual variables. For each \(H\in K\), the value that \(H\) assigns to a formula \(B\) is defined inductively. Propositional variables are assigned \(T\) or \(F\) by hypothesis. If \(B\) is \(P(x_1, \ldots, x_n)\), \(B\) is assigned \(T\) if and only if the \(n\)-tuple of elements assigned to \(x_1\), …, \(x_n\) belongs to the set of \(n\)-tuples of individuals that \(H\) assigns to \(P. H\) assigns \(T\) to \(\neg B\) if and only if it assigns \(F\) to \(B. H\) assigns \(T\) to \(B\wedge C\) if and only if it assigns \(T\) to \(B\) and to \(C\). If \(B\) is \(x = y\) it is assigned \(T\) if and only if \(x\) and \(y\) are assigned the same value in \(D\). If \(B\) is \((\forall x)Fx\) it is assigned \(T\) if and only if \(Fx\) is assigned \(T\) for every assignment to \(x\). \(\Box B\) is assigned \(T\) if and only if \(B\) is assigned \(T\) by every \(H\in K\).