Language, Proof and Logic

Citation

Barker-Plummer, D., Barwise, J., & Etchemendy, J. (2011). Language, Proof and Logic (2nd ed.). CSLI Publications.

Chapter Summary

Language, Proof and Logic (LPL) is a textbook packaged with software. Tarski's World teaches the first-order language and its semantics, Fitch is a natural deduction environment for building and checking proofs, Boole handles truth tables, and Submit sends exercise files to the Grade Grinder, an online service that grades them automatically. An introduction is followed by 19 chapters in three parts. Many sections are explicitly marked "(optional)". Back matter includes a summary of formal proof rules, a glossary, and file, exercise and general indexes. The publisher describes the second edition as a major expansion and revision, with more on mathematical induction (and software support for Peano and course-of-values induction) and improved coverage of naive and Zermelo–Fraenkel set theory.

Introduction

Sections on the special role of logic in rational inquiry, why one should learn an artificial language, and consequence and proof. They are followed by instructions about the homework exercises, which the contents page marks as essential, and a note to the instructor.

Part I: Propositional Logic

Chapters 1–2: Atomic Sentences; The Logic of Atomic Sentences

Chapter 1 introduces individual constants, predicate symbols and atomic sentences, with optional sections on function symbols, the first-order languages of set theory and arithmetic, and alternative notation. Chapter 2 defines valid and sound arguments, introduces methods of proof and formal proofs, shows how to build proofs in Fitch, and explains how to demonstrate nonconsequence.

Chapters 3–4: The Boolean Connectives; The Logic of Boolean Connectives

Chapter 3 covers negation, conjunction and disjunction, a game for evaluating sentences, ambiguity and parentheses, equivalent ways of saying things, and translation. Chapter 4 separates tautologies from logical truths, and tautological from logical equivalence and consequence. It applies tautological consequence in Fitch, with optional sections on moving negations inward and on conjunctive and disjunctive normal forms.

Chapters 5–6: Methods of Proof for Boolean Logic; Formal Proofs and Boolean Logic

Informal proof comes first: valid inference steps, proof by cases and proof by contradiction. Chapter 6 then gives the formal introduction and elimination rules for conjunction, disjunction and negation, the proper use of subproofs, and strategy and tactics for finding proofs.

Chapters 7–8: Conditionals; The Logic of Conditionals

The material conditional and biconditional, conversational implicature and, optionally, truth-functional completeness. Chapter 8 adds informal and formal proof methods for the conditionals, an optional section on soundness and completeness, and review exercises for Part I.

Part II: Quantifiers

Chapters 9–11: Introduction to Quantification; The Logic of Quantifiers; Multiple Quantifiers

Chapter 9 introduces variables, the quantifier symbols, wffs and sentences, the semantics of the quantifiers and the four Aristotelian forms, and practises translating complex noun phrases. Chapter 10 treats first-order validity and consequence, quantifier equivalences including DeMorgan's laws, an optional section on the axiomatic method, and lemmas. Chapter 11 handles mixed quantifiers, a step-by-step method of translation, paraphrasing English, ambiguity and context sensitivity, and prenex form.

Chapters 12–13: Methods of Proof for Quantifiers; Formal Proofs and Quantifiers

Informal methods come first: valid quantifier steps, existential instantiation, general conditional proof and proofs with mixed quantifiers. The formal universal and existential rules in Fitch follow, with strategy and tactics and optional sections on soundness and completeness.

Chapter 14: More about Quantification

Numerical quantification and proving numerical claims, "the", "both" and "neither", adding other determiners to first-order logic, the logic of generalized quantification, and the expressive limits of first-order logic.

Part III: Applications and Metatheory

Chapters 15–16: First-order Set Theory; Mathematical Induction

Chapter 15 develops naive set theory: the empty set, subsets, intersection and union, ordered pairs, relations and functions. Optional sections cover the powerset, Russell's Paradox and Zermelo–Fraenkel set theory. Chapter 16 presents inductive definitions and proofs, induction on the natural numbers and induction in Fitch, with optional sections on axiomatizing the natural numbers and on strong induction.

Chapters 17–19: Advanced Topics in Propositional Logic; Advanced Topics in FOL; Completeness and Incompleteness

Chapter 17 proves completeness for propositional logic, with optional sections on Horn sentences and resolution. Chapter 18 defines first-order structures, revisits truth and satisfaction and proves soundness for first-order logic, with optional sections on Skolemization, unification and resolution. Chapter 19 proves the Completeness Theorem by the Henkin construction, then covers the Löwenheim–Skolem and Compactness Theorems and closes with the Gödel Incompleteness Theorem.

Key Concepts

Part I: Propositional Logic

• Validity and soundness: an argument is valid when its conclusion follows from its premises, and sound when it is also valid and its premises are true.
• Tautological versus logical consequence: consequence in virtue of the truth-functional connectives alone, versus consequence in virtue of meaning more generally.
• Fitch-style natural deduction: formal proofs built from introduction and elimination rules, with subproofs for temporary assumptions.
• Truth-functional completeness: whether a set of connectives can express every truth function.

Part II: Quantifiers

• First-order validity and consequence: what follows from the meaning of the quantifiers and identity alone, beyond tautological consequence.
• Translation: rendering English sentences, including complex noun phrases and mixed quantifiers, into first-order logic step by step.
• Existential instantiation and general conditional proof: the informal patterns that the formal quantifier rules mirror.
• Generalized quantifiers: determiners such as "most" or "both" and the limits of what first-order logic can express.

Part III: Applications and Metatheory

• Mathematical induction: proof over inductively defined sets, including the natural numbers.
• Soundness and completeness: the proof system proves only, and all, the valid consequences.
• Compactness and Löwenheim–Skolem: consequences of completeness about infinite sets of sentences and the sizes of models.
• Gödel's incompleteness theorem: the limit on proving all truths of arithmetic in a consistent formal system.

Critical Analysis

Strengths

• Software built into the learning. According to the publisher, the package's programs let students build worlds, truth tables and proofs, and the Grade Grinder grades hundreds of computer exercises almost instantly. Students get quick feedback, and instructors are spared routine checking.
• Informal before formal. The contents pair each logical topic with a chapter on informal methods of proof before a chapter on formal proofs (Chapters 5–6 and 12–13). Students learn to reason in ordinary mathematical prose as well as in a formal system.
• Clearly marked optional material. Optional sections are labelled in the contents, so a course can take the core path through Parts I and II and choose extras.
• Range from beginner to metatheory. The publisher says no prior logic is assumed and that the book suits introductory and second courses. The Openproof site places it anywhere from first undergraduate courses to a first graduate course, since Part III reaches completeness, compactness and Gödel's theorem.
• Translation and natural language. Whole sections on translation, paraphrasing English, conversational implicature and generalized quantifiers reflect the authors' interest in language, not only in proof.

Limitations

• Tied to the software package. The full benefit depends on the Registration ID sold with the package. The publisher notes that it is not transferable once activated, so second-hand copies may not give access to the web apps and grading.
• Long and dense. The book runs to roughly 600 pages, and Part III moves well beyond what a first course needs.
• First-order only. The contents include no modal, many-valued or other non-classical logic; Chapter 14 discusses the expressive limits of first-order logic, but students in philosophy will need another text for modal logic.

Where It Fits in the Course

Within the logic course, LPL is one of two introductions to formal logic using Fitch-style natural deduction. forall x: Calgary is a free, openly licensed text covering truth-functional and first-order logic with a similar proof system. It is shorter and needs no software, and it suits students who want a lighter first pass. Copi's Introduction to Logic covers informal reasoning, syllogistic logic, symbolic logic and induction in one volume, so it fits a critical-reasoning course better than LPL does.

After LPL, Theodore Sider's Logic for Philosophy is a second course that treats propositional and predicate logic more rigorously and adds the modal logic that LPL leaves out. Computability and Logic by Boolos, Burgess and Jeffrey develops computability and full proofs of the limitative results; LPL's Chapter 19, which ends with a sketch of Gödel's theorem according to the publisher, is a useful bridge to it.

How to Use This Book

The book assumes no prior logic. Read the introduction's instructions on homework before starting exercises, because the software and the Grade Grinder are part of how the exercises are meant to be done and submitted. A first course typically covers Parts I and II (Chapters 1–14). The authors' online course built on the package covers exactly these first two parts in 14 chapters, and recommends roughly one chapter a week. Skip the optional sections on a first pass, except where your instructor assigns them.

Work through each informal-methods chapter before its formal counterpart, and use Tarski's World to check translations against concrete worlds before moving to proofs in Fitch. Part III suits a second course or students heading into mathematics or computer science. Chapters 15–16 on set theory and induction are good preparation for any proof-based mathematics, and Chapters 17–19 lead to the metatheory. Use the summary of formal proof rules and the glossary at the back as reference while doing exercises.