This web page presents and discusses the precise notion of semantics for first-order logic, in particular the definition of what it means for a sentence to be true in a structure .
The definition of what it means for is attributed to Tarski in the 1920s. It is not clear to me whether other people at the time even realised that this was a notion that could be defined adequately by mathematical means. (As a student I had various non-mathematical friends who clearly thought there was something heretical when I announced one day that I had just read an account of the definition of truth.) Tarski himself seemed at this time to regard his definition as methodological book-keeping, and not as useful mathematics, though it clearly is an important step before the question of completeness of first-order logic can be stated let alone proved. (The first proof of the Completeness theorem for first-order logic is due to Gödel in 1930.) In much more advanced work and certain specific circumstances (for instance the theory of satisfaction classes in models of Peano Arithmetic) this definition of truth has genuine mathematical importance, but in most contexts it really is just book-keeping, and so the discussion is relegated to these web pages.
The formal definition of is by induction on the complexity of the statement , and there are several sub-clauses corresponding to the different kinds of sub-formulas that may occur in . But before we give these we indicate the main complication, which is that sub-formulas of are not necessarily sentences but are formulas, and as such contain free-variables which must be given specific meanings too during the inductive definition.
There are two possible approaches to this problem, each with advantages and disadvantages. One approach is to work with a larger first-order language with constant symbols naming all elements of our structure . This is convenient as it will eventually allow us to discuss with ease a great number of properties of and its elements. It does however rely on the idea of substitution of terms for variables, another tricky technical issue that is addressed in these web pages elsewhere. To make this web page more self-contained, we approach the definition of truth by starting with a different way of attaching meanings to free variables.
For the rest of this web page, we fix a first-order language with variables (for ) and various constant symbols, relation and function symbols (of possibily different arities) as described in Definition 9.1. We denote by the set of variables of . In particular, note that we assume a one-to-one correspondence given by . The definition of truth given below will rely on the fact that our first-order language has exactly these variables, and the variables are all distinct.
We also fix for this discussion an -structure as in Definition 9.22, where is a non-empty set, the domain of the structure, and for simplicty of notation we use the same symbol to denote both the structure and its domain.
An assignment of variables into is a function .
An assignment of variables into extends to a function (which we shall also denote ) that takes an arbitrary term of and gives an element of the domain of . This definition is very similar to the way a valution extends to a map on a boolean algebra .
Let denote the set of terms of as defined in Definition 9.2.
An assignment of variables into extends to a function as follows.
(We remark that the notation is potentially confusing as
the same symbol is used for different objects:
for both the structure and its domain;
for the constant symbol and the element of realising it;
for the function symbol and the function on realising it;
for the assignment of variables and for the assignment of
terms derived from it. However, the alternative would be
cumbersome and pedantic. Such use of
overloading of symbols is common
in computer programming and mathematics and is highly beneficial
to everyone once the reader has observed it and appreciated it.)
Because a term can be read in exactly one way (this is the unique readability of terms), the definition above shows that every assignment of variables extends in a unique way to an assignment of terms .
The next step is to define an assignment of truth values in to each formula of , following Definition 9.4. The third clause here is exactly the extension of a valuation into a boolean algebra to the whole of as given following Definition 7.1.
If is an assignment of variables, and then denotes the assignment of variables given by and for all . By the above definition, can be considered as an assignment of terms of in the same way.
Let denote the set of formulas of as defined in Definition 9.4.
An assignment of terms gives rise to an assignment of formulas as follows.
Once again, by unique readability, an assignment extends in a unique way to an assignment .
The idea of a sentence of was outlined in Definition 9.6. (A further web page on free variables explain this idea in more detail.) We claimed there that sentences are independent of any choice of meaning of variables. This can now be formally stated as a proposition and proved. In fact we will prove something slightly stronger.
Let be a formula of and be assignments such that for all variables that occur free in . Then .
By induction on , where the induction hypothesis is the statement of the proposition for all formulas that are constructed using a construction sequence of length at most . We do some of the steps here, leaving the remaining steps as exercises for the reader.
If is an atomic formula of type or then and can only depend on the values and for variables actually occuring in the terms . (A formal proof of this fact requires a proof by induction on terms!). Therefore as these values and are equal.
If is a quantified formula of the type then suppose . We must use the indution hypothesis applied to to show that . But means that for all we have . but for each such the assigment agrees with on all variables free in , since such a variable is either free in or else is itself and both these assignments give to . Therefore by the induction hypothesis and as this holds for all such this proves the induction step in this case. The case of of the type is similar.
Let be a sentence of and assignments. Then .
For a sentence of , we write to mean for every (equivalently some) assignment of variables into .