1933 - Kurt Gödel develops two interpretations of intuitionistic logic in terms of a
provability logic, which would become the standard axiomatization of S4.
1944 -
Emil Leon Post introduces the
partial order of the
Turing degrees, and also introduces Post's problem: to determine if there are
computably enumerable degrees lying in between the degree of computable functions and the degree of the halting problem.
1948 -
McKinsey and
Alfred Tarski study closure algebras for S4 and intuitionistic logic.
1950-1999
1950 -
Boris Trakhtenbrotproves that validity in all finite models (the finite-model version of the Entscheidungsproblem) is also undecidable; here validity corresponds to non-halting, rather than halting as in the usual case.
1952 - Kleene presents "Turing's Thesis", asserting the identity of computability in general with computability by Turing machines, as an equivalent form of Church's Thesis.
1954 -
Jerzy Łoś and
Robert Lawson Vaughtindependently proved that a first-order theory which has only infinite models and is
categorical in any infinite cardinal at least equal to the language cardinality is
complete. Łoś further conjectures that, in the case where the language is countable, if the theory is categorical in an uncountable cardinal, it is categorical in all uncountable cardinals.