# Earliest proof of the soundness of first order predicate logic

When was the soundness theorem for first order predicate logic (quantification theory) first proven?

Is there any evidence that soundness was presupposed or taken as self-evident prior to 1930?

• On how semantic notions were handled prior to 1950-s see Manzano-Alonso, Completeness: from Gödel to Henkin. In particular, the scene was dominated by Hilbert's decidability paradigm, and even "Gödel never employs semantic notions that we consider basic" in his completeness proofs. Church still warned that semantic passages are "not part of the logistic development" in late 1940-s. So what was presupposed, taken as self-evident, or even proved, before 1949 was not what "completeness" and "soundness" came to mean after. Apr 14 at 22:48

See D.Hilbert & W.Ackermann, Principles of Mathematical Logic: the 1950 American translation of the 1938 second edition of Grundzüge der theoretischen Logik.

The 1928 first edition is considered the first elementary text exposing the formalism now known as first-order logic.

See §9 The Consistency and Independence of the System of Axioms, page 87-on.

The consistency proof is based on an arithmetical interpretation in the universe $$\{ 0,1 \}$$ showing that all the axioms always yield the value $$0$$ and, in addition, that if one or more formulas always have the value $$0$$, any other formula obtained from them by means of the rules [of inference] likewise always gives the value $$0$$.

Gödel first proved the soundness theorem in his completeness theorem in 1930 based on proof theory ("Die Vollständigkeit der Axiome des logischen Funktionenkalküls"). The model-theoretic proof of the soundness theorem, i.e. a set of sentences is consistent if and only if they have a model, was first given by Henkin in 1949. However, the completeness theorem is also a corollary of results in Skolem's lecture note titled "On mathematical logic" in 1928.

A good sourcebook for mathematical logic is "From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931" edited by van Heijenoort in 1967, which contains the English translation of both Gödel's paper (p582--591) and Skolem's note (p508--524) listed above.

• NO; it was already available in Hilbert & Ackermann's textbook Grundzüge der theoretischen Logik (1st ed, 1928) Apr 15 at 6:06
• But the consensus is to credit the completeness theorem to Gödel. Skolem also got some credit for his lecture in in 1928. Apr 15 at 16:32
• OP asks when the soundness theorem for first-order logic was first proved. Apr 16 at 6:56
• The consensus for "every provable formula is valid" is that it was first proved by Henkin in 1949 but can be traced back to Godel's completeness theorem. The wiki page on the soundness theorem confirms that. Apr 16 at 19:09