Introduction to First-Order Logic — Read

First-Order Logic

You are probably familiar with first-order logic from your first introduction to formal logic.In fact, we more or less assume you are! If you're not, you could review a more elementary textbook, such as forall x (P. D. Magnus and Tim Button and J. Robert Loftis and Aaron Thomas-Bolduc and Robert Trueman and Richard Zach, 2021). You may know it as “quantificational logic” or “predicate logic.” First-order logic, first of all, is a formal language. That means, it has a certain vocabulary, and its expressions are strings from this vocabulary. But not every string is permitted. There are different kinds of permitted expressions: terms, formulas, and sentences. We are mainly interested in sentences of first-order logic: they provide us with a formal analogue of sentences of English, and about them we can ask the questions a logician typically is interested in. For instance:

• Does $B$source 27 follow from $A$source 27 logically?

• Is $A$source 28 logically true, logically false, or contingent?

• Are $A$source 30 and $B$source 30 equivalent?

These questions are primarily questions about the “meaning” of sentences of first-order logic. For instance, a philosopher would analyze the question of whether $B$source 35 follows logically from $A$source 35 as asking: is there a case where $A$source 36 is true but $B$source 36 is false ($B$source 36 doesn't follow from $A$source 37), or does every case that makes $A$source 37 true also make $B$source 38 true ($B$source 38 does follow from $A$source 38)? But we haven't been told yet what a “case” is—that is the job of semantics. The semantics of first-order logic provides a mathematically precise model of the philosopher's intuitive idea of “case,” and also—and this is important—of what it is for a sentence $A$source 42 to be true in a case. We call the mathematically precise model that we will develop a structure. The relation which makes “true in” precise, is called the relation of satisfaction. So what we will define is “$A$source 46 is satisfied in $M$source 46” (in symbols: $M\models A$source 46) for sentences $A$source 47 and structures $M$source 47. Once this is done, we can also give precise definitions of the other semantical terms such as “follows from” or “is logically true.” These definitions will make it possible to settle, again with mathematical precision, whether, e.g., $\forall x\left(A\right(x)\to B(x\left)\right),\exists xA\left(x\right)\models \exists xB\left(x\right)$source 51 (Reader correction: The source closes the universal scope only after the entailment. The reader rendering places that bracket before the premise comma and removes the resulting extra final bracket). The answer will, of course, be “yes.” If you've already been trained to symbolize sentences of English in first-order logic, you will recognize this as, e.g., the symbolizations of, say, “All ants are insects, there are ants, therefore there are insects.” That is obviously a valid argument, and so our mathematical model of “follows from” for our formal language should give the same answer.

Another topic you probably remember from your first introduction to formal logic is that there are derivations. If you have taken a first formal logic course, your instructor will have made you practice finding such derivations, perhaps even a derivation that shows that the above entailment holds. There are many different ways to give derivations: you may have done something called “natural deduction” or “truth trees,” but there are many others. The purpose of derivation systems is to provide tools using which the logicians' questions above can be answered: e.g., a natural deduction derivation in which $\forall x\left(A\right(x)\to B(x\left)\right)$source 69 (Reader correction: The source fragment omits the closing scope bracket of the universal formula. The reader rendering supplies that bracket explicitly) and $\exists xA\left(x\right)$source 70 are premises and $\exists xB\left(x\right)$source 70 (Reader correction: The source fragment contains one extra closing scope bracket. The reader rendering removes that extra bracket explicitly) is the conclusion (last line) verifies that $\exists xB\left(x\right)$source 71 logically follows from $\forall x\left(A\right(x)\to B(x\left)\right)$source 72 and $\exists xA\left(x\right)$source 73.

But why is that? On the face of it, derivation systems have nothing to do with semantics: giving a formal derivation merely involves arranging symbols in certain rule-governed ways; they don't mention “cases” or “true in” at all. The connection between derivation systems and semantics has to be established by a meta-logical investigation. What's needed is a mathematical proof, e.g., that a formal derivation of $\exists xB\left(x\right)$source 80 from premises $\forall x\left(A\right(x)\to B(x\left)\right)$source 81 and $\exists xA\left(x\right)$source 82 is possible, if, and only if, $\forall x\left(A\right(x)\to B(x\left)\right)$source 82 (Reader correction: The source fragment omits the closing scope bracket of the universal formula. The reader rendering supplies that bracket explicitly) and $\exists xA\left(x\right)$source 83 together entail $\exists xB\left(x\right)$source 84 (Reader correction: The source fragment contains one extra closing scope bracket. The reader rendering removes that extra bracket explicitly). Before this can be done, however, a lot of painstaking work has to be carried out to get the definitions of syntax and semantics correct.

Syntax

We first must make precise what strings of symbols count as sentences of first-order logic. We'll do this later; for now we'll just proceed by example. The basic building blocks—the vocabulary—of first-order logic divides into two parts. The first part is the symbols we use to say specific things or to pick out specific things. We pick out things using constants, and we say stuff about the things we pick out using predicates. E.g, we might use $a$source 20 as a constant to pick out a single thing, and then say something about it using the sentence $P\left(a\right)$source 21. If you have meanings for “$a$source 22” and “$P$source 22” in mind, you can read $P\left(a\right)$source 23 as a sentence of English (and you probably have done so when you first learned formal logic). Once you have such simple sentences of first-order logic, you can build more complex ones using the second part of the vocabulary: the logical symbols (connectives and quantifiers). So, for instance, we can form expressions like $(P\left(a\right)\wedge Q\left(b\right))$source 28 or $\exists xP\left(x\right)$source 29.

In order to provide the precise definitions of semantics and the rules of our derivation systems required for rigorous meta-logical study, we first of all have to give a precise definition of what counts as a sentence of first-order logic. The basic idea is easy enough to understand: there are some simple sentences we can form from just predicates and constants, such as $P\left(a\right)$source 36. And then from these we form more complex ones using the connectives and quantifiers. But what exactly are the rules by which we are allowed to form more complex sentences? These must be specified, otherwise we have not defined “sentence of first-order logic” precisely enough. There are a few issues. The first one is to get the right strings to count as sentences. The second one is to do this in such a way that we can give mathematical proofs about all sentences. Finally, we'll have to also give precise definitions of some rudimentary operations with sentences, such as “replace every $x$source 46 in $A$source 46 by $b$source 46.” The trouble is that the quantifiers and variables we have in first-order logic make it not entirely obvious how this should be done. E.g., should $\exists xP\left(a\right)$source 48 count as a sentence? What about $\exists x\exists xP\left(x\right)$source 50? What should the result of “replace $x$source 51 by $b$source 51 in $(P\left(x\right)\wedge \exists xP\left(x\right))$source 51” be?

Formulas

Here is the approach we will use to rigorously specify sentences of first-order logic and to deal with the issues arising from the use of variables. We first define a different set of expressions: formulas. Once we've done that, we can consider the role variables play in them—and on the basis of some other ideas, namely those of “free” and “bound” variables, we can define what a sentence is (namely, a formula without free variables). We do this not just because it makes the definition of “sentence” more manageable, but also because it will be crucial to the way we define the semantic notion of satisfaction.

Let's define “formula” for a simple first-order language, one containing only a single predicate $P$source 25 and a single constant $a$source 26, and only the logical symbols $\neg$source 26, $\wedge$source 26, and $\exists$source 27. Our full definitions will be much more general: we'll allow infinitely many predicates and constants. In fact, we will also consider functions which can be combined with constants and variables to form “terms.” For now, $a$source 30 and the variables will be our only terms. We do need infinitely many variables. We'll officially use the symbols $v_0$source 32, $v_1$source 32, …, as variables.

the atomic-formula clause tells us that $P\left(a\right)$source 54 and $P\left(v_i\right)$source 55 are formulas, for any $i\in \mathbb{N}$source 55. These are the so-called atomic formulas. They give us something to start from. The other clauses give us ways of forming new formulas from ones we have already formed. So for instance, by the negation clause, we get that $\neg P\left(v_2\right)$source 59 is a formula, since $P\left(v_2\right)$source 60 is already a formula by the atomic-formula clause. Then, by the existential-quantifier clause, we get that $\exists v_2\neg P\left(v_2\right)$source 62 is another formula, and so on. the limiting clause tells us that only strings we can form in this way count as formulas. In particular, $\exists v_{0}P\left(a\right)$source 65 and $\exists v_0\exists v_{0}P\left(a\right)$source 65 do count as formulas, and $(\neg P\left(a\right))$source 67 does not, because of the extraneous outer parentheses.

This way of defining formulas is called an inductive definition, and it allows us to prove things about formulas using a version of proof by induction called structural induction. These are discussed in a general way in the section on inductive definitions and the section on structural induction, which you should review before delving into the proofs later on. Basically, the idea is that if you want to give a proof that something is true for all formulas, you show first that it is true for the atomic formulas, and then that if it's true for any formula $A$source 78 (and $B$source 78), it's also true for $\neg A$source 79, $(A\wedge B)$source 79, and $\exists xA$source 80. For instance, this proves that it's true for $\exists v_2\neg P\left(v_2\right)$source 81: from the first part you know that it's true for the atomic formula $P\left(v_2\right)$source 82. Then you get that it's true for $\neg P\left(v_2\right)$source 83 by the second part, and then again that it's true for $\exists v_2\neg P\left(v_2\right)$source 85 itself. Since all formulas are inductively generated from atomic formulas, this works for any of them.

Satisfaction

We can already skip ahead to the semantics of first-order logic once we know what formulas are: here, the basic definition is that of a structure. For our simple language, a structure $M$source 15 has just three components: a non-empty set $\left|M\right|$source 16 called the domain, what $a$source 17 picks out in $M$source 17, and what $P$source 18 is true of in $M$source 18. The object picked out by $a$source 18 is denoted $a^M$source 19 and the set of things $P$source 19 is true of by $P^M$source 20. A structure $M$source 20 consists of just these three things: $\left|M\right|$source 21, $a^M\in \left|M\right|$source 21 and $P^M\subseteq \left|M\right|$source 22. The general case will be more complicated, since there will be many predicates and constants, the constants can have more than one place, and Reader correction TR015-SOURCE-PROSE-CORRECTION-001: In the general case there may be many predicates and constants; predicate or relation symbols, not individual constants, can have more than one place. there will also be functions.

This is enough to give a definition of satisfaction for formulas that don't contain variables. The idea is to give an inductive definition that mirrors the way we have defined formulas. We specify when an atomic formula is satisfied in $M$source 30, and then when, e.g., $\neg A$source 31 is satisfied in $M$source 31 on the basis of whether or not $A$source 32 is satisfied in $M$source 32. E.g., we could define:

1. $P\left(a\right)$source 35 is satisfied in $M$source 35 iff $a^M\in P^M$source 36.

2. $\neg A$source 37 is satisfied in $M$source 37 iff $A$source 37 is not satisfied in $M$source 38.

3. $(A\wedge B)$source 39 is satisfied in $M$source 39 iff $A$source 39 is satisfied in $M$source 40, and $B$source 40 is satisfied in $M$source 40 as well.

Let's say that $\left|M\right|=\{0,1,2\}$source 43, $a^M=1$source 43, and $P^M=\{1,2\}$source 44. This definition would tell us that $P\left(a\right)$source 45 is satisfied in $M$source 45 (since $a^M=1\in \{1,2\}=P^M$source 46). It tells us further that $\neg P\left(a\right)$source 47 is not satisfied in $M$source 48, and that in turn $\neg \neg P\left(a\right)$source 48 is and $(\neg P\left(a\right)\wedge P\left(a\right))$source 49 is not satisfied, and so on.

The trouble comes when we want to give a definition for the quantifiers: we'd like to say something like, “$\exists v_{0}P\left(v_0\right)$source 53 is satisfied iff $P\left(v_0\right)$source 54 is satisfied.” But the structure $M$source 55 doesn't tell us what to do about variables. What we actually want to say is that $P\left(v_0\right)$source 57 is satisfied for some value of $v_0$source 58. To make this precise we need a way to assign elements of $\left|M\right|$source 59 not just to $a$source 59 but also to $v_0$source 59. To this end, we introduce variable assignments. A variable assignment is simply a function $s$source 61 that maps variables to elements of $\left|M\right|$source 62 (in our example, to one of $1$source 63, $2$source 63, or $3$source 63). Reader correction TR015-SOURCE-PROSE-CORRECTION-002: In this example the assignment values are zero, one, or two, the elements of the domain fixed above. Since we don't know beforehand which variables might appear in a formula we can't limit which variables $s$source 65 assigns values to. The simple solution is to require that $s$source 66 assigns values to all variables $v_0$source 66, $v_1$source 67, … We'll just use only the ones we need.

Instead of defining satisfaction of formulas just relative to a structure, we'll define it relative to a structure $M$source 71 and a variable assignment $s$source 71, and write $M,s\models A$source 72 for short. Our definition will now include an additional clause to deal with atomic formulas containing variables:

1. $M,s\models P\left(a\right)$source 76 iff $a^M\in P^M$source 77.

2. $M,s\models P\left(v_i\right)$source 78 iff $s\left(v_i\right)\in P^M$source 79.

3. $M,s\models \neg A$source 80 iff not $M,s\models A$source 80.

4. $M,s\models (A\wedge B)$source 81 iff $M,s\models A$source 81 and $M,s\models B$source 81.

Ok, this solves one problem: we can now say when $M$source 83 satisfies $P\left(v_0\right)$source 84 for the value $s\left(v_0\right)$source 84. To get the definition right for $\exists v_{0}P\left(v_0\right)$source 85 we have to do one more thing: We want to have that $M,s\models \exists v_{0}P\left(v_0\right)$source 87 iff $M,s\text{'}\models P\left(v_0\right)$source 88 for some way $s\text{'}$source 88 of assigning a value to $v_0$source 89. But the value assigned to $v_0$source 89 does not necessarily have to be the value that $s\left(v_0\right)$source 90 picks out. We'll introduce a notation for that: if $m\in \left|M\right|$source 91, then we let $s[m/v_0]$source 92 be the assignment that is just like $s$source 93 (for all variables other than $v_0$source 93), except to $v_0$source 94 it assigns $m$source 94. Now our definition can be:

5. $M,s\models \exists v_{i}A$source 96 iff $M,s[m/v_i]\models A$source 97 for some $m\in \left|M\right|$source 97.

Does it work out? Let's say we let $s\left(v_i\right)=0$source 99 for all $i\in \mathbb{N}$source 99. $M,s\models \exists v_{0}P\left(v_0\right)$source 100 iff there is an $m\in \left|M\right|$source 101 so that $M,s[m/v_0]\models P\left(v_0\right)$source 101. And there is: we can choose $m=1$source 102 or $m=2$source 103. Note that this is true even if the value $s\left(v_0\right)$source 103 assigned to $v_0$source 104 by $s$source 104 itself—in this case, $0$source 104—doesn't do the job. We have $M,s[1/v_0]\models P\left(v_0\right)$source 105 but not $M,s\models P\left(v_0\right)$source 106.

If this looks confusing and cumbersome: it is. But the added complexity is required to give a precise, inductive definition of satisfaction for all formulas, and we need something like it to precisely define the semantic notions. There are other ways of doing it, but they are all equally (in)elegant.

Sentences

Ok, now we have a (sketch of a) definition of satisfaction (“true in”) for structures and formulas. But it needs this additional bit—a variable assignment—and what we wanted is a definition of sentences. How do we get rid of assignments, and what are sentences?

You probably remember a discussion in your first introduction to formal logic about the relation between variables and quantifiers. A quantifier is always followed by a variable, and then in the part of the sentence to which that quantifier applies (its “scope”), we understand that the variable is “bound” by that quantifier. In formulas it was not required that every variable has a matching quantifier, and variables without matching quantifiers are “free” or “unbound.” We will take sentences to be all those formulas that have no free variables.

Again, the intuitive idea of when an occurrence of a variable in a formula $A$source 30 is bound, which quantifier binds it, and when it is free, is not difficult to get. You may have learned a method for testing this, perhaps involving counting parentheses. We have to insist on a precise definition—and because we have defined formulas by induction, we can give a definition of the free and bound occurrences of a variable $x$source 35 in a formula $A$source 35 also by induction. E.g., it might look like this for our simplified language:

1. If $A$source 38 is atomic, all occurrences of $x$source 38 in it are free (that is, the occurrence of $x$source 39 in $P\left(x\right)$source 39 is free).

2. If $A$source 40 is of the form $\neg B$source 40, then an occurrence of $x$source 40 in $\neg B$source 41 is free iff the corresponding occurrence of $x$source 41 is free in $B$source 42 (that is, the free occurrences of variables in $B$source 42 are exactly the corresponding occurrences in $\neg B$source 43).

3. If $A$source 44 is of the form $(B\wedge C)$source 44, then an occurrence of $x$source 44 in $(B\wedge C)$source 45 is free iff the corresponding occurrence of $x$source 45 is free in $B$source 46 or in $C$source 46.

4. If $A$source 47 is of the form $\exists xB$source 47, then no occurrence of $x$source 48 in $A$source 48 is free; if it is of the form $\exists yB$source 48 where $y$source 49 is a different variable than $x$source 49, then an occurrence of $x$source 49 in $\exists yB$source 50 is free iff the corresponding occurrence of $x$source 50 is free in $B$source 51.

Once we have a precise definition of free and bound occurrences of variables, we can simply say: a sentence is any formula without free occurrences of variables.

Semantic Notions

We mentioned above that when we consider whether $M,s\models A$source 13 holds, we (for convenience) let $s$source 14 assign values to all variables, but only the values it assigns to variables in $A$source 15 are used. In fact, it's only the values of free variables in $A$source 16 that matter. Of course, because we're careful, we are going to prove this fact. Since sentences have no free variables, $s$source 18 doesn't matter at all when it comes to whether or not they are satisfied in a structure. So, when $A$source 20 is a sentence we can define $M\models A$source 21 to mean “$M,s\models A$source 21 for all $s$source 21,” which as it happens is true iff $M,s\models A$source 22 for at least one $s$source 22. We need to introduce variable assignments to get a working definition of satisfaction for formulas, but for sentences, satisfaction is independent of the variable assignments.

Once we have a definition of “$M\models A$source 27,” we know what “case” and “true in” mean as far as sentences of first-order logic are concerned. On the basis of the definition of $M\models A$source 29 for sentences we can then define the basic semantic notions of validity, entailment, and satisfiability. A sentence is valid, $\models A$source 32, if every structure satisfies it. It is entailed by a set of sentences, $\Gamma \models A$source 33, if every structure that satisfies all the sentences in $\Gamma$source 34 also satisfies $A$source 34. And a set of sentences is satisfiable if some structure satisfies all sentences in it at the same time.

Because formulas are inductively defined, and satisfaction is in turn defined by induction on the structure of formulas, we can use induction to prove properties of our semantics and to relate the semantic notions defined. We'll collect and prove some of these properties, partly because they are individually interesting, but mainly because many of them will come in handy when we go on to investigate the relation between semantics and derivation systems. In order to do so, we'll also have to define (precisely, i.e., by induction) some syntactic notions and operations we haven't mentioned yet.

Substitution

We'll discuss an example to illustrate how things hang together, and how the development of syntax and semantics lays the foundation for our more advanced investigations later. Our derivation systems should let us derive $P\left(a\right)$source 16 from $\forall v_{0}P\left(v_0\right)$source 16 (Reader correction: The source closes the universal scope before the argument of the atomic formula. The reader rendering keeps that argument inside the atom and the quantified scope). Maybe we even want to state this as a rule of inference. However, to do so, we must be able to state it in the most general terms: not just for $P$source 19, $a$source 19, and $v_0$source 19, but for any formula $A$source 20, and term $t$source 20, and variable $x$source 21. (Recall that constants are terms, but we'll consider also more complicated terms built from constants and functions.) So we want to be able to say something like, “whenever you have derived $\forall xA\left(x\right)$source 24 you are justified in inferring $A\left(t\right)$source 25—the result of removing $\forall x$source 25 and replacing $x$source 26 by $t$source 26.” But what exactly does “replacing $x$source 26 by $t$source 26” mean? What is the relation between $A\left(x\right)$source 27 and $A\left(t\right)$source 27? Does this always work?

To make this precise, we define the operation of substitution. Substitution is actually tricky, because we can't just replace all $x$source 32's in $A$source 32 by $t$source 32, and not every $t$source 32 can be substituted for any $x$source 33. We'll deal with this, again, using inductive definitions. But once this is done, specifying an inference rule as “infer $A\left(t\right)$source 34 from $\forall xA\left(x\right)$source 35” becomes a precise definition. Moreover, we'll be able to show that this is a good inference rule in the sense that $\forall xA\left(x\right)$source 37 entails $A\left(t\right)$source 37. But to prove this, we have to again prove something that may at first glance prompt you to ask “why are we doing this?” That $\forall xA\left(x\right)$source 39 entails $A\left(t\right)$source 39 relies on the fact that whether or not $M\models A\left(t\right)$source 40 holds depends only on the value of the term $t$source 41, i.e., if we let $m$source 41 be whatever element of $\left|M\right|$source 42 is picked out by $t$source 42, then $M,s\models A\left(t\right)$source 43 iff $M,s[m/x]\models A\left(x\right)$source 43. This holds even when $t$source 44 contains variables, but we'll have to be careful with how exactly we state the result.

Models and Theories

Once we've defined the syntax and semantics of first-order logic, we can get to work investigating the properties of structures and the semantic notions. We can also define derivation systems, and investigate those. For a set of sentences, we can ask: what structures make all the sentences in that set true? Given a set of sentences $\Gamma$source 18, a structure $M$source 18 that satisfies them is called a model of $\Gamma$source 19. We might start from $\Gamma$source 20 and try to find its models—what do they look like? How big or small do they have to be? But we might also start with a single structure or collection of structures and ask: what sentences are true in them? Are there sentences that characterize these structures in the sense that they, and only they, are true in them? These kinds of questions are the domain of model theory. They also underlie the axiomatic method: describing a collection of structures by a set of sentences, the axioms of a theory. This is made possible by the observation that exactly those sentences entailed in first-order logic by the axioms are true in all models of the axioms.

As a very simple example, consider preorders. A preorder is a relation $R$source 33 on some set $A$source 33 which is both reflexive and transitive. A set $A$source 34 with a two-place relation $R\subseteq A\times A$source 34 on it is exactly what we would need to give a structure for a first-order language with a single two-place relation symbol $P$source 36: we would set $\left|M\right|=A$source 37 and $P^M=R$source 37. Since $R$source 37 is a preorder, it is reflexive and transitive, and we can find a set $\Gamma$source 39 of sentences of first-order logic that say this: First-order axioms for a reflexive and transitive relation $$\begin{gathered} \forall v_{0}P\left(v_0,v_0\right) \\ \forall v_0\forall v_1\forall v_2\left(\right(P\left(v_0,v_1\right)\wedge P\left(v_1,v_2\right))\to P\left(v_0,v_2\right)) \end{gathered}$$source 40 These sentences are just the symbolizations of “for any $x$source 44, $\mathrm{Rxx}$source 45” ($R$source 45 is reflexive) and “whenever $\mathrm{Rxy}$source 45 and $\mathrm{Ryz}$source 45 then also $\mathrm{Rxz}$source 46” ($R$source 46 is transitive). We see that a structure $M$source 46 is a model of these two sentences $\Gamma$source 47 iff $R$source 47 (i.e., $P^M$source 48), is a preorder on $A$source 48 (i.e., $\left|M\right|$source 48). In other words, the models of $\Gamma$source 49 are exactly the preorders. Any property of all preorders that can be expressed in the first-order language with just $P$source 51 as predicate (like reflexivity and transitivity above), is entailed by the two sentences in $\Gamma$source 52 and vice versa. So anything we can prove about models of $\Gamma$source 53 we have proved about all preorders.

For any particular theory and class of models (such as $\Gamma$source 56 and all preorders), there will be interesting questions about what can be expressed in the corresponding first-order language, and what cannot be expressed. There are some properties of structures that are interesting for all languages and classes of models, namely those concerning the size of the domain. One can always express, for instance, that the domain contains exactly $n$source 62 elements, for any $n\in {\mathbb{Z}}_{>0}$source 63. One can also express, using a set of infinitely many sentences, that the domain is infinite. But one cannot express that the domain is finite, or that the domain is nonenumerable. These results about the limitations of first-order languages are consequences of the compactness and Löwenheim–Skolem theorems.

Soundness and Completeness

We'll also introduce derivation systems for first-order logic. There are many derivation systems that logicians have developed, but they all define the same derivability relation between sentences. We say that $\Gamma$source 16 derives $A$source 16, $\Gamma ⊢A$source 16, if there is a derivation of a certain precisely defined sort. Derivations are always finite arrangements of symbols—perhaps a list of sentences, or some more complicated structure. The purpose of derivation systems is to provide a tool to determine if a sentence is entailed by some set $\Gamma$source 21. In order to serve that purpose, it must be true that $\Gamma \models A$source 22 if, and only if, $\Gamma ⊢A$source 22.

If $\Gamma ⊢A$source 25 but not $\Gamma \models A$source 25, our derivation system would be too strong, prove too much. The property that if $\Gamma ⊢A$source 26 then $\Gamma \models A$source 27 is called soundness, and it is a minimal requirement on any good derivation system. On the other hand, if $\Gamma \models A$source 29 but not $\Gamma ⊢A$source 29, then our derivation system is too weak, it doesn't prove enough. The property that if $\Gamma \models A$source 31 then $\Gamma ⊢A$source 31 is called completeness. Soundness is usually relatively easy to prove (by induction on the structure of derivations, which are inductively defined). Completeness is harder to prove.

Soundness and completeness have a number of important consequences. If a set of sentences $\Gamma$source 37 derives a contradiction (such as $A\wedge \neg A$source 38) it is called inconsistent. Inconsistent $\Gamma$source 39s cannot have any models, they are unsatisfiable. From completeness the converse follows: any $\Gamma$source 40 that is not inconsistent—or, as we will say, consistent—has a model. In fact, this is equivalent to completeness, and is the form of completeness we will actually prove. It is a deep and perhaps surprising result: just because you cannot prove $A\wedge \neg A$source 44 from $\Gamma$source 45 guarantees that there is a structure that is as $\Gamma$source 46 describes it. So completeness gives an answer to the question: which sets of sentences have models? Answer: all and only consistent sets do.

The soundness and completeness theorems have two important consequences: the compactness and the Löwenheim–Skolem theorem. These are important results in the theory of models, and can be used to establish many interesting results. We've already mentioned two: first-order logic cannot express that the domain of a structure is finite or that it is nonenumerable.

Historically, all of this—how to define syntax and semantics of first-order logic, how to define good derivation systems, how to prove that they are sound and complete, getting clear about what can and cannot be expressed in first-order languages—took a long time to figure out and get right. We now know how to do it, but going through all the details can still be confusing and tedious. But it's also important, because the methods developed here for the formal language of first-order logic are applied all over the place in logic, computer science, and linguistics. So working through the details pays off in the long run.