The Soundness Theorem is the theorem that says that if in first-order logic, then , i.e. every structure making all sentences in true also makes true.
The main idea is sketched out in The Mathematics of Logic, but the formal proof needs the precise definition of truth which was omitted from the printed book for technical reasons. This web page provides the missing proof and should be read in conjunction with the printed book (especially Section 9.1 and Definition 9.8 on page 122 where the proof system for first-order logic is given) and the companion web page containing the definition of truth.
Like the definition of truth itself, the main problem is how to handle free-variables. Since variables are variable they have a meaning that is apparently allowed to change, and Soundness is all about meaning. The proof of Soundness is, like all soundness theorems, by induction on the length of a proof, and itself may be a set of sentences but to handle all subproofs we need an induction assumption that covers all possible statements that can be present as the assumptoin of a subproof, and these include arbitrary formulas with free variables. Therefore our induction hypothesis must say what to do with free variables.
The theorem we shall actually prove is the following strengthening of the Soundness Theorem. This has Soundness as an immediate corollary, and is also stated in such a way as to indicate the correct induction hypothesis for our proof.
Suppose is first-order language with set of variables and is any structure for . Then:
By induction on the length of the proof . We shall assume that the itemised statement is true for all proofs with at most steps and show it true for a proof of steps. It is important that the statement we are doing induction on ranges over all possible sets , and assignments , for as we shall see these vary during he course of this argument.
For the case of a proof of only one step there is nothing to say, since any proof with only a single step is either one using the given statements rule and this means the conclusion is the same as one of the assumptions , so , or else it is a proof of the trivially true statement , or of the statement by the Reflexivity rule. This last statement has since is itself reflexive and if and only if .
The rest of this argument follows the list of allowed proof steps given in Definition 9.8. See also the more detailled list of proof steps in web pages on proofs as trees and on substitution in first order logic.
If the last step in the proof being considered is one of the rules of propositional logic, then we mimic the proof of the Soundness Theorem for propositional logic, given in Theorem 7.10, page 84, using the specific boolean algebra . This is left as an exercise.
If the last step in the proof being considered is one of the equality rules, there are three cases corresponding to reflexivity, symmetry and transitivity. These are all straightforward, following from the reflexivity, symmetry and transitivity of and the clause in the definition of truth saying that if and only if .
If the last step in the proof being considered is the substitution rule, then we use the results of a previous web page on semantic aspects of substitution. In particular, we may assume that some is proved from in at most steps and also that for are also all proved from in at most steps, and that the conclusion is where are the substitutions and . Then by our induction hypothesis and so for each , hence by a a previous proposition on substitution and the induction hypothesis once more.
If the last step in the proof being considered is the ∃-Elimination rule, then we are given that in at most proof steps, and in at most proof steps, where the substitution is , also that the substitution is valid and does not appear free in nor nor in any other formula written down in scope. Then ∃-Elimination gives us the conclusion in at most steps: we must show this conclusion is sound.
Let be an assignment such that for each . Then by induction also. This means that there is some value such that the assignment has . Let be the substitution and . Then so . Also, for each , since is not free in , and therefore by induction and we have . It follows that since once again only differ at which is not free in , and this is the required conclusion.
If the last step in the proof being considered is the ∃-Introduction rule, then we may assume that in at most steps and is the statement , where the substitution is for some . Then given an assignment with for each , we have by our induction hypothesis. Let , the element of to which is assigned by . Also let . Then . It follows from the definition of assignment that since makes true.
If the last step in the proof being considered is the ∀-Elimination rule, then we argue in a similar way to the case for ∃-Introduction. We have in at most steps, and we are given some term . Then for any assignment with for each we have by the induction hypothesis. Now let be the substitution and . Then has and hence , as required.
If the last step in the proof being considered is the ∀-Introduction rule, then we argue in a similar way to the case for ∃-Elimination. We are given and variables and substitution and have that in at most steps, where no statement written down that is in scope has free. Let be an assignment with for all and let be arbitrary. Let . Then let and observe that for all since does not appear free in any such and hence by induction . But and therefore the concusion is that and hence as was arbitrary.
A boolean valued model for the first order language
is a set with a boolean algrebra and
special elements for each constant symbol
of , functions for each -ary
function symbol of and for and for each -ary relation
symbol of it has a function
State and prove a Soundness Theorem for boolean valued models.