Working with Quantifiers: Translation, Laws and Search

A first course in analysis defines “$a_n\to L$” with three quantifiers and two bounds, then asks for a proof that a sequence does not converge, which starts from its negation. Chapter 5 gave the rules one per section; this chapter puts them to work: turning a definition into a formula, negating and rearranging it by laws, and finding the derivation a claim needs. You know every quantifier rule. Can you turn a definition from analysis into a formula, negate it without error, and find the derivation it needs? It ends where Chapter 5 began: why “uniformly continuous implies continuous” has a short derivation and a false converse.

What you need. Chapters 1–5. From Chapter 3: the search method (Section 3.1) and the four kinds of task (Section 3.2). From Chapter 4: truth tables and semantic entailment (Definition 4.5.3), completeness (Theorem 4.8.4), the move test the subgoal (Section 4.7) and the TAUT step for propositional formulas (Definition 4.8.1). From Chapter 5: the four quantifier rules with their side conditions (Definition 5.4.1, Definition 5.6.1), bounded quantifiers and the convention for mixing kinds of number (Definition 5.1.1), substitution, free-for and renaming (Section 5.2), equality (Section 5.7), and counter-readings (Section 5.3). School arithmetic and the order of $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{R}$ are used in examples as facts.

Time. About 20 hours on the core track (all of A, one B and one C per section, the exit checks); about 35 hours for everything.

Minimum before Sets, Relations, and Cardinality. Chapters 1–6 and 8, core; Sections 7.1–7.2 before its Chapter 3.

How to read this chapter. Every section is on the first reading, with its folds closed. The folds hold the proofs of the bounded rules, of the replacement rule and of TAUT on the skeleton, the derivations of the distribution and passage laws, and short remarks on edge cases. They are not optional: later proofs may use them.

Roadmap

• Translating mathematics. Definitions from analysis as formulas, worked from the outside in; the bounded rules; five traps, each shown wrong by a reading; “infinitely many” against “eventually”.
• Negating and moving quantifiers. “Not every” is “some not”; negation pushed inward by the replacement rule; the four forms A, E, I, O and their square; the laws that move a quantifier across a connective, and prenex form.
• Finding first-order derivations. The search method with flags and witnesses; TAUT on the skeleton; the propositional core; the four kinds of task; a library of sequents and a battery.
• Uniformly continuous implies continuous, rule by rule. The capstone derivation, the lines where the converse breaks, $x^2$ as the counter-reading, and witness functions $\delta (\epsilon )$ against $\delta (x,\epsilon )$.

Named moves

• Read it back. Read a translation back into words before using it. (Section 6.1)
• Negate quantifier by quantifier. Push $\mathrm{\neg }$ inward, swapping $\mathrm{\forall }$ and $\mathrm{\exists }$, keeping the bounds. (Section 6.2)
• Name the witness early, then instantiate at the term you need. Chapter 5’s two moves, in that order. (Section 6.3)
• The propositional core. Instantiate at the names in play, reason propositionally, with TAUT, then close the boxes. (Section 6.3)
• Test the subgoal by a counter-reading. Section 4.7’s move, with quantifiers. (Section 6.3)
• Read the dependency off the boxes. A witness may depend only on the flags whose boxes enclose it. (Section 6.4)

Where this goes. Analysis on the Real Line, Chapter 1 proves from the real-number axioms the facts about $\mathbb{N}$ in $\mathbb{R}$ and absolute value that Sections 6.1 and 6.2 use as school facts, and it uses “not every” gives “some not” (Section 6.2) in its proof of the Archimedean property. Its Chapters 5 and 6 define continuity and uniform continuity, which Section 6.4 uses only as quantifier patterns. Picking a witness for every $\epsilon$ at once, as one function (Section 6.4), in general appeals to the axiom of choice, which Sets, Relations, and Cardinality, Chapter 3 states.

Summary

The bounded rules add no power (Proposition 6.1.1). “Not every” is “some not”, with one direction classical (Proposition 6.2.1); a negated implication is a conjunction (Proposition 6.2.2); a bound stays with its quantifier (Proposition 6.2.3). A part may be replaced anywhere by a provably equivalent part, by a syntactic induction (Proposition 6.2.4); a step right for propositional reasons alone is derivable (Proposition 6.3.1). The chapter translated and negated the definitions of analysis, and took the search method and the four tasks to quantifiers. The capstone derived “uniformly continuous implies continuous” (Example (Uniformly continuous implies continuous)) and located the side conditions that stop the converse.

What is open: every “break” here was a counter-reading. Does one rule out every derivation? Chapter 7 asks.

Terms

• A, E, I, O forms: every, no, some, some not (Section 6.2).
• alternation: a $\mathrm{\forall }$/$\mathrm{\exists }$ change in a prefix (Section 6.2).
• bounded rules: abbreviations, no new power (Proposition 6.1.1).
• contradictory, contrary: exactly one true; never both true (Section 6.2).
• negated implication: $\mathrm{\neg }(\phi \to \psi )$ is $\phi \wedge \mathrm{\neg }\psi$ (Proposition 6.2.2).
• passage laws: move a quantifier across a connective (Proposition 6.2.7).
• prenex form: every quantifier at the front (Section 6.2).
• propositional core: instantiate, reason propositionally, close (Section 6.3).
• propositional skeleton: prime parts read as letters (Definition 6.3.1).
• quantifier distribution: $\mathrm{\forall }$ over $\wedge$, $\mathrm{\exists }$ over $\vee$ (Proposition 6.2.6).
• quantifier negation: “not every” is “some not” (Proposition 6.2.1).
• replacement of provable equivalents: swap a part for an equivalent (Proposition 6.2.4).
• TAUT step, on the skeleton: propositionally right (Proposition 6.3.1).
• uniformly continuous: one $\delta$ for all points (Section 6.4).
• witness function: a witness depending on flags (Section 6.4).