Automated Reasoning in Higher Order Logic
This page was created and is maintained by Chad E Brown.
Chapter 2: Syntax of First-Order Languages.
Chapter 3: Semantics of First-Order Languages.
Chapter 4: A Sequent Calculus.
Chapter 5: The Completeness Theorem.
Chapter 6: The Lowenheim-Skolem Theorem and the Compactness Theorem.
Chapter 7: The Scope of First-Order Logic.
Chapter 8: Appendix [to Part A].
Chapter 9: Extensions of First-Order Logic.
Chapter 10: Limitations of the Formal Method.
Chapter 11: An Algebraic Characterization of Elementary Equivalence.
Chapter 12: Characterizing First-Order Logic.
Part A.
Chapter 1: Introduction--provides motivational text (distinguishing between traditional philosophical logic and mathematical logic) and motivational examples (group theory and equivalence relations). The idea behind Godel's Completeness Theorem is explained, with an intuitive idea of "propositions," (semantic) "consequences," and "proofs." Also, an outline of the material after Godel's Completeness Theorem is given. The authors claim to show that first-order logic is a "best possible language." However, this assumes the point of view that first-order semantics are the only appropriate notion of semantics.
Chapter 2: Syntax of First-Order Languages--The standard material is covered: alphabets, strings, countability of languages, first-order languages (terms/formulas), induction "in the calculus of terms and in the calculus of formulas" (what Andrews calls "induction on the construction of a wff"), free and bound variables, sentences.
Chapter 3: Semantics of First-Order Languages--Again, standard material: Given a symbol set (signature) S, they define S-structure (domain + interpretations of relations, functions & constants in S), assignment (of variables to the domain), and S-interpretation (S-structure + assignment). Satisfaction of a formula by an S-interpretation is defined inductively in the usual way (interpreting terms as members of the domain and formulas as truth values). Then we have: models (of S-formulas), the consequence relation, validity, satisfiability, logical equivalence. The coincidence lemma shows that interpretations of formulas [terms] depend only on the interpretation of the symbols occurring in the formula [term]. This leads to reducts and expansions of S-structures. They define isomorphisms of S-structures and prove that the same sentences are true in isomorphic S-structures (and the more general theorem about formulas in S-interpretations with the assignments corresponding to the isomorphism). Example formalizations are given: equivalence relations, continuity, finite & infinite cardinality, orderings, fields.
Partial functions cannot be directly represented, but can be represented as total functions defined arbitrarily where the partial function was undefined or as the graph relation of the partial function. (Note: In Q_0, these two representations become, in some sense, equivalent, since we have the description operator which can turn such a graph into a total function--the arbitrary definition is completely determined by the interpretation of the description operator.) Also, first-order logic can be many-sorted, but we can perform "sort reduction" by adding new predicate symbols. Torsion groups cannot be captured by first-order sentences (see compactness later). Also, the theory of the naturals can only be captured up to isomorphism by using a second-order formula. The fact that these determine the naturals up to isomorphism is called "Dedekind's Theorem" (p. 47). Note that when discussing semantics of second-order formulas (which is not formulated explicitly), they assume quantifiers over (for example) subsets of a domain cover all sets. This corresponds to "standard" models (as opposed to "general" models) in the Henkin style semantics of higher order logic used by Andrews.
Substitution of terms for variables is inductively defined--avoiding variable capture by changing the names of bound variables automatically. The semantic theorem ("Substitution Lemma") that substitution can be done before or after interpretation is proven.
Chapter 4: A Sequent Calculus--At last we reach formal provability. The definition of provability is given in terms of sequents (antecedent formulas and a single succedent formula) and rules of inference on sequents. The given rules are Antecedent [Thinning], Assumption [Hypothesis], Proof by Cases, Contradiction, Or-Antecedent, Or-Succedent, Exists-Intro-Succedent, Exists-Intro-Antecedent, Reflexivity, and Substitution. Several other rules are derived. The "correctness" [soundness] of each rule is shown as it is introduced, leading to the "Correctness Theorem" [Soundness Theorem]. Then, consistency is defined and the basic theorems about consistency are shown (Con H iff every finite subset of H is consistent; satisfiable sets are consistent; consistent sets can be consistently extended by a formula or its negation). This sets the stage to prove compactness once we have completeness.
Chapter 5: The Completeness Theorem. A Henkin-style proof of Godel's Completeness Theorem is presented. That is, it is shown that a consistent set of formulas can be extended to a maximally consistent set with witnesses--and the latter can be used to construct a syntactic model (modulo provable equality of terms). They split the proof into the countable and the general case. The general case requires Zorn's Lemma, while the countable case does not appear to use the Axiom of Choice (since we can well-order a countable set of formulas).
Chapter 6: The Lowenheim-Skolem Theorem and the Compactness Theorem. The proof of the completeness theorem implies the downward Lowenheim-Skolem Theorem (by looking at the cardinality of the constructed term model). The Compactness Theorem follows from the equivalence of consistency and satisfaction. Compactness implies the upward Lowenheim-Skolem Theorem. Together, we have what the authors call the Lowenheim-Skolem-Tarski Theorem that any set of formulas with an infinite model has a model of every infinite cardinality (at least the size of the language). These tools allow the exploration of elementary and delta-elementary classes (of structures) and the distinction between elementary equivalence and isomorphism. They call the theorem asserting the existence of a countable nonstandard model of arithmetic Skolem's Theorem.
Chapter 7: The Scope of First-Order Logic. The apparent circularity of founding mathematics on formal logic (which the book has studied mathematically) is addressed by describing the formal notion of proof as a "game." Also, a brief introduction to the intuitionistic alternative is given. Then the authors describe how set theory can be axiomatized within first-order logic (first a simple version with urelements, then later full ZFC without regularity [foundation]), giving a basis for mathematics. Within set theory, we can express statements such as "Any two Peano structures are isomorphic." Then, within any model of the set theory, there will be an [object-level] "isomorphism" between any two [object-level] "Peano structures." Still, we may have two different models of set theory, and we may consider a "Peano structure" in each of the models. We can lift the elements out of such a structure into a [meta-level] set by considering the objects a in the model such that a is [object-level] in the structure. These sets may not be isomorphic. In fact, they construct an example in which such a set may be uncountable. Incidentally, they talk about "object set theory" and "background set theory" instead of the object-level and meta-level. Skolem's paradox is also discussed. They end by discussing how first-order logic can be described within axiomatic set theory.
Chapter 8: Appendix. This chapter addresses conservative extensions by definitions, relativization and substructures (i.e., including a predicate interpreted as the domain of a substructure and relativizing quantifiers by the predicate), and normal forms (disjunctive normal form and prenex normal form).
Part B.
Chapter 9: Extensions of First-Order Logic. Three new logics are introduced (second-order; L-omega1,omega; & LQ). The semantics are first-order structures with the obvious interpretations given to the new formulas. In second-order logic, this corresponds to standard models (since we interpret second-order variables as ranging over *all* relations). Of course, this implies completeness, compactness, and Lowenheim-Skolem all fail for second-order logic. L-omega1,omega allows countable disjunction (hence, conjunction). Here, compactness fails, but we do have downward Lowenheim-Skolem. LQ introduces a quantifier Q which is interpreted to mean "there are uncountably many." Here we do not have Lowenheim-Skolem (though we apparently can prove that each satisfiable LQ sentence has an at most aleph_1 model), but we do have a restricted version of compactness (namely, countable sets are satisfiable iff all finite subsets are).
Chapter 10: Limitations of the Formal Method. They describe procedures, decidability, enumerability, and computability. Computability is formalized in terms of Register Machines. A set is decidable iff it and its complement are enumerable. This can be used to show sets (such as the set of satisfiable formulas) are not enumerable by showing their complement is enumerable and not decidable. The Halting Problem is shown to be undecidable by a diagonal argument. Then the Halting Problem is reduced to the problem of deciding validity of first-order sentences (over a language with infinitely many relation, function, and constant symbols [of each arity]). The undecidability of such a first-order language follows.
With respect to second-order logic (assuming an infinite language as above), the notions of fin-satisfiability and fin-validity of sentences are defined (in which we only look at finite structures). Fin-satisfiability is enumerable (we can check all models of size n, and keep increasing n). Fin-satisfiability is not decidable (since the halting problem can be reduced to it). Thus, fin-validity is not enumerable (using negation of sentences to get the correspondence between fin-validity and not-fin-satisfiability). This is called "Trahtenbrot's Theorem." The incompleteness of second-order logic (with respect to standard models) follows, since a second-order sentence phi is fin-valid iff [phi_fin -> phi] is valid. (Recall, we can capture finiteness with second-order logic using a pigeonhole principle.) (The assumption of an infinite language can be weakened.)
Theories (as consistent sets of sentences closed under consequence) may be R-enumerable, R-axiomatizable and finitely axiomatizable. A theory is complete if every sentence or its negation is in the theory. An R-enumerable (hence R-axiomatizable) complete theory is R-decidable. We can code programs into arithmetic and use this to show undecidability of arithmetic (by reducing the halting problem to it). It follows that arithmetic (complete number theory) is undecidable and, in fact, is not even R-enumerable. The coding does not use full arithmetic and can be done in weaker theories (such as Peano Arithmetic). We need to be able to represent computable functions in the theory. This allows us to prove a fixed-point theorem. If a theory (i.e., the Godel numbers of the sentences provable in the theory) is representable in the theory, then the theory is incomplete. This is proven by the standard diagonal argument using the fixed-point theorem. Tarski's Theorem that "Arithmetic truth is not representable in arithmetic" follows (since complete number theory is complete and representability in arithmetic is equivalent to definability in arithmetic). Godel's First Incompleteness Theorem also follows by contradiction (R-enumerability and completeness imply decidability imply representability, contradiction). This does not appear to use omega-consistency! I should take a closer look.
The authors also construct the usual Godel Sentence which cannot be proven from the axioms unless the axioms are inconsistent. They note that this argument can be coded to show Godel's Second Incompleteness Theorem, that consistency cannot be proven within a theory which includes Peano Arithmetic. In particular, Peano Arithmetic cannot be proven consistent within Peano Arithmetic. Also, ZFC cannot be proven consistent within ZFC.
Chapter 11: An Algebraic Characterization of Elementary Equivalence. Partial isomorphisms between S-structures are introduced, leading to the notion of two models being finitely isomorphic or partially isomorphic (weakenings of full isomorphism). A partial isomorphism allows us to do the back-and-forth argument to show countable partially isomorphic models are isomorphic (the canonical example being linear dense orderings--Cantor's Proof). Even more easily we can show finitely isomorphic finite models are isomorphic. We furthermore obtain Fraisse's Theorem, that given a finite symbol set S, two S-structures are elementarily equivalent iff they are finitely isomorphic. Example: Any two linear dense orderings are partially isomorphic, hence finitely isomorphic, hence elementarily equivalent (hence the theory is complete). Since completeness and R-axiomatizability imply R-decidability, we can use Fraisse's Theorem to determine R-decidability as well.
Fraisse's Theorem is proven by restricting ourselves at the "nth level" of the finite isomorphism to preserving formulas with no more than n nested quantifiers (the "quantifier rank"). Since the symbol set S is assumed to be finite, up to logical equivalence there are only finitely many such formulas. The proof leads to the notion of m-isomorphism. Two structures are m-isomorphic iff they satisfy the same sentences of quantifier rank no more than m.
This back-and-forth notion of finite isomorphism can be described as a game ("Ehrenfeucht Games"). See also the discussion of Fraisse's Theorem in Leivant.
Chapter 12: Characterizing First-Order Logic. An abstract notion of a logical system is defined. First-order logic, as well as the extensions considered in Chapter 9, are examples of such a system. The expressive power of a logical system is measured by considering the classes of (first-order) structures single formulas of the system can determine. They work with "regular" logical systems which are closed under Boolean connectives, permit relativization, and allow elimination of function and constant symbols. Lindstrom's First Theorem says that any regular logical system stronger than first-order logic which satisfies Lowenheim-Skolem and Compactness is equivalent to first-order logic. Lindstrom's Second Theorem says that any effective regular logical system effectively stronger than first-order logic which satisfies Lowenheim-Skolem and is enumerable for validity is actually effectively equivalent to first-order logic.
So, first-order logic is the best! Well, it is the best at describing first-order structures. (See also the discussion of ontology and logic in Leivant and his application of Lindstrom's Theorem to ramified type theory.)