forall x: Calgary. An Introduction to Formal Logic

Citation

Magnus, P. D., Button, T., Trueman, R., & Zach, R. (2025). forall x: Calgary. An Introduction to Formal Logic (Fall 2025 ed.), with contributions by J. R. Loftis and A. Thomas-Bolduc. Open Logic Project. Free official edition: https://forallx.openlogicproject.org/

Chapter Summary

The book has 48 short chapters in nine parts; this summary follows the parts and keeps the chapter titles.

Chapters 1–3 (Part I, Key notions of logic): Arguments; The scope of logic; Other logical notions

Before any symbols appear, Part I explains what an argument is (premises and a conclusion, built from sentences that can be true or false) and defines validity: no case in which the premises are true and the conclusion false. Chapter 2 distinguishes kinds of validity, introduces formal validity and soundness, and contrasts deductive validity with inductive strength. Chapter 3 adds joint possibility, necessary truth and falsehood, and necessary equivalence, all defined in terms of cases.

Chapters 4–8 (Part II, Truth-functional logic): First steps to symbolization; Connectives; Sentences of TFL; Ambiguity; Use and mention

Part II introduces the language of truth-functional logic (TFL). It motivates symbolisation by showing that some arguments are valid in virtue of form, introduces sentence letters and symbolisation keys, and presents the five connectives (negation, conjunction, disjunction, conditional, biconditional) with careful advice on English expressions such as "unless". Chapter 6 gives a recursive definition of a sentence of TFL and bracketing conventions, Chapter 7 shows how symbolisation resolves lexical and structural ambiguity, and Chapter 8 explains quotation, object language versus metalanguage, and metavariables.

Chapters 9–15 (Part III, Truth tables): Characteristic truth tables; Truth-functional connectives; Complete truth tables; Semantic concepts; Limitations of TFL; Truth table shortcuts; Partial truth tables

This part gives TFL its semantics. After the characteristic truth tables and a discussion of truth-functionality (including why the material conditional only approximates English "if"), it shows how to build complete truth tables and uses them to define tautologies, contradictions, equivalence, satisfiability and entailment, written with the double turnstile. Chapter 13 shows with examples what TFL cannot capture, and the last two chapters teach shortcuts and partial truth tables for faster testing.

Chapters 16–22 (Part IV, Natural deduction for TFL): The very idea of natural deduction; Basic rules for TFL; Constructing proofs; Additional rules for TFL; Proof-theoretic concepts; Derived rules; Soundness and completeness

Part IV develops a Fitch-style natural deduction system with introduction and elimination rules for each connective, including subproofs and indirect proof. Chapter 18 offers strategies for finding proofs (working backward from the goal, working forward from premises, proceeding indirectly). Disjunctive syllogism, modus tollens, double-negation elimination, excluded middle and De Morgan rules are added and then shown to be derivable from the basic rules. Chapter 20 introduces the single turnstile and proof-theoretic notions such as theorems and interderivability, and Chapter 22 explains, without full proof, why the proof system and truth tables agree.

Chapters 23–29 (Part V, First-order logic): Building blocks of FOL; Sentences with one quantifier; Multiple generality; Identity; Sentences of FOL; Definite descriptions; Ambiguity

Here the language is extended with names, predicates, quantifiers and domains. The chapters build symbolisation skill step by step: common quantifier phrases, empty predicates and the choice of domain, many-place predicates and the order of quantifiers, and identity (for "only", "except" and counting). Chapter 27 defines terms, formulas, free variables and sentences formally; Chapter 28 presents Russell's theory of definite descriptions and discusses its adequacy; and Chapter 29 uses symbolisation to resolve scope ambiguities in English.

Chapters 30–35 (Part VI, Interpretations): Extensionality; Truth in FOL; Semantic concepts; Using interpretations; Reasoning about interpretations; Properties of relations

Part VI gives first-order logic its semantics. Predicates are interpreted by their extensions, interpretations are specified for domains, names and predicates, and truth in FOL is defined for atomic sentences, connectives and quantifiers. Validity, entailment and satisfiability are then redefined for FOL, and the chapters show how to construct interpretations to demonstrate that a sentence is not a validity or that an argument is invalid, and why showing validity instead requires general reasoning about all interpretations. The final chapter defines transitivity, reflexivity, symmetry and related properties.

Chapters 36–41 (Part VII, Natural deduction for FOL): Basic rules for FOL; Proofs with quantifiers; Conversion of quantifiers; Rules for identity; Derived rules; Proofs and semantics

The proof system is extended with introduction and elimination rules for the universal and existential quantifiers (with attention to empty domains and vacuous quantification), followed by strategies for quantifier proofs, rules for converting quantifiers across negation, and rules for identity. The conversion rules are then shown to be derivable. Chapter 41 stresses that provability (⊢) and semantic consequence (⊨) are different notions and explains when each is easier to establish.

Chapters 42–44 (Part VIII, Modal logic): Introducing modal logic; Natural deduction for ML; Semantics for ML

This part extends TFL with the operators □ and ◇. It explains different readings of necessity (including provability), sets out natural deduction systems K, T, S4 and S5, and gives possible-world semantics with accessibility relations for each system.

Chapters 45–48 (Part IX, Metatheory): Normal forms; Functional completeness; Proving equivalences; Soundness

The final part proves results about TFL itself: every sentence has disjunctive and conjunctive normal forms, certain sets of connectives are functionally complete (and others fail to be), equivalences can be established by substitution and chains of equivalences, and the natural deduction system for TFL is sound. Appendices cover alternative notations, alternative proof systems and a quick reference of rules, followed by a glossary.

Key Concepts

Part I: Key notions of logic

• Validity: an argument is valid when there is no case in which all premises are true and the conclusion false.
• Soundness of an argument: being valid with all premises actually true.
• Joint possibility: sentences that could all be true together in some case.

Part II: Truth-functional logic

• Symbolisation key: the assignment of English sentences to sentence letters.
• Main logical operator: the connective that determines a sentence's overall structure.
• Object language and metalanguage: the language under study versus the language used to talk about it, kept apart by quotation and metavariables.

Part III: Truth tables

• Valuation: an assignment of truth values to sentence letters, one per line of a truth table.
• Tautology, contradiction, entailment: true on every valuation; false on every valuation; no valuation makes the premises true and the conclusion false.
• Truth-functionality: a connective's output depends only on the truth values of its inputs.

Part IV: Natural deduction for TFL

• Introduction and elimination rules: paired rules for proving and using sentences with each connective.
• Subproof and indirect proof: temporary assumptions that are discharged, including proof by deriving a contradiction.
• Derived rule: a rule that adds convenience but can be justified from the basic rules.

Part V: First-order logic

• Quantifiers and domain: ∀ and ∃ range over a chosen domain of objects.
• Order of quantifiers: ∀x∃y and ∃y∀x say different things.
• Russell's analysis of definite descriptions: "the F is G" as "there is exactly one F, and it is G".

Part VI: Interpretations

• Extension: the set of objects (or tuples) a predicate applies to.
• Interpretation: a domain together with referents for names and extensions for predicates.
• Counter-interpretation: an interpretation that shows a sentence is not a validity or an argument is invalid.

Part VII: Natural deduction for FOL

• Universal introduction and existential elimination: quantifier rules with restrictions on the names used.
• Single versus double turnstile: provability versus semantic consequence.

Part VIII: Modal logic

• Necessity and possibility operators: □ and ◇ added to TFL.
• Systems K, T, S4, S5: proof systems of increasing strength, matched to accessibility relations in possible-world semantics.

Part IX: Metatheory

• Normal forms: disjunctive and conjunctive normal forms into which every TFL sentence can be converted.
• Functional completeness: the ability of a set of connectives to express every truth function.
• Soundness of the proof system: whatever can be proved is entailed.

Critical Analysis

Strengths

• Careful separation of semantics and proof. The book defines logical notions first informally (Part I), then by truth tables and interpretations, and then proof-theoretically, and it insists on the difference between ⊨ and ⊢ (Chapters 20, 22 and 41). This structure prepares students for metatheory rather than treating logic as a bag of techniques.
• Strong teaching of symbolisation. Chapters on "unless", ambiguity, empty predicates, the order of quantifiers, identity and definite descriptions give detailed guidance on the hardest skill for beginners, translating English into formal notation, with plenty of worked examples.
• Proof strategy, not only rules. Chapter 18 and Chapter 37 teach how to search for proofs (working backward and forward, indirect proof), and the system uses Gentzen-style rules in which indirect proof is the only classical rule, so the step from basic to derived rules is transparent.
• Open and well supported. The text is CC BY licensed, has an accessible HTML version, freely available solutions to many exercises, and its syntax and proof systems (except modal logic) are supported by the Carnap online software for automated marking.

Limitations

• No completeness proof. Chapter 22 discusses soundness and completeness informally, and Part IX proves only the soundness of natural deduction for TFL; completeness for TFL or FOL is left to more advanced texts.
• Modal logic is a brief add-on. Part VIII covers K, T, S4 and S5 in three chapters without first-order modal logic or philosophical applications in depth, which suits a taste rather than a course on modal logic.
• Frequently changing versions. The preface notes that the online PDF "changes frequently" and advises instructors to fix a version; chapter and page numbers can differ between the version read here and printed copies.
• Formal rather than informal logic. Apart from Part I's treatment of inductive arguments, the book does not cover fallacies, argument diagramming or critical reasoning, so courses that combine informal and formal logic will need other material.

Where It Fits in the Course

In the Logic list, forall x: Calgary is a first-course formal logic text, alongside Barker-Plummer, Barwise and Etchemendy's Language, Proof and Logic, which is generally described as covering similar ground (propositional and first-order logic with a Fitch-style proof system) and as being built around its own companion software. Copi, Cohen and Rodych's Introduction to Logic is generally described as covering informal reasoning and traditional logic more extensively; students who want fallacies and critical reasoning can use it alongside forall x, whose formal coverage is more systematic.

Two later texts follow naturally. Sider's Logic for Philosophy moves on to metalogic, modal and non-classical logics for philosophers and assumes the material of Parts II–VII; forall x's Part VIII and Part IX are a useful bridge. Boolos, Burgess and Jeffrey's Computability and Logic treats computability and the major metatheorems (including completeness and incompleteness) that forall x does not prove, and is best taken after a first course based on this book.

How to Use This Book

The book is written for a semester-long introduction to formal logic, typically in a philosophy department, and assumes no mathematics beyond ordinary care with definitions. The preface reports a 12-week plan covering Parts I–VII plus Chapters 45–47, leaving out partial truth tables and derived rules. A one-semester course can follow that plan; Part VIII (modal logic) and Chapter 48 (soundness) suit a longer course or an honours stream.

Do the practice exercises at the end of most chapters, and check answers with the separate solutions booklet published on the book's site. If your course uses Carnap (carnap.io), symbolisation, truth tables and proofs can be practised with automatic feedback. Because the online PDF is updated, download one version and keep using it for the whole term, as the preface recommends; the quick-reference appendix and glossary are useful during proofs and exams.

Edition and Sources

This guide is based on the Fall 2025 edition of forall x: Calgary (PDF revision c5cb415, dated 2026-09-27), downloaded from the official site https://forallx.openlogicproject.org/. The site's current PDF is this Fall 2025 version; earlier Fall 2020 and Fall 2021 PDFs are archived there, but no Fall 2023 file is offered, so the guide may differ in details from the Fall 2023 printing listed on this page. The guide draws on the preface (scope, credits, notes for instructors), the full table of contents, and the opening of every one of the 48 chapters with all section headings and the presence of practice exercises, with Chapters 13, 22, 35, 41 and 42 read more fully.