List of results

Theorems and lemmas 97 Definitions 71 Examples 163 Exercises 459

Connectives and Derivations

1.1 Statements, Arguments and How to Break One

Definition 1.1.1 Statement
Example Statements and nonstatements
Definition 1.1.2 Main Connective
Definition 1.1.3 Counterexample Set
Exercise A1
Exercise A2: Drill
Exercise B1: Translating analysis
Exercise B2: Parsing
Exercise B3: Necessary and sufficient, used later
Exercise B4: Break it or explain why not
Exercise B5: One key, sixteen sentences, used later
Exercise B6: Same form?
Exercise C1: “Only if” and “unless”, used later

1.2 Derivations, Starting with And

Definition 1.2.1 Rule Schema
Definition 1.2.2 Box-Free Derivation
Example Chaining
Example Not a derivation
Definition 1.2.3 Derivable
Definition 1.2.4 Sequent
Example Derivations, simplest first
Definition 1.2.5 Rules for Conjunction
Example Two warm-ups
Proposition 1.2.1 Conjunction Commutes
Proposition 1.2.2 Conjunction Is Associative
Example A product of numbers in the unit interval
Example Instances of $\mathrm{\wedge I}$ and $\mathrm{\wedge E}$
Exercise A1
Exercise A2: Drill
Exercise B1: The other grouping
Exercise B2: Annotating a proof
Exercise B3: Two layers, then rebuild
Exercise C1: A bad rule
Exercise C2: Find the error
Exercise C3: A shortcut through two layers
Exercise C4: Challenge: What conjunction cannot do

1.3 Using an Implication: Modus Ponens

Example Four cards
Definition 1.3.1 Implication Elimination
Example Chains of implications
Example Two chains about numbers
Example Instances of $\mathrm{{\to}E}$
Exercise A1
Exercise A2: Drill
Exercise B1: Two chains
Exercise B2: Two facts and a number
Exercise B3: Which premises are needed?
Exercise B4: Assemble the hypothesis
Exercise B5: Supply the missing premise
Exercise C1: Find the error
Exercise C2: Both ends

1.4 Proving an Implication: the Rule of the Box

Definition 1.4.1 Rules for Implication
Proposition 1.4.1 Implication Is Transitive
Example Two errors that cancel
Definition 1.4.2 Derivation
Example A line cited from a closed box
Example First boxes
Proposition 1.4.2 Two Hypotheses or One at a Time
Example Instances of $\mathrm{{\to}I}$
Exercise A1
Exercise A2: Drill
Exercise B1: Two boxes, one inside the other
Exercise B2: An assumption that is not used
Exercise B3: Unwinding an absolute value
Exercise B4: Putting a derivation in order
Exercise C1: Exit check: a line from a closed box
Exercise C2: A hypothesis inside a hypothesis
Exercise C3: Exit check: a derivation and its prose
Exercise C4: The assumptions a line depends on, used later

1.5 Or, Introduced

Definition 1.5.1 Or-Introduction
Example A side chosen too early
Example Derivations with or-introduction
Example A disjunctive hypothesis splits into two implications
Example A product with a zero factor
Example Instances of $\mathrm{\vee I}$
Exercise A1
Exercise A2: Drill
Exercise B1: Committing to a side
Exercise B2: The last line
Exercise B3: A theorem with a weaker hypothesis
Exercise B4: Derive or break
Exercise C1: Which new rules are safe?
Exercise C2: Predicting the manufacture

1.6 Using Or: Proof by Cases

Definition 1.6.1 Rules for Disjunction
Example First derivations with “or”
Example Cases on a hypothesis are two implications
Example Constructive dilemma
Proposition 1.6.1 Distributivity
Example Regrouping a disjunction
Example A number is at most its absolute value
Example The absolute value of a product
Example The triangle inequality by cases
Example Instances of $\mathrm{\vee E}$
Exercise A1
Exercise A2: Drill
Exercise B1: The other distributive law
Exercise B2: The larger of two numbers
Exercise B3: Two cases, two conclusions
Exercise B4: The smaller of two numbers
Exercise B5: Derive or break
Exercise B6: Translate, then derive
Exercise B7: Fifteen standard sequents
Exercise C1: Challenge: The reverse triangle inequality
Exercise C2: Find the error
Exercise C3: Exit check: a distributive law, rule by rule
Exercise C4: The second half
Exercise R1
Exercise R2
Exercise R3

Negation and Classical Logic

2.1 Contradiction: Using a Negation

Definition 2.1.1 Rules for Contradiction
Example The first clashes
Proposition 2.1.1 Contradictory Premises Prove Anything
Proposition 2.1.2 Vacuous Implication
Example Manufacturing the other half of a clash
Example An impossible case
Theorem 2.1.3 Even Square, Even Number
Example An implication with an impossible hypothesis
Example Instances of $\mathrm{\neg E}$ and $\mathrm{\bot E}$
Exercise A1
Exercise A2: Drill
Exercise B1: Two clashes
Exercise B2: An even successor
Exercise B3: Two vacuous promises
Exercise B4: An impossible case, scaffolded
Exercise B5: Derive or break
Exercise B6: Name the rule you reject
Exercise C1: A disjunct that cannot hold
Exercise C2: A clash that escaped its box

2.2 Proving a Negation

Definition 2.2.1 Rules for Negation
Example A negative statement proved by not-introduction
Example Two negations from one premise
Example Three negations become one
Theorem 2.2.1 Irrationality of the Square Root of Two
Example Instances of $\mathrm{\neg I}$
Exercise A1
Exercise A2: Drill
Exercise B1: A box inside a box
Exercise B2: A quadratic with no zero
Exercise B3: The square root of three, used later
Exercise B4: A premise that turns on itself
Exercise B5: From $\sqrt 2$ to $\sqrt p$
Exercise B6: Derive or break
Exercise C1: The square root of six
Exercise C2: A proof that proves too much

2.3 Derived Rules: Proved Sequents as New Rules

Proposition 2.3.1 Modus Tollens
Proposition 2.3.2 Contrapositive
Definition 2.3.1 Derived Rule
Lemma 2.3.3 Weakening and Cut
Proposition 2.3.4 Disjunctive Syllogism
Example Derived rules in use
Example Modus tollens on numbers
Example Even square, even number, by contraposition
Example Instances of $\mathrm{MT}$ , $\mathrm{CP}$ and $\mathrm{DS}$
Exercise A1
Exercise A2: Drill
Exercise B1: The other disjunctive syllogism, used later
Exercise B2: Putting a derivation in order
Exercise B3: Two refutations
Exercise B4: Dilemmas as derived rules, used later
Exercise B5: Derive or break
Exercise C1: Two premises that cannot both fail, used later
Exercise C2: A circular derivation
Exercise C3: Exit check: labeling a proof

2.4 Iff, Equivalence, and What a Definition Says

Definition 2.4.1 Rules for the Biconditional
Example An iff read both ways
Proposition 2.4.1 An Iff Is Two Implications
Example Negating both sides of an iff
Lemma 2.4.2 No Statement Is Equivalent to Its Negation
Definition 2.4.2 Provable Equivalence
Proposition 2.4.3 Provable Equivalence and the Biconditional
Theorem 2.4.4 Odd Square, Odd Number
Theorem 2.4.5 Squaring Preserves Order
Example A definition used in both directions
Proposition 2.4.6 Proving Equivalence by a Cycle
Example Three descriptions of the unit interval
Example Instances of $\mathrm{{\leftrightarrow}I}$ and $\mathrm{{\leftrightarrow}E}$
Exercise A1
Exercise A2: Drill
Exercise B1: Iff is transitive
Exercise B2: A parity equivalence
Exercise B3: Strict inequalities
Exercise B4: Both directions
Exercise B5: Criticize the definition
Exercise B6: Four conditions, one cycle
Exercise B7: Derive or break
Exercise C1: Divisibility by six
Exercise C2: Dropping a hypothesis, and repairing the statement

2.5 Proof by Contradiction and the Classical Rules

Example A number whose square is at most itself
Definition 2.5.1 Reductio ad Absurdum
Proposition 2.5.1 Double Negation
Proposition 2.5.2 Converse of the Contrapositive
Proposition 2.5.3 Excluded Middle
Proposition 2.5.4 Peirce’s Law
Proposition 2.5.5 De Morgan’s Laws
Proposition 2.5.6 Implication as a Disjunction
Theorem 2.5.7 The Classical Rules Are Interderivable
Example A number below every positive number
Example Instances of $\mathrm{RAA}$
Exercise A1
Exercise A2: Drill
Exercise B1: With and without the new rule, used later
Exercise B2: Back from negated sides, used later
Exercise B3: The redundant rule
Exercise B4: Stuck at a letter
Exercise B5: Derive or break, used later
Exercise B6: A law that sounds false
Exercise C1: Challenge: Excluded middle does the work of reductio directly
Exercise C2: Find the error, used later
Exercise C3: Exit check: a classical disjunction
Exercise C4: Challenge: Smaller rule sets
Exercise R1
Exercise R2
Exercise R3

Finding Derivations

3.1 How to Find a Derivation

Definition 3.1.1 Partial Derivation
Example Splitting the goal, then using the premise
Example Proof by cases, found by the method
Example Choosing a side too early
Example A search that reaches step 5 at once
Example Lines that need nothing new
Example Building a skeleton
Exercise A1
Exercise A2: Drill
Exercise B1: Three searches
Exercise B2: The last step
Exercise B3: Two boxes and a chain
Exercise B4: Cut the detours
Exercise C1: The second half
Exercise C2: A disjunction from nothing
Exercise C3: Exit check: search
Exercise C4: Two sequents that look alike

3.2 Four Kinds of Task

Example A statement that implies a contradiction
Example Proving a disjunction by refuting one side
Definition 3.2.1 Inconsistent and Consistent Lists
Proposition 3.2.1 An Inconsistent List Proves Everything
Example Four conditions that no integer meets
Example Three inconsistent lists, and a look-alike
Proposition 3.2.2 Derivable Exactly When the Counterexample Set Is Inconsistent
Example Two claims, one connective apart
Exercise A1
Exercise A2: Drill
Exercise B1: Three theorems
Exercise B2: Two directions
Exercise B3: Derive or break, used later
Exercise B4: Derive ⊥, or make every member true, used later
Exercise C1: Exit check: the counterexample set, used later
Exercise C2: Challenge: Splitting an inconsistency, used later

3.3 From Argument to Derivation

Example An argument about a prime, extracted
Example A proof and its derivation, side by side
Exercise A1
Exercise B1: Extract, then derive
Exercise B2: Two columns
Exercise B3: Fifteen items
Exercise B4: Put the proof in order
Exercise C1: Exit check: from a paragraph to a derivation
Exercise C2: Challenge: A statement that promises anything
Exercise R1
Exercise R2
Exercise R3
Exercise R4

Truth, Soundness and Completeness

4.1 Formulas as Objects

Definition 4.1.1 Formula
Example Formation sequences
Example Strings that are not formulas
Definition 4.1.2 Parse Tree
Example Three parse trees
Definition 4.1.3 Subformula
Example Two groupings of three implications
Exercise A1
Exercise A2: Drill
Exercise B1: Trees from Chapter 1
Exercise B2: Shorthand and back
Exercise C1: Forgetting the grouping convention

4.2 Induction on the Natural Numbers

Axiom 4.2.1 Principle of Induction
Example A sum of products of neighbors
Example An inequality by induction
Theorem 4.2.2 Strong Induction
Example Threes and fives
Example Prove more to prove less
Exercise A1
Exercise A2: Drill
Exercise B1
Exercise B2: Divisible by six
Exercise B3: Two base cases
Exercise C1: Find the error
Exercise C2: Prove more

4.3 Induction and Recursion on Formulas

Theorem 4.3.1 Structural Induction
Lemma 4.3.2 Parenthesis Count
Theorem 4.3.3 Unique Readability
Definition 4.3.1 Height
Theorem 4.3.4 Structural Recursion
Example Four recursive definitions
Exercise A1
Exercise A2: Drill
Exercise B1
Exercise B2
Exercise B3: The mirror image of a formula
Exercise C1: Initial segments are not formulas
Exercise C2: Find the error
Exercise C3: Exit check: structural induction
Exercise C4: Challenge: Inside the folded proofs
Exercise C5: Challenge: formulas without parentheses

4.4 Valuations and Truth Tables

Definition 4.4.1 Valuation
Definition 4.4.2 Truth Value of a Formula
Example Computing a value
Lemma 4.4.1 Coincidence Lemma
Definition 4.4.3 Truth Table
Example The truth table of modus ponens
Example An implication and its contrapositive
Example Working backwards from F
Definition 4.4.4 Truth Function
Exercise A1
Exercise A2: Drill
Exercise B1: Backwards from F
Exercise B2: Counting atoms, the last step blank
Exercise B3: A table for a named pattern
Exercise B4: Exactly one is true
Exercise B5: Which primes divide n?
Exercise C1: A formula built from biconditionals
Exercise C2: Find the error, used later
Exercise C3: The game and the clauses

4.5 Tautologies, Entailment and Equivalence

Definition 4.5.1 Tautology and Contradiction
Definition 4.5.2 Satisfiable
Definition 4.5.3 Semantic Entailment
Example Affirming the consequent is not valid
Example Two cases, two conclusions
Example One grouping entails the other, not conversely
Definition 4.5.4 Semantic Equivalence
Proposition 4.5.1 Standard Equivalences
Definition 4.5.5 Contradictory, Contrary and Subcontrary Formulas
Lemma 4.5.2 Replacement
Example One row, two valuations
Lemma 4.5.3 Substitution
Exercise A1
Exercise A2: Drill
Exercise B1: Valid or not
Exercise B2: A biconditional as a disjunction
Exercise B3: Entailment and implication
Exercise B4: Contradictory, contrary, subcontrary, or none
Exercise C1: Substitution with a new connective, the last half blank, used later
Exercise C2: Is equivalence preserved by substitution?
Exercise C3: The rows of implication are forced
Exercise C4: One question for all

4.6 Hunting for a Refuting Row

Definition 4.6.1 Search Tree
Example A tree that closes
Example A branch that stays open
Proposition 4.6.1 The Search Decides
Example Three claims about an integer
Exercise A1
Exercise A2: Drill
Exercise B1: Valid or refuted?
Exercise B2: Can all five be true?
Exercise B3: Name the move, then complete it
Exercise C1: Rules for a new connective
Exercise C2: Exit check: refuting-row search
Exercise C3: Challenge: the search with one more connective

4.7 Soundness

Lemma 4.7.1 Contexts in a Derivation
Theorem 4.7.2 Soundness
Example Running the claim on a case split
Corollary 4.7.3 Refuting Row
Exercise A1
Exercise A2: Drill
Exercise B1: Derivable or not
Exercise B2: Ordering the $\vee$ E case
Exercise B3: Derive or refute
Exercise B4: Test the subgoal
Exercise C1: A safe rule and an unsafe one
Exercise C2: Exit check: soundness
Exercise C3: A changed table
Exercise C4: Challenge: ⊥ read as a letter
Exercise C5: Challenge: two three-valued tables
Theorem 4.7.4 Reductio Is Not Derivable from the Other Rules

4.8 Completeness

Lemma 4.8.1 The Rules Prove the Truth Tables
Lemma 4.8.2 One Row of the Truth Table Is Derivable
Example Deriving one row
Lemma 4.8.3 Splitting on an Atom
Theorem 4.8.4 Completeness
Example The method on a tautology
Corollary 4.8.5 Derivable Means Valid
Definition 4.8.1 The Step TAUT
Example One line for twelve
Exercise A1
Exercise A2: Drill
Exercise B1: Three rows from the primitive rules
Exercise B2: The method on modus ponens
Exercise B3: Table first, then a derivation
Exercise B4: When TAUT is welcome
Exercise B5: Consistent or not
Exercise C1: The remaining cases
Exercise C2: Exit check: completeness
Exercise C3: Exit check: deciding sequents
Exercise C4: Challenge: Strike out ∨I
Exercise C5: Challenge: From a closed tree to a derivation
Exercise R1
Exercise R2
Exercise R3

4.9 Normal Forms and Adequate Connectives

Definition 4.9.1 Literal
Definition 4.9.2 Disjunctive Normal Form
Definition 4.9.3 Conjunctive Normal Form
Example Exactly one of two
Theorem 4.9.1 Disjunctive Normal Form
Theorem 4.9.2 Conjunctive Normal Form
Example Two routes to a normal form
Proposition 4.9.3 Validity of a CNF
Example Validity at a glance
Proposition 4.9.4 Laws of the Constants, Idempotence and Absorption
Example Simplifying by a chain
Definition 4.9.4 Positive and Negative Occurrences
Theorem 4.9.5 Monotonicity
Definition 4.9.5 Adequate Set of Connectives
Theorem 4.9.6 Adequate Sets
Exercise A1
Exercise A2: Drill
Exercise B1: Normal forms of three formulas
Exercise B2: Two connectives from two
Exercise B3: Odd parity
Exercise C1: One connective is enough
Exercise C2: Two sets that are not adequate
Exercise C3: Exit check: normal forms
Exercise C4: From connectives to sets
Exercise C5: Counting rows
Exercise C6: Challenge: Interpolation

4.10 Compactness and Maximal Consistent Sets

Definition 4.10.1 Derivability and Entailment from Infinitely Many Premises
Lemma 4.10.1 The Formulas Can Be Listed
Lemma 4.10.2 Lindenbaum’s Lemma
Lemma 4.10.3 Maximal Consistent Collections
Lemma 4.10.4 Truth Lemma
Theorem 4.10.5 Completeness for Infinitely Many Premises
Theorem 4.10.6 Compactness
Example Infinitely many premises, finitely many used
Exercise A1
Exercise A2: Drill
Exercise B1: Running the construction
Exercise B2: The clause for implication
Exercise C1: Coloring an infinite graph
Exercise C2: Challenge: Compactness without derivations

Predicate Logic and the Quantifier Rules

5.1 Predicates and Quantifiers

Example Reading three sentences
Definition 5.1.1 Bounded Quantifier
Example Swapping two quantifiers
Exercise A1
Exercise A2: Drill
Exercise B1: Ordered quantifiers
Exercise B2: Order matters
Exercise B3: Every and some on three numbers
Exercise C1: A least element
Exercise C2: The wrong connective

5.2 Terms, Formulas, Free Variables and Substitution

Definition 5.2.1 Term
Definition 5.2.2 First-Order Formula
Definition 5.2.3 Free and Bound Variables
Definition 5.2.4 Sentence
Example The free variables of a limit statement
Example Four substitutions
Definition 5.2.5 Substitution of a Term for a Variable
Definition 5.2.6 Free For
Exercise A1
Exercise A2: Drill
Exercise B1: Computing substitutions
Exercise B2: The set of free variables
Exercise B3: Swapping two letters
Exercise C1: Challenge: What substitution does to the free variables
Exercise C2: Renaming is not swapping

5.3 Using "For Every": Instantiation

Definition 5.3.1 Universal Elimination
Example Instantiation at work
Example Instances of $\mathrm{\forall E}$
Exercise A1
Exercise A2: Drill
Exercise B1: Two links
Exercise B2: An increasing function
Exercise B3: Squares are not negative
Exercise B4: Read the terms off the goal
Exercise B5: Derive or break
Exercise C1: A partner makes a loop
Exercise C2: Instantiating at the variable itself

5.4 Proving "For Every": Let x Be Arbitrary

Definition 5.4.1 Rules for the Universal Quantifier
Example Flagged boxes at work
Proposition 5.4.1 Universal Quantifier and Conjunction
Example A Proof to Check
Example Instances of $\mathrm{\forall I}$
Exercise A1
Exercise A2: Drill
Exercise B1: A chain, for every x
Exercise B2: Contraposition under a quantifier, used later
Exercise B3: A number is at most its absolute value, for every number
Exercise B4: Back to Exercise C2 of Section 5.3
Exercise B5: Derive or break: properties of a relation, used later
Exercise C1: How fresh is fresh?
Exercise C2: Find the error

5.5 Proving "There Exists": Exhibit a Witness

Definition 5.5.1 Existential Introduction
Proposition 5.5.1 Every Implies Some
Example Derivations with existential introduction
Example Instances of $\mathrm{\exists I}$
Exercise A1
Exercise A2: Drill
Exercise B1: Postpone, then choose
Exercise B2
Exercise B3
Exercise B4: Derive or break
Exercise C1: The conclusion clause of for-all-introduction, used later
Exercise C2: A witness is not a name, used later

5.6 Using "There Exists": Name a Witness

Definition 5.6.1 Rules for the Existential Quantifier
Proposition 5.6.1 Some Distributes Over And, One Way
Example Derivations with existential elimination
Proposition 5.6.2 Some-All Gives All-Some
Example The sum of two even integers is even
Theorem 5.6.3 The Barber
Example Instances of $\mathrm{\exists E}$
Exercise A1
Exercise A2: Drill
Exercise B1
Exercise B2: Fix, obtain, choose, faded
Exercise B3
Exercise B4: Derive or break
Exercise C1
Exercise C2: Find the error, used later
Exercise C3: The diagonal of a list

5.7 Equality

Definition 5.7.1 Rules for Equality
Proposition 5.7.1 Equality Is Symmetric and Transitive
Proposition 5.7.2 Leibniz’s Law
Example Equal Sets Have the Same Elements
Example Instances of $\mathrm{{=}E}$
Exercise A1
Exercise A2: Drill
Exercise B1: The identity is unique
Exercise B2: Rewrite, and turn round
Exercise B3: Derive or break
Exercise C1: Two different objects

5.8 Unique Existence, Counting and Descriptions

Definition 5.8.1 Unique Existence
Proposition 5.8.1 Two Halves of Unique Existence
Definition 5.8.2 Counting with Equality
Example Exactly Two Square Roots of One
Definition 5.8.3 Definite Description
Proposition 5.8.2 Definitions Prove Nothing New
Exercise A1
Exercise A2: Drill
Exercise B1: Exactly two, by halves
Exercise B2: A unique square root of zero
Exercise B3: Exactly one fixed point
Exercise B4: The empty set is unique
Exercise B5: Composites of one-to-one maps
Exercise C1: Two unique quantifiers do not commute
Exercise C2: “At most one”, two ways
Exercise C3: One and one make two
Exercise R1
Exercise R2
Exercise R3
Exercise R4

Working with Quantifiers: Translation, Laws and Search

6.1 Translating Mathematics: Nested and Bounded Quantifiers

Example Five definitions, translated
Example Five traps, each with a separating reading
Proposition 6.1.1 Rules for Bounded Quantifiers
Exercise A1
Exercise A2: Drill
Exercise B1: Three definitions
Exercise B2: A bounded rehearsal
Exercise B3: One key, twenty sentences
Exercise B4: Unfold, then fold back
Exercise C1: Where the $\forall x$ stands
Exercise C2: Six orders, four statements
Exercise C3: Eventually, therefore infinitely often

6.2 Negating and Moving Quantifiers

Proposition 6.2.1 Quantifier Negation
Proposition 6.2.2 Negated Implication
Proposition 6.2.3 Negating Bounded Quantifiers
Proposition 6.2.4 Replacement of Provable Equivalents
Example Three negations from analysis
Example The square for multiples of 4 and squares
Proposition 6.2.5 Arbitrarily Close Numbers Are Equal
Proposition 6.2.6 Distribution of Quantifiers
Proposition 6.2.7 Passage Laws
Example Bringing a formula into prenex form
Exercise A1
Exercise A2: Drill
Exercise B1: Four negations
Exercise B2: Two passage laws in one derivation
Exercise B3: Choosing $\varepsilon$ from the data
Exercise B4: Derive or break
Exercise B5: Find the error
Exercise C1: Two prenex forms
Exercise C2: Exit check: negations
Exercise C3: “There exists” from “for every”

6.3 Finding First-Order Derivations

Example A search that waits for its witnesses
Definition 6.3.1 Propositional Skeleton
Proposition 6.3.1 Tautological Steps on the Skeleton
Example A propositional core inside a flagged box
Example One pair of predicates, four tasks
Exercise A1
Exercise B1: Derive or break, twelve claims
Exercise B2: Two witnesses in a row
Exercise B3: How much TAUT saves
Exercise C1: Some index decides, used later
Exercise C2: Every M is P, every M is S, so some S is P?

6.4 Uniformly Continuous Implies Continuous, Rule by Rule

Example Uniformly continuous implies continuous
Example The search from C to UC
Example The square function on the real line
Example The negation at work, in one derivation
Example A “proof” that continuity gives uniform continuity
Exercise A1
Exercise A2: Drill
Exercise B1: Lipschitz implies uniformly continuous
Exercise B2: Put the proof in order
Exercise B3: The square root
Exercise B4: Witness functions
Exercise C1: Composition, half done
Exercise C2: Gluing two sets
Exercise C3: Exit check: a quantifier derivation
Exercise R1
Exercise R2
Exercise R3

Models and Theories

7.1 Structures and Satisfaction

Definition 7.1.1 Structure
Definition 7.1.2 Assignment
Definition 7.1.3 Satisfaction
Lemma 7.1.1 Free Variables Coincidence Lemma
Definition 7.1.4 Semantic Entailment in Predicate Logic
Example A Semantic Proof, Clause by Clause
Example The Drinker Sentence, by Meaning
Exercise A1
Exercise A2: Drill
Exercise B1: One sentence, two pictures
Exercise B2: A model on three elements
Exercise B3: Is it a structure?
Exercise C1: Proofs by meaning
Exercise C2: Challenge: only the symbols that occur matter

7.2 Counter-models

Example The swap of $\exists$ and $\forall$
Example A Counter-model, Found by the Procedure
Example Size One Fails, Size Two Works
Example Three Classes of Sentences
Exercise A1
Exercise A2: Drill
Exercise B1: Three counter-models, used later
Exercise B2: Prove it or break it
Exercise B3: The converse from Section 5.4
Exercise B4: Each side condition earns its place
Exercise C1: True in every finite model, used later
Exercise C2: A sentence with no finite model, used later
Exercise C3: Exit check: formalize, negate, decide
Exercise C4: The least size of a counter-model

7.3 Soundness for Predicate Logic

Lemma 7.3.1 Substitution Lemma
Corollary 7.3.2 Renaming Keeps Meaning
Theorem 7.3.3 Soundness for Predicate Logic
Corollary 7.3.4 Counter-models
Exercise A1
Exercise B1: The $\mathrm{\exists I}$ case
Exercise B2: Three non-derivability results
Exercise C1: The $\mathrm{\exists E}$ case
Exercise C2: “Free for” is needed

7.4 Theories and Their Models

Definition 7.4.1 Theory
Definition 7.4.2 Model of a Theory
Example Axioms, Models and Non-models
Example The Six Symmetries of a Triangle
Proposition 7.4.1 A Group Has Only One Identity
Definition 7.4.3 Inconsistent Theory
Proposition 7.4.2 A Theory with a Model Is Consistent
Proposition 7.4.3 Independence by Models
Example Reflexive, Symmetric, Transitive: Each Independent of the Other Two
Exercise A1
Exercise A2: Drill
Exercise B1: Construct a relation, or show none exists, used later
Exercise B2: A sentence true in one structure and false in the other
Exercise B3: Derive a theorem of a theory
Exercise C1: Describe every model
Exercise C2: The partial order axioms are independent
Exercise C3: Exit check: a theory checked three ways

7.5 Definability and Isomorphism

Definition 7.5.1 Definable Set
Example Sets Defined by Formulas
Example Maximum, Maximal, Supremum
Definition 7.5.2 Isomorphism of Structures
Theorem 7.5.1 Isomorphic Structures Satisfy the Same Sentences
Corollary 7.5.2 Automorphisms Preserve Definable Sets
Example Zero Cannot Be Defined from the Order of the Integers
Exercise A1
Exercise A2: Drill
Exercise B1: Define it by a formula
Exercise B2: What does this formula define?
Exercise B3: Automorphisms of small structures
Exercise C1: The definable subsets of $(\mathbb{Z}, <)$
Exercise C2: Challenge: the automorphisms of $(\mathbb{Q}, <)$
Exercise R1
Exercise R2
Exercise R3
Exercise R4

7.6 What First-Order Logic Can and Cannot Say

Theorem 7.6.1 Gödel’s Completeness Theorem
Theorem 7.6.2 Compactness Theorem
Theorem 7.6.3 Löwenheim–Skolem Theorem
Example A Model of Arithmetic with an Infinite Number
Exercise A1
Exercise A2: Drill
Exercise B1: Arbitrarily large finite models
Exercise B2: Which theorem settles it?
Exercise C1: “Finite” is not first-order
Exercise C2: Challenge: least elements in a non-standard model

From Derivations to Mathematical Prose

8.1 The Connective Rules in Prose

Example Two parts, and one part
Example A hypothesis assumed, a lemma cited, a contrapositive announced
Example Two cases, a weakening, a refuted disjunct
Example A negative claim, its positive form, and an empty case
Example One proof by contradiction, read two ways
Example Both directions, the second by cases
Example Three conditions, one cycle
Example A direct proof in costume
Example A contrapositive in costume
Exercise A1
Exercise A2: Drill
Exercise B1: Take off the costume
Exercise B2: Where the classical step sits
Exercise B3: Two clauses of a least upper bound
Exercise B4: Two integers of the same parity
Exercise C1: Euclid without the contradiction
Exercise C2: Which face, and the weakest form

8.2 The Quantifier Rules in Prose

Example A constant sequence
Example The reciprocals tend to zero
Example A sequence has at most one limit
Example Two inclusions
Example An induction, and a legitimate symmetry
Exercise A1
Exercise A2: Drill
Exercise B1: Ambiguous English
Exercise B2: An induction, annotated
Exercise B3: Six, two and three, used later
Exercise C1: When “similarly” is honest
Exercise C2: Moving a quantifier changes the meaning

8.3 Four Levels of One Proof

Definition 8.3.1 Levels of Proof
Definition 8.3.2 Silent Steps
Example The irrationality of the square root of two at four levels
Example Uniformly continuous implies continuous, at four levels
Example Two columns
Exercise A1
Exercise A2: Drill
Exercise B1: Some-all gives all-some, on the natural numbers
Exercise B2: Back from prose to a skeleton, with blanks
Exercise B3: A column of reductions
Exercise C1: Arbitrarily close numbers, at two levels
Exercise C2: Exit check: levels
Exercise C3: Back from prose to a skeleton

8.4 Reading a Proof: Self-Explanation

Example Explaining a proof, well and badly
Exercise A1
Exercise A2: Drill
Exercise B1: Self-explain a counterexample
Exercise B2: The unjustified line
Exercise B3: Name the unstated facts
Exercise C1: A longer proof
Exercise C2: Challenge: A proof about derivations

8.5 Writing a Proof

Example A subset of a bounded set
Example Label every sentence
Example From a derivation to a paragraph
Example One of three, generalized
Exercise A1
Exercise A2: Drill
Exercise B1: From skeleton to prose
Exercise B2: Put the proof in order
Exercise B3: The last step
Exercise B4: Which proof generalizes?
Exercise C1: A constant found backwards
Exercise C2: Rewrite it properly
Exercise C3: From $\sqrt 2$ to $\sqrt 3$ , and not to $\sqrt 4$

8.6 Checking Proofs, and What Is Not Allowed

Example What is not allowed
Example Proof A
Example Proof B
Example Proof C
Example Proof D
Exercise A1
Exercise A2: Drill
Exercise B1: Two proofs in two columns
Exercise B2: Find the error
Exercise B3: Correct, or which entry?
Exercise C1: The second half
Exercise C2: A true conclusion
Exercise C3: Exit check: four student proofs
Exercise R1: A dialogue

8.7 The Dispute over Excluded Middle

Theorem 8.7.1 An Irrational Power of an Irrational Number Can Be Rational
Proposition 8.7.2 A Witness for an Irrational Power
Proposition 8.7.3 Excluded Middle Cannot Be Refuted
Exercise A1
Exercise A2: Drill
Exercise B1: Double negation of double negation elimination
Exercise B2: Reading proofs as methods
Exercise B3: Where the witness goes missing
Exercise B4: Census of the classical results
Exercise B5: Behind two negations, and one instance
Exercise C1: More witnesses
Exercise C2: Modus ponens survives Kolmogorov’s translation
Exercise R1
Exercise R2
Exercise R3
Exercise R4

8.8 Stages of Knowledge: Kripke Models

Definition 8.8.1 Kripke Model
Definition 8.8.2 Forcing
Example Two stages refute excluded middle
Lemma 8.8.1 Heredity
Theorem 8.8.2 Soundness without RAA
Corollary 8.8.3 Kripke Countermodel
Example A fork
Exercise A1
Exercise A2: Drill
Exercise B1: A chain of three stages
Exercise B2: Derive without RAA, or break with a Kripke model
Exercise C1: Peirce’s law and one instance of excluded middle
Exercise C2: Challenge: three negations are one