  By the late summer of 1958, Kripke had a completeness result for S4. On 3 September 1958 he wrote to Prior, mentioning his work on semantical completeness theorems for quantified extensions of S4 with and without the Barcan formula (Marcus 1946, 1962). (Prior himself had already given an early counterexample to the Barcan formula in a tense-modal context (Prior 1957: 26, Copeland 2016).) In his September letter, Kripke gave a branching-time matrix, characteristic for S4. This is essentially a tense-logical interpretation of the reflexivity + transitivity semantics for S4. He wrote: