Proof theory

As with any logic, the semantics of first-order logic yield rules for deducing the truth of one sentence from that of another. In this chapter, we develop both formal proofs and resolution for first-order logic. As in propositional logic, each of these provides a systematic method for proving that one sentence is a consequence of another. Recall the Consequence problem for propositional logic. Given formulas F and G, the problemis to decide whether or not G is a consequence of F. From Chapter 1, we have three approaches to this problem: • We could compute the truth table for the formula F → G. If the truth values are all 1s then we conclude that F → G is a tautology and G is a consequence of F. Otherwise, G is not a consequence of F. • Using Tables 1.5 and 1.6, we could try to formally derive G from {F}. By the Completeness Theorem for propositional logic, G is a consequence of F if and only if {F} ├ G. • We could use resolution. By Theorem1.76, G is a consequence of F if and only if ∅ ∈ Res(H) where H is a formula in CNF equivalent to (F ∧￢G). Using these methods not only can we determine whether one formula is a consequence of another, but also we can determine whether a given formula is a tautology or a contradiction. A formula F is a tautology if and only if F is a consequence of (A∨￢A) if and only if ￢F is a contradiction. In this chapter, we consider the analogous problems for first-order logic. Given formulas φ and ψ, how can we determine whether ψ is a consequence of φ? Equivalently, how can we determine whether a given formula is a tautology or a contradiction? We present three methods for answering these questions. • In Section 3.1, we define a notion of formal proof for first-order logic by extending Table 1.5. • In Section 3.3, we “reduce” formulas of first-order logic to sets of formulas of propositional logic where we use resolution as defined in Chapter 1.

Structures and first-order logic

First-order logic is a richer language than propositional logic. Its lexicon contains not only the symbols ∧, ∨, ￢, →, and ↔ (and parentheses) from propositional logic, but also the symbols ∃ and ∀ for “there exists” and “for all,” along with various symbols to represent variables, constants, functions, and relations. These symbols are grouped into five categories. • Variables. Lower case letters from the end of the alphabet (. . . x, y, z) are used to denote variables. Variables represent arbitrary elements of an underlying set. This, in fact, is what “first-order” refers to. Variables that represent sets of elements are called second-order. Second-order logic, discussed in Chapter 9, is distinguished by the inclusion of such variables. • Constants. Lower case letters from the beginning of the alphabet (a, b, c, . . .) are usually used to denote constants. A constant represents a specific element of an underlying set. • Functions. The lower case letters f, g, and h are commonly used to denote functions. The arguments may be parenthetically listed following the function symbol as f(x1, x2, . . . , xn). First-order logic has symbols for functions of any number of variables. If f is a function of one, two, or three variables, then it is called unary, binary, or ternary, respectively. In general, a function of n variables is called n-ary and n is referred to as the arity of the function. • Relations. Capital letters, especially P, Q, R, and S, are used to denote relations. As with functions, each relation has an associated arity. We have an infinite number of each of these four types of symbols at our disposal. Since there are only finitely many letters, subscripts are used to accomplish this infinitude. For example, x1, x2, x3, . . . are often used to denote variables. Of course, we can use any symbol we want in first-order logic. Ascribing the letters of the alphabet in the above manner is a convenient convention. If you turn to a random page in this book and see “R(a, x, y),” you can safely assume that R is a ternary relation, x and y are variables, and a is a constant.

Finite model theory

This final chapter unites ideas from both model theory and complexity theory. Finite model theory is the part of model theory that disregards infinite structures. Examples of finite structures naturally arise in computer science in the form of databases, models of computations, and graphs. Instead of satisfiability and validity, finite model theory considers the following finite versions of these properties. • A first-order sentence is finitely satisfiable if it has a finite model. • A first-order sentence is finitely valid if every finite structure is a model. Finite model theory developed separately from the “classical” model theory of previous chapters. Distinct methods and logics are used to analyze finite structures. In Section 10.1, we consider various finite-variable logics that serve as useful languages for finite model theory. We define variations of the pebble games introduced in Section 9.2 to analyze the expressive power of these logics. Pebble games are one of the few tools from classical model theory that is useful for investigating finite structures. In Section 10.2, it is shown that many of the theorems from Chapter 4 are no longer true when restricted to finite models. There is no analog for the Completeness and Compactness theorems in finite model theory. Moreover, we prove Trakhtenbrot’s theorem which states that the set of finitely valid first-order sentences is not recursively enumerable. Descriptive complexity is the subject of 10.3. This subject describes the complexity classes discussed in Chapter 7 in terms of the logics introduced in Chapter 9. We prove Fagin’s theorem relating the class NP to existentional second-order logic. We prove the Cook–Levin theorem as a consequence of Fagin’s Theorem. This theorem states that the Satisfiability Problem for Propositional Logic is NP-complete. We conclude this chapter (and this book) with a section describing the close connection between logic and the P = NP problem. In this section, we discuss appropriate logics for the study of finite models. First-order logic, since it describes each finite model up to isomorphism, is too strong. For this reason, we must weaken the logic. It may seem counter-intuitive that we should gain knowledge by weakening our language.

First-order theories

We continue our study of Model Theory. This is the branch of logic concerned with the interplay between sentences of a formal language and mathematical structures. Primarily, Model Theory studies the relationship between a set of first-order sentences T and the class Mod(T) of structures that model T. Basic results of Model Theory were proved in the previous chapter. For example, it was shown that, in first-order logic, every model has a theory and every theory has a model. Put another way, T is consistent if and only if Mod(T) is nonempty. As a consequence of this, we proved the Completeness theorem. This theorem states that T ├ φ if and onlyif M ╞ φ for each M in Mod(T). So to study a theory T, we can avoid the concept of ├ and the methods of deduction introduced in Chapter 3, and instead work with the concept of ╞ and analyze the class Mod(T). More generally, we can go back and forth between the notions on the left side of the following table and their counterparts on the right. Progress in mathematics is often the result of having two or more points of view that are shown to be equivalent. A prime example is the relationship between the algebra of equations and the geometry of the graphs defined by the equations. Combining these two points of view yield concepts and results that would not be possible in either geometry or algebra alone. The Completeness theorem equates the two points of view exemplified in the above table. Model Theory exploits the relationship between these two points of view to investigate mathematical structures. First-order theories serve as our objects of study in this chapter. A first-order theory may be viewed as a consistent set of sentences T or as an elementary class of structures Mod(T). We shall present examples of theories and consider properties that the theories mayor may not possess such as completeness, categoricity, quantifier-elimination, and model-completeness. The properties that a theory possesses shed light on the structures that model the theory. We analyze examples of first-order structures including linear orders, vector spaces, the random graph, and the complex numbers.

Properties of first-order logic

We show that first-order logic, like propositional logic, has both completeness and compactness. We prove a countable version of these theorems in Section 4.1. We further show that these two properties have many useful consequences for first-order logic. For example, compactness implies that if a set of first-order sentences has an infinite model, then it has arbitrarily large infinite models. To fully understand completeness, compactness, and their consequences we must understand the nature of infinite numbers. In Section 4.2, we return to our discussion of infinite numbers that we left in Section 2.5. This digression allows us to properly state and prove completeness and compactness along with the Upward and Downward Löwenhiem–Skolem theorems. These are the four central theorems of first-order logic referred to in the title of Section 4.3. We discuss consequences of these theorems in Sections 4.4–4.6. These consequences include amalgamation theorems, preservation theorems, and the Beth Definability theorem. Each of the properties studied in this chapter restrict the language of first-order logic. First-order logic is, in some sense, weak. There are many concepts that cannot be expressed in this language. For example, whereas first-order logic can express “there exist n elements” for any finite n, it cannot express “there exist countably many elements.” Any sentence having a countable model necessarily has uncountable models. As we previously mentioned, this follows from compactness. In the final section of this chapter, using graphs as an illustration, we discuss the limitations of first-order logic. Ironically, the weakness of first-order logic makes it the fruitful logic that it is. The properties discussed in this chapter, and the limitations that follow from them, make possible the subject of model theory. All formulas in this chapter are first-order unless stated otherwise. Many of the properties of first-order logic, including completeness and compactness, are consequences of the following fact: Every model has a theory and every theory has a model. Recall that a set of sentences is a “theory” if it is consistent (i.e. if we cannot derive a contradiction). “Every theory has a model” means that if a set of sentences is consistent, then it is satisfiable.

Beyond first-order logic

We consider various extensions of first-order logic. Informally, a logic 𝓛 is an extension of first-order logic if every sentence of first-order logic is also a sentence of 𝓛. We also require that 𝓛 is closed under conjunction and negation and has other basic properties of a logic. In Section 9.4, we list the properties that formally define the notion of an extension of first-order logic. Prior to Section 9.4, we provide various natural examples of such extensions. In Sections 9.1–9.3, we consider, respectively, second-order logic, infinitary logics, and logics with fixed-point operators. We do not provide a thorough treatment of any one of these logics. Indeed, we could easily devote an entire chapter to each. Rather, we define each logic and provide examples that demonstrate the expressive power of the logics. In particular, we show that none of these logics has compactness. In the final Section 9.4, we prove that if a proper extension of first-order logic has compactness, then the Downward Löwenhiem–Skolem theorem must fail for that logic. This is Lindstrom’s theorem. The Compactness theorem and Downward Löwenheim–Skolem theorem are two crucial results for model theory. Every property of first-order logic from Chapter 4 is a consequence of these two theorems. Lindström’s theorem implies that the only extension of first-order logic possessing these properties is first-order logic itself. Second-order logic is the extension of first-order logic that allows quantification of relations. The symbols of second-order logic are the same symbols used in first-order logic. The syntax of second-order logic is defined by adding one rule to the syntax of first-order logic. The additional rule makes second-order logic far more expressive than first-order logic. Specifically, the syntax of second-order logic is defined as follows. Any atomic first-order formula is a formula of second-order logic. Moreover, we have the following four rules: (R1) If φ is a formula then so is ￢φ. (R2) If φ and ψ are formulas then so is φ ∧ ψ. (R3) If φ is a formula, then so is ∃x φ for any variable x.

The incompleteness theorems

In this chapter we prove that the structure N = (ℕ|+, · , 1) has a first-order theory that is undecidable. This is a special case of Gödel’s First Incompleteness theorem. This theorem implies that any theory (not necessarily first-order) that describes elementary arithmetic on the natural numbers is necessarily undecidable. So there is no algorithm to determine whether or not a given sentence is true in the structure N. As we shall show, the existence of such an algorithm leads to a contradiction. Gödel’s Second Incompleteness theorem states that any decidable theory (not necessarily first-order) that can express elementary arithmetic cannot prove its own consistency. We shall make this idea precise and discuss the Second Incompleteness theorem in Section 8.5. Gödel’s First Incompleteness theorem is proved in Section 8.3. Although they are purely mathematical results, Gödel’s Incompleteness theorems have had undeniable philosophical implications. Gödel’s theorems dispelled commonly held misconceptions regarding the nature of mathematics. A century ago, some of the most prominent mathematicians and logicians viewed mathematics as a branch of logic instead of the other way around. It was thought that mathematics could be completely formalized. It was believed that mathematical reasoning could, at least in principle, be mechanized. Alfred North Whitehead and Bertrand Russell envisioned a single system that could be used to derive and enumerate all mathematical truths. In their three-volume Principia Mathematica, Russell and Whitehead rigorously define a system and use it to derive numerous known statements of mathematics. Gödel’s theorems imply that any such system is doomed to be incomplete. If the system is consistent (which cannot be proved within the system by Gödel’s Second theorem), then there necessarily exist true statements formulated within the system that the system cannot prove (by Gödel’s First theorem). This explains why the name “incompleteness” is attributed to these theorems and why the title of Gödel’s 1931 paper translates (from the original German) to “On Formally Undecidable Propositions of Principia Mathematica and Related Systems” (translated versions appear in both [13] and [14]). Depending on one’s point of view, it may or may not be surprising that there is no algorithm to determine whether or not a given sentence is true in N.

Models of countable theories

We define and study types of a complete first-order theory T. This concept allows us to refine our analysis of Mod(T). If T has few types, then Mod(T) contains a uniquely defined smallest model that can be elementarily embedded into any structure of Mod(T). We investigate the various properties of these small models in Section 6.3. In Section 6.4, we consider the “big” models of Mod(T). For any theory, the number of types is related to the number of models of the theory. For any cardinal κ, I(T, κ) denotes the number of models in Mod(T) of size κ. We prove two basic facts regarding this cardinal function. In Section 6.5, we show that if T has many types, then I(T, κ) takes on its maximal possible value of 2κ for each infinite κ. In Section 6.6, we prove Vaught’s theorem stating that I(T, ℵ0) cannot equal 2. All formulas are first-order formulas. All theories are sets of first-order sentences. For any structure M, we conveniently refer to an n-tuple of elements from the underlying set of M as an “n-tuple of M.” The notion of a type extends the notion of a theory to include formulas and not just sentences. Whereas theories describe structures, types describe elements within a structure. Definition 6.1 Let M be a ν-structure and let ā = (a1, . . . , an) be an n-tuple of M. The type of ā in M, denoted tpM(ā), is the set of all ν-formulas φ having free variables among x1, . . . , xn that hold in M when each xi in is replaced by ai. More concisely, but less precisely: If ā is an n-tuple, then each formula in tpM(ā) contains at most n free variables but may contain fewer. In particular, the type of an n-tuple contains sentences. For any structure M and tuple ā of M, tpM(ā) contains Th(M) as a subset. The set tpM(ā) provides the complete first-order description of the tuple ā and how it sits in M.

Computability and complexity

In this chapter we study two related areas of theoretical computer science: computability theory and computational complexity. Each of these subjects take mathematical problems as objects of study. The aim is not to solve these problems, but rather to classify them by level of difficulty. Time complexity classifies a given problem according to the length of time required for a computer to solve the problem. The polynomial-time problems P and the nondeterministic polynomial-time problems NP are the two most prominent classes of time complexity. Some problems cannot be solved by the algorithmic process of a computer. We refer to problems as decidable or undecidable according to whether or not there exists an algorithm that solves the problem. Computability theory considers undecidable problems and the brink between the undecidable and the decidable. There are only countably many algorithms and uncountably many problems to solve. From this fact we deduce that most problems are not decidable. To proceed beyond this fact, we must state precisely what we mean by an “algorithm” and a “problem.” One of the aims of this chapter is to provide a formal definition for the notion of an algorithm. The types of problems we shall consider are represented by the following examples. • The even problem: Given an n ∈ ℕ, determine whether or not n is even. • The 10-clique problem: Given finite graph, determine whether or not there exists a subgraph that is isomorphic to the 10-clique. • The satisfiability problem for first-order logic: Given a sentence of first-order logic, determine whether or not it is satisfiable. The first problem is quite easy. To determine whether a given number is even, we simply check whether the last digit of the number is 0, 2, 4, 6 or 8. The second problem is harder. If the given graph is large and does contain a 10-clique as a subgraph, then we may have to check many subsets of the graph before we find it. Time complexity gives precise meaning to the ostensibly subjective idea of one problem being “harder” than another. The third problem is the most difficult of the three problems.

Propositional logic

In propositional logic, atomic formulas are propositions. Any assertion will do. For example, . . . A = “Aristotle is dead,” B = “Barcelona is on the Seine,” and C = “Courtney Love is tall” . . . are atomic formulas. Atomic formulas are the building blocks used to construct sentences. In any logic, a sentence is regarded as a particular type of formula. In propositional logic, there is no distinction between these two terms. We use “formula” and “sentence” interchangeably. In propositional logic, as with all logics we study, each sentence is either true or false. A truth value of 1 or 0 is assigned to the sentence accordingly. In the above example, we may assign truth value 1 to formula A and truth value 0 to formula B. If we take proposition C literally, then its truth is debatable. Perhaps it would make more sense to allow truth values between 0 and 1. We could assign 0.75 to statement C if Miss Love is taller than 75% of American women. Fuzzy logic allows such truth values, but the classical logics we study do not. In fact, the content of the propositions is not relevant to propositional logic. Henceforth, atomic formulas are denoted only by the capital letters A, B, C,. . . (possibly with subscripts) without referring to what these propositions actually say. The veracity of these formulas does not concern us. Propositional logic is not the study of truth, but of the relationship between the truth of one statement and that of another. The language of propositional logic contains words for “not,” “and,” “or,” “implies,” and “if and only if.” These words are represented by symbols: . . . ￢ for “not,” ∧ for “and,” ∨ for “or,” → for “implies,” and ↔ for “if and only if.” . . . As is always the case when translating one language into another, this correspondence is not exact. Unlike their English counterparts, these symbols represent concepts that are precise and invariable. The meaning of an English word, on the other hand, always depends on the context.