# 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?

This (https://math.stackexchange.com/a/2681301/387521) answer suggests that it was never given a formal proof prior to 1930. If so, what can we make of earlier results (for example, Lowenheim's 1915 proof of the Lowenheim-Skolem theorem) which contain gaps fillable by an appeal to propositional compactness? Is there any evidence that propositional compactness or an equivalent result would have been considered self-evident at the time?

• 1930 is obviously an upper bound. Do you suspect that it compactness for PL might have been discovered earlier? Jun 19, 2020 at 21:58
• @RobArthan I'm almost certain that completeness of truth tables for propositional logic was proved pre-$1930$, and analogously to the first-order situation compactness is a trivial corollary of that. However, I'm not as certain that propositional compactness would have been seen as worth stating on its own pre-$1930$. Jun 19, 2020 at 22:04
• @NoahSchweber: maybe: what looks now like an obvious corollary may not have seemed so in the early days of mathematical logic. This question needs some historical research (perhaps by the OP $\ddot{\smile}$) for a more definite answer. Perhaps it would do better on hsm.stackexchange.com. Jun 19, 2020 at 22:13
• @RobArthan Sure, I'm just saying it's very reasonable for the OP to suspect there's a better bound. (And after a quick google jaunt I couldn't find the answer immediately, so I think this is fine for MSE.) Jun 19, 2020 at 22:14
• @NoahSchweber: I have no complants about this as an MSE question. I just thought that HSM might get the OP an answer sooner. Jun 19, 2020 at 22:17

The situation appears to be the following:

The propositional compactness theorem is first implicitly proved in $$1921$$ in the form of the propositional completeness theorem, but it's not until Godel's work on first-order logic that compactness was identified as an interesting property in its own right.

The earliest treatment of propositional logic from the now-standard "provability vs. truth" perspective was surprisingly late to the party. As far as I can tell, the first paper to really lay this out was Emil Post's $$1921$$ paper Introduction to a general theory of elementary propositions. To quote Beziau's article An unexpected feature of classical propositional logic in the Tractatus, page $$387$$:

After Peirce who proved that all the $$16$$ [binary] connectives can be defined by only one (joint work with his student Christine Ladd-Franklin) [..., Post's paper] is the first work with important mathematical results: completeness, functional completeness and Post completeness. In mathematics results work together with conceptualization. In Post's paper we find for the first time a clear distinction between proof and truth in [classical propositional logic], distinction on which basis the completeness theorem which is herein presented makes sense.

Compactness is such an easy corollary of completeness that it's arguably implicit in Post's results; however, at a glance it does not seem to be stated explicitly. One possible reason for this is that - as far as I can tell - infinite propositional theories weren't even objects of explicit study until circa Godel, so compactness didn't have a chance to arise.

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.

• This does not contradict, but also does not confirm, the supposition that no one gave a formal proof of propositional compactness before G\"{o}del. Dawson's paper concerns the period after 1930 whereas I am really wondering about the background suppositions of the period leading up to it. Jun 20, 2020 at 15:59
• @Mallik - Frankly speaking, I've some difficulties to understand your point of view... :-) Are you interested in FOL ? If so, the answer is well-known: Godel (as per HSM's accepted answer to your question; answer that does not speak of propositional calculus). If instead (as per the title of the question) you are interested to prop logic, the "received answer" is:" it was obvious". Personally, I'll prefer to provide detailed refererences. Jun 20, 2020 at 18:38
• @MauroALLEGRANZA I think the OP's point of view is reasonably clear. They're interested in the propositional case, and they don't believe (neither do I) that it in fact was always obvious - after all, plenty of early work in propositional logic is stuff we now consider totally trivial. Jun 21, 2020 at 16:16