# When was compactness theorem for propositional logic first proven?

Compactness for first-order predicate logic was first proven as a corollary of (Gödel 1930). Does anyone know a reference for the first proof of the compactness of propositional logic?

Some proofs from around 1915 (e.g. Lowenheim's proof of the Lowenheim-Skolem theorem) seem to invoke it implicitly and I am wondering whether it was considered so obvious as to never have received a formal proof.

For a general overview of the history of first order logic see SEP, The Emergence of First-Order Logic. On the history of compactness theorem more specifically see Dawson, The compactness of first-order logic: from Gödel to Lindström and van Heijenoort, Dreben, Introductory note on 1929, 1930 and 1930a to Kurt Gödel: Collected Works: Volume I.

What these sources note is that neither the notion of first order logic nor the semantic/syntactic distinction essential to the formulation of the compactness theorem appear in the literature before Gödel's 1929 dissertation. So it is fair to say that the compactness theorem was not only first proved, but even first stated, by Gödel in 1930, who inferred it from a generalization of his completeness theorem. None of the sources credits Löwenheim even with loosely anticipating the compactness theorem (a set of sentences is satisfiable if and only if every finite subset of it is satisfiable), in contrast to the downward Löwenheim-Skolem theorem (if a set of sentences is satisfiable it is satisfiable on a countable model).

The credit for anticipating compactness goes rather to Skolem's Einige Bemerkungen zur axiomatischen Begriindung der Mengenlehre (1923). The 1923 paper is known for giving a proof of a version of the downward Löwenheim-Skolem theorem that did not appeal to the axiom of choice, which he previously used in Logisch-kombinatorische Untersuchungen iiber die Erfiillbarkeit oder Beweisbarkeit mathematischer Satze nebst einem Theoreme über dichte Mengenwas (1920). In its turn, this prior proof fixed Löwenheim's 1915 proof, which is considered faulty because it implicitly used the König's lemma not known at the time.

Here is Dawson:

"Gödel's proofs employed Skolem's methods; but, unlike Skolem, Gödel carefully distinguished between syntactic and semantic notions. The relation between the works of the two men has been examined by Vaught (1974, 157-159) and, in great detail, by van Heijenoort and Dreben 1986. All three commentators agree that both the completeness and compactness theorems were implicit in Skolem 1923, but that no one before Gödel drew them as conclusions, not even after Hilbert and Ackermann, in their 1928 book Grundzüge der theoretischen Logik singled out first-order logic for attention and explicitly posed the question of its completeness.

Vaught attributes the delay in the enunciation of the completeness theorem to 'the lack of able logicians who knew and appreciated both the notion of model and the notion of logistic system', but he notes that such an excuse does not apply in the case of the compactness theorem, since it is a purely semantic statement. Rather, he opines that perhaps 'the compactness theorem was not [...] inferred by Skolem or others' at that time simply because, 'when viewed as a theorem of pure model theory [... it] appears wholly unlikely'. Alternatively, Godel himself attributed the 'blindness of logicians' toward the completeness theorem (and, by extension, the compactness theorem as well) to the 'widespread lack, at that time, of the required epistemological attitude', not only 'toward metamathematics' but 'toward non-finitary reasoning'."

Van Heijenoort and Dreben add the following (Theorem IX is a generalization of the completeness theorem):

In 1930 (below, page 119) the generalization is labeled Theorem IX and is obtained immediately, by means of the completeness theorem, from Theorem X, which does not appear in 1929 and is known today as the compactness theorem... The proof sketched for Theorem X differs essentially from the 1929 sketch for the generalization (Theorem IX) only in one regard... But, since provability in a formal system is now discarded, Gödel's argument for compactness comes very close to Skolem's (suggested) argument in 1923a for his generalization of the Löwenheim-Skolem Theorem."

See John Dawson, The Compactness of First-order Logic From Gödel to Lindström (HPL,1993), page 18:

After 1934, [...] the only person who seems to have recognized the importance of compactness was the Russian A. I. Maltsev. Beginning in 1936, he published 'a seminal run' of papers in what would now be called model-theoretic algebra, papers in which he 'obtained applications [of logic] to group theory of greater technical virtuosity than the possibly more basic applications to algebra later on found [...] by Henkin and Abraham Robinson' (Sabbagh 1991). Three of those papers (1936,1940 and 1941) are of interest here.

In his first published work, written in German, Maltsev 1936 [Maltsev, A.I. 1936 'Untersuchungen aus dem Gebiete der mathematischen Logik', Matematicheskii Sbornik, n.s., 1, 323-336.] devoted his efforts to generalizing two theorems, one for the propositional calculus and the other for the restricted functional calculus. The theorems in question were Godel's compactness theorem and Skolem's result that no denumerable set of formulas of first-order logic can completely characterize the structure of the natural numbers.

See English translation into: A.I. Mal'cev, The Metamathematics of Algebraic Systems: Collected Papers 1936-1967 (North Holland, 1971), page 1:

This article is devoted to generalizing two theorems, one for propositional calculus (PC) and the other for first-order predicate logic (FOPL). The first theorem is due to Gödel [K. Gödel, Die Vollsthdigkeit der Axiome des logischen Funktionenkalkuls (1936),] and can be formulated as follows:

For any countable system of formulas of PC to be consistent, it is sufficient that every finite part of the system be consistent.

Finally, see also On a General Method for Obtaining Local Theorems in Group Theory by A. Mal'cév, Review by Leon Henkin and Andrzej Mostowski (Jsl, 1959):

Historical note. The formulation and proof of the "general local theorem" [If every finite subset of a given (possibly non-denumerable) set of first-order sentences is satisfiable, then so is the whole set] for denumerable sets of first-order sentences is of course due to Gödel in 1930. The corresponding result for non-denumerable sets of formulas of propositional calculus was given by Mal'cev in 1936.

The result can be easily derived from A.Tarski's 1930 paper (On some fundamental concepts of Metamathematics, published in German in 1931) were it is stated (without proof) as Theorem 11, expressing the Finiteness property of the consequence relation: thus, it was "obviously" applicable to propositional calculus.