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?
1
-
1$\begingroup$ 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. $\endgroup$– ConifoldCommented Apr 14, 2021 at 22:48
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
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$.
The word "soundness" is not used, but the proof implies soundness, because it shows that the axioms are "identically equal to $0$" (page 39) and that the rules of inference "transfer" the value $0$.
An early occurrence of "sound interpretation" is in Alonzo Church's Introduction to Mathematical Logic (1956), page 109.
For an early modern "model theoretic" approach, see John Kemeny, A new Approach to Semantics I (JSL, 1956), where we found the following comments wrt "syntactical" concepts (like consistency): "What is important is whether they reproduce the intuitive meaning, and whether they are based on sound concepts."
Leon Henkin's result of 1949: "If $\Lambda$ is a set of formulas [...], and if $\Lambda$ is consistent, then $\Lambda$ is simultaneously satisfiable in a domain of individuals..." (page 162), from which the corollary: "If $A$ is a valid wff then $\vdash A$" (page 164), is still the "one direction" completeness of Gödel 1930's paper.
answered Apr 15, 2021 at 6:14
$\begingroup$
$\endgroup$
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.
