mathematical-proof-logic

Mathematical Proof Logic

Mathematical proof is the oldest and most rigorous form of argumentation humans have developed. Its rigor comes from logic: every legitimate step in a proof must correspond to a rule of inference in some underlying logical system -- usually first-order logic with a background theory like ZFC set theory or Peano arithmetic. This skill is about the logical structure of proof, not the pragmatic heuristics for finding one. It answers the question "what makes this sequence of sentences a valid proof?" rather than "what trick should I try?" The complementary proof-techniques skill in the math department covers the latter.

Agent affinity: godel (metamathematics), tarski (semantic grounding), russell (Principia heritage)

Concept IDs: log-predicate-logic, log-proof-techniques, log-deductive-reasoning, log-mathematical-proof

Proof as Logical Object

A mathematical proof is, formally, a finite sequence of sentences in a formal language such that every sentence is either:

1. An axiom of the background theory,
2. A previously established theorem (lemma), or
3. Inferred from earlier sentences by an inference rule of the logic.

The final sentence is the theorem proved. This is the Hilbert-style view of proof: a proof is a tree (or list) of formulas with rule-applications as its edges.

In practice, working mathematicians almost never write proofs in this fully formal style. They write prose that could, in principle, be expanded into a formal proof. The logical skeleton is always there underneath -- it is what verification, peer review, and automated proof assistants check against.

The Underlying Logic

Most of mathematics runs on first-order logic (FOL) with a chosen background theory:

• ZFC set theory is the default for most of mathematics. Everything -- numbers, functions, groups, topological spaces -- is definable as a set.
• Peano arithmetic (PA) for number theory proper.
• Second-order logic in some contexts, but most practitioners prefer to stay first-order and handle second-order features set-theoretically.

Classical FOL is assumed unless the proof is explicitly constructive. In classical logic, double negation elimination (¬¬p → p) and the law of excluded middle (p ∨ ¬p) are available. In intuitionistic logic, they are not -- and proofs by contradiction that rely on them are rejected. Most mathematicians work classically; constructive mathematicians deliberately restrict themselves.

Proof Structures as Logical Patterns

The famous "proof techniques" of undergraduate math classes are all specific deduction patterns in FOL. Understanding them as logical patterns clarifies why they work.

Direct proof

To prove P → Q:

1. Assume P.
2. Derive Q.
3. Discharge the assumption, conclude P → Q (→I rule).

This is implication introduction, plain and simple.

Proof by contrapositive

To prove P → Q, instead prove ¬Q → ¬P. This works because P → Q ≡ ¬Q → ¬P (contrapositive equivalence in classical logic). Sometimes the contrapositive is much easier to work with.

Proof by contradiction (reductio ad absurdum)

To prove P:

1. Assume ¬P.
2. Derive a contradiction (some formula of the form φ ∧ ¬φ).
3. Conclude P (negation elimination + double negation).

This relies on classical logic's double negation elimination. Constructivists accept a narrower form: you can prove ¬P by deriving a contradiction from P, but not P by deriving a contradiction from ¬P.

Proof by cases

To prove Q from P₁ ∨ P₂ ∨ ... ∨ Pₙ:

1. Show Q follows from P₁.
2. Show Q follows from P₂.
3. ... and so on.
4. Conclude Q (disjunction elimination, ∨E).

The case split must be exhaustive -- every possibility must be covered -- and it is the author's job to state why.

Proof by induction

Mathematical induction is a schema. To prove ∀n ∈ ℕ P(n):

1. Base case: Show P(0) (or P(1), depending on where you start).
2. Inductive step: Show ∀k (P(k) → P(k+1)).
3. Conclude ∀n P(n) by the principle of induction.

The principle of induction is an axiom of Peano arithmetic. It is not derivable from the other axioms; it is a primitive claim about the natural numbers. Strong induction (assume P holds for all m < n, prove P(n)) is equivalent.

Existence proofs

To prove ∃x φ(x), two styles:

• Constructive: Exhibit a specific object t and show φ(t). This is ∃I on a concrete term.
• Non-constructive: Assume ¬∃x φ(x), derive a contradiction, conclude ∃x φ(x). This only works classically and does not tell you which x satisfies φ.

The distinction matters in some branches of mathematics (constructive analysis, type theory) and is invisible in most of ordinary mathematics.

Uniqueness proofs

To prove "there is exactly one x such that P(x)":

1. Existence: prove ∃x P(x).
2. Uniqueness: prove ∀x ∀y (P(x) ∧ P(y) → x = y).

The two halves are separate obligations.

Definitions, Axioms, Lemmas, Theorems

Mathematical texts distinguish several kinds of statements. The distinctions are mostly pragmatic but logically meaningful.

• Definition: A new symbol is introduced and given meaning in terms of already-established concepts. Logically, definitions are conservative extensions -- they add no new content but allow more compact expression.
• Axiom: A statement taken as true without proof. In a given theory, axioms are the base. Across theories, they are choices -- different axioms give different mathematics (Euclidean vs non-Euclidean geometry is the classic example).
• Lemma: A theorem proved as an intermediate step toward a larger result. Logically identical to a theorem, but flagged for the reader as auxiliary.
• Proposition: A minor theorem, usually stated without much fanfare.
• Theorem: A major result, the destination of a proof.
• Corollary: A result that follows immediately (often in a line or two) from a theorem.

All of these except definitions are claims to be proved, and the proof must be valid under the chosen logic and background theory.

Informal Prose and Its Formal Shadow

Mathematical writing is prose that encodes a formal proof. Reading it requires parsing the prose back into deductive structure. Some common phrases and their logical meaning:

| Prose | Logical meaning | |---|---| | "Let x be ..." | Universal generalization setup (∀I preparation) or ∃E witness | | "Assume for contradiction that ..." | Assumption for ¬I or indirect proof | | "Without loss of generality ..." | Implicit case reduction, often by symmetry | | "Clearly ..." | Author claims a step is obvious; reader must verify | | "It suffices to show ..." | Replace current goal with a sufficient condition | | "Conversely ..." | Proving the other direction of a biconditional | | "By hypothesis ..." | Reference to an earlier assumption | | "By definition ..." | Unfolding a definition |

The "without loss of generality" pitfall. "WLOG" is legitimate when a symmetry argument justifies it. It is fallacious when the author is actually doing only one case and pretending the other is symmetric without checking. Readers should always ask: what is the symmetry, and does it actually hold?

Worked Example: A Classical Proof

Theorem: √2 is irrational.

Proof. Assume for contradiction that √2 is rational. Then √2 = p/q for some integers p, q with q ≠ 0, where p/q is in lowest terms (i.e., gcd(p, q) = 1).

Then 2 = p²/q², so p² = 2q².

Thus p² is even, so p is even (since the square of an odd number is odd).

Write p = 2k for some integer k. Then (2k)² = 2q², so 4k² = 2q², so q² = 2k².

Thus q² is even, so q is even.

But p and q are both even, contradicting the assumption that gcd(p, q) = 1.

Therefore √2 is not rational. ∎

Logical skeleton:

1. Assumption for contradiction: ∃p ∃q (integers, q ≠ 0, gcd(p,q) = 1, √2 = p/q)
2. ∃E: introduce witnesses p, q.
3. Algebraic manipulation: p² = 2q² (arithmetic and definition of /).
4. Lemma: p² even → p even. (Contrapos