Proof methods, induction, and invariants

The polynomial $n^2+n+41$ gives a prime number for each integer from zero through thirty-nine. It is tempting to guess that it always gives primes. At forty it equals $1681=41^2$, so the unrestricted claim is false. Forty successful cases were useful evidence for a conjecture, but one later valid input refutes that conjecture. More successful tests would never repair this particular universal statement.

A proof has a different obligation: start from explicit hypotheses and definitions, and give an argument covering every case in the stated domain. A program correctness proof adds another distinction. Showing that a returned answer is correct does not establish that the program ever returns. You need both a result argument and a termination argument when the contract promises completion.

Retrieval check: write an implication’s contrapositive, describe an equivalence class, and prove an elementary set inclusion using an arbitrary member. Review Module 02 and Module 03 if needed. We use classical logic, ordinary finite lists, and natural numbers including zero. Statements about all lists mean all finite lists unless explicitly stated otherwise.

A theorem is a statement established by proof. Its hypotheses specify the assumptions under which its conclusion follows. A lemma is a proved supporting statement used within another argument; the name describes its role rather than a lesser standard of correctness. A conjecture is a proposed statement still needing justification. A successful example illustrates a theorem or supports a conjecture, but it is not a substitute for proof of an unrestricted claim.

Before choosing a method, rewrite the claim with its domain and logical structure visible. “Odd numbers multiply to odd numbers” means: for all integers a,b, if both are odd then their product is odd. The universal scope and implication suggest taking arbitrary integers satisfying the hypotheses, then using the definition of odd. There is no need to enumerate integers or use an advanced theorem when the definitions supply the argument directly.

This short argument has an architecture worth copying: name arbitrary allowed inputs, unpack the hypotheses, transform the expression using justified steps, and recognise the conclusion’s definition. Writing only the algebra omits why the introduced symbols exist and why their combination is an integer. Writing only “odd times odd is odd” repeats the claim. A proof connects the two with reasons.

An assumption is available within its scope. To prove $P\Rightarrow Q$, you may assume P and derive Q; you may not assume Q itself and treat its consequences as proof. Some calculations can be run backwards if every step is reversible, but then that reversibility should be stated. Squaring an equation or multiplying by a quantity that may be zero can lose equivalence or introduce extra candidates. A chain of implications is not automatically a chain of equivalences.

For a universal statement, your chosen input must be arbitrary within the domain. Starting with “let n=4” proves a fact at four, not at every n. For an existential statement, a chosen value may be exactly what is needed, provided it is a valid witness. For an equality of sets, arbitrary membership establishes both sides’ agreement. Logical structure tells you which form of evidence is relevant.

Keep notation stable. If k is introduced as an integer witnessing oddness, do not later silently use it for a list index or a different witness. If two existential hypotheses provide integers, use distinct names unless you have justified their equality. A clear proof is easier to audit because each symbol has a role and every conclusion has a reason. Brevity helps only when it leaves the necessary links visible.

Counterexamples need the same care. To refute $\forall x\in D,\ P(x)$, give $x\in D$ with P false. To refute an implication under a hypothesis, show the hypothesis true and the conclusion false. A negative input cannot refute a nonnegative-input claim; a case where the premise fails does not refute a conditional. You may still use such cases to clarify scope, but label their purpose correctly.

A direct proof derives the conclusion from the hypotheses. The odd-product proof is direct. A proof by cases splits the allowed domain into cases that cover it completely, then proves the conclusion in each. Cases may overlap, but they must not leave allowed inputs uncovered. The reason for choosing cases should relate to a definition or operation that behaves differently in those regions.

For $P\Rightarrow Q$, a contrapositive proof establishes $\neg Q\Rightarrow\neg P$. Module 02 proved these implications equivalent, so this method is logically justified. It is often convenient when not-Q gives a simpler representation than P. Do not confuse it with proving the converse $Q\Rightarrow P$ or inverse $\neg P\Rightarrow\neg Q$, which generally establish different statements.

A proof by contradiction assumes the hypotheses together with the negation of the desired conclusion, then derives an impossibility. In classical logic, no consistent allowed case can satisfy those assumptions, so the conclusion must hold under the hypotheses. The contradiction should be identifiable: a statement and its negation, a number both strictly above and not above another, or a violation of a previously established fact.

Contradiction and contrapositive can look similar, but their starting assumptions differ. For a contrapositive you assume not-Q and prove not-P. For contradiction you assume P and not-Q and derive false. Both methods are valid when applied to the intended statement. Selecting a method should simplify the reasoning, not supply an excuse to hide the conclusion among the assumptions.

To disprove a claim, use a counterexample rather than constructing an argument for its opposite by wishful algebra. “All functions preserve addition” fails for the square function at two and three; the valid counterexample settles the unrestricted claim. The opposite “no function preserves addition” is also false, since the identity function does. Negating a universal gives some failure, not failure of every possible object.

Proofs by cases need complete coverage in software contexts too. A search may return a successful position or an absence sentinel. Verifying only the successful branch leaves the absence branch unproved. A recurrence may have two base constructors. Handling one does not cover objects constructed from the other. Before reviewing algebra, list the cases required by the object’s definition.

When a theorem is imported rather than proved, state it and check its hypotheses. Later AI arguments may use a differentiability or convexity theorem. The conclusion is available only if the current function meets its assumptions. In this module the imported facts are elementary parity, integer arithmetic, and the logical rules already proved. Keeping that dependency visible prevents circular justification.

An existence statement requires at least one object satisfying the property. A constructive proof supplies that object or gives a procedure producing it, then verifies the property and domain. “There should be a solution” is not evidence. A candidate derived by algebra must be substituted back when the derivation may have introduced extra values or lost a domain restriction.

The uniqueness notation $\exists!x,\ P(x)$ combines existence and at-most-one. Showing “any two solutions are equal” alone proves at-most-one and can hold even when there are no solutions. For example, the real equation $x^2=-1$ has no solutions; the conditional comparison of two hypothetical real solutions says nothing about existence. Showing one solution alone also does not prove uniqueness, as $x^2=1$ has two real solutions.

A constructive proof can depend on a given input. To prove every integer x has a larger integer, define the witness $x+1$ and verify it. This proves $\forall x\exists y,\ y>x$, not that there is one fixed y larger than every x. Quantifier order from Module 02 remains relevant inside proofs. An algorithm constructing a witness for each input should state its input domain and guarantee.

Sometimes existence follows indirectly. If assuming no witness produces a contradiction, classical logic establishes a witness exists even without giving a convenient construction. That may suffice for a mathematical theorem but not for an implementation requiring an actual returned object. Distinguish the theorem’s existential conclusion from an algorithm’s operational promise to find and output a witness within available resources.

Uniqueness arguments often compare arbitrary hypothetical solutions. Suppose a and b are both least elements of a partial order. Each is below the other; antisymmetry gives equality. This does not show a least element exists in every partial order. The two incomparable singleton sets from Module 03 give a counterexample to existence. Separating these claims prevents a valid uniqueness lemma being overstated as an existence theorem.

Definitions can supply constructive procedures. For a nonempty finite list of integers, a minimum exists: start from its first member, then update the candidate when a smaller member appears. A full correctness argument needs an invariant saying the candidate is a minimum of the processed prefix, while termination follows from the finite number of elements. The construction suggests the proof, but saying “the algorithm obviously finds it” skips those obligations.

To show two representations define the same object, you may construct maps in both directions and verify their compositions recover the inputs. A bijection between records and identifiers would give unique reversibility, but a many-to-one class-label map does not. A constructive inverse requires both coverage of the intended inverse domain and uniqueness of the recovered output, as the previous module showed.

A counterexample can also be constructive: choose an object and verify exactly why it violates the claim. For “every relation that is symmetric is transitive,” the three-object closeness relation provides two present pairs and a missing closing pair. The witness need not be large or realistic to refute the statement; it needs to satisfy its declared assumptions. In application review, a small witness is often easier to understand and preserve.

Mathematical induction proves a family of statements indexed by natural numbers. To establish P(n) for every $n\ge n_0$, prove a base P($n_0$) and a step: for an arbitrary $k\ge n_0$, assume P(k) and derive P(k+1). The temporary assumption is the induction hypothesis. It is legitimate within the step because the step proves an implication; the base starts the chain of implications.

A missing base can leave a false family with a perfectly consistent algebraic step. The proposed odd-sum formula $\sum_{i=0}^{n-1}(2i+1)=n^2+1$ has a step that carries the extra one forward: adding $2n+1$ to $n^2+1$ gives $(n+1)^2+1$. Its base n=0 is false, so the induction does not establish anything. A step is an implication, and false antecedents do not manufacture true conclusions.

In strong induction, the step may assume every earlier case P($n_0$),…,P(k) to prove P(k+1). This is convenient when a recursive object depends on several smaller inputs or one smaller input not necessarily k. Strong induction and ordinary induction have the same proving power over naturals. Ordinary induction can track the stronger statement “all cases through k hold,” producing the strong hypothesis in its next step.

Every integer n≥2 can be expressed as a product of primes. Base two is prime. For the strong step, consider k+1. If it is prime, it is already a one-factor product. Otherwise it factors as ab with $2\le a,b<k+1$. The hypothesis supplies prime products for a and b, whose combined factors give one for k+1. This proves existence of a factorisation. It does not prove its uniqueness; that requires an additional argument.

Base coverage follows the step’s backward dependence. If your step reaches back by three, one base may not cover all residue positions. For example every integer n≥8 is $3a+5b$ for nonnegative integers a,b: bases 8=3+5, 9=3+3+3, and 10=5+5; for n≥11, n−3≥8 has such a representation by strong induction, and adding another three gives one for n. All three bases are needed for this particular argument.

The well-ordering principle says every nonempty subset of naturals has a least member. It explains induction through a smallest-counterexample argument. If a claimed family had a failure, select its least failed index. It cannot be the established base; the earlier index succeeds, so the induction step makes this index succeed too, a contradiction. This reasoning depends on a lower-bounded natural index domain, not an arbitrary collection with no least elements.

State the start index, the hypothesis’s range, and the exact target of the step. Assuming P(k+1) while proving P(k+1) is circular. Proving P(k) implies P(k+2) with only base zero may cover even indices and leave odd indices unproved. Testing the first several cases can reveal these mistakes, but the written argument must show how its base cases and step cover the whole claimed domain.

Some objects are defined by how they are built rather than by an integer formula. A finite list is either empty or a head followed by a smaller tail list. A finite full binary tree is either a leaf or a node with exactly two child trees. A recursive definition should specify every constructor, the allowed smaller pieces, and a base. These rules define the domain over which a structural proof must operate.

For lists, write $[]$ for empty and $h::t$ for head h with tail t. Define length by $\ell([])=0$ and $\ell(h::t)=1+\ell(t)$. Define concatenation by $[]\mathbin{+\!+}b=b$ and $(h::t)\mathbin{+\!+}b=h::(t\mathbin{+\!+}b)$. The notation names a mathematical operation, not Python syntax. Python lists and + can implement the corresponding finite behaviour, though an efficient implementation need not copy this recursive definition literally.

Structural induction proves a property for the base constructors, then for every composite constructor assuming it for the constituent smaller structures. It follows the grammar of the object. You do not assume the property of the object currently being proved; you assume it of its already smaller components and show the constructor preserves it. The argument covers every object generated by the finite construction rules.

A tree proof may need two hypotheses. Let L(T) count leaves and I(T) count internal nodes of a finite full binary tree. Claim L(T)=I(T)+1. For a leaf, L=1,I=0. For a node with child trees A,B, leaf counts add and internal count is $1+I(A)+I(B)$. Using the two hypotheses gives $L(A)+L(B)=I(A)+I(B)+2=I(T)+1$. The “exactly two children” condition matters; the formula need not hold for a general tree.

A recursive computation also needs termination. Calling a function on the tail of a finite nonempty list decreases length by one until empty. Calling it on the same list again does not. A useful termination measure takes values in naturals and decreases strictly on every recursive call. Finite list length is such a measure. A decrease in an arbitrary real number is insufficient: the sequence 1,1/2,1/4,… decreases forever without reaching zero.

Recursion on integers needs a declared allowed domain and a reachable base. A countdown on nonnegative n with base zero and call n−1 when n>0 terminates because n decreases in naturals. Allowing negative inputs without another base can make repeated subtraction move away from zero. A syntactically present base case is not enough; every allowed call path must eventually reach a handled case.

Structural induction is closely related to induction on size, but its shape can make assumptions clearer. For two-child trees, assuming facts about both smaller children is more direct than inventing an arbitrary traversal order. For a recursive expression language with several constructors, each constructor becomes a proof case. Leaving one out leaves that part of the domain unproved, even if all examples use the handled constructors.

A proof of a recursive definition’s property need not establish a fast implementation. Correctness and operation count are separate questions. A recursive concatenation may repeatedly copy data in a particular language, even though the length identity is mathematically correct. Module 06 will analyse growth and recurrences. Here, first establish that the operation is defined, terminates on allowed finite structures, and satisfies its claimed property.

A loop invariant is a predicate that holds at a fixed point on every iteration reachable from the precondition. To use it in a correctness proof, establish initialisation, preservation, and exit consequence. The predicate need not describe every line of the loop; it must describe the chosen observation point consistently. An invariant assertion passing on a few runs is useful instrumentation but is not the general proof.

Consider first-match search on a fixed finite list a of n integers and integer target t. Start i=0. At each loop head while i<n, if $a_i=t$, return i; otherwise increment i. At ordinary exit return −1. Assume comparisons and list access terminate, and the list is not mutated during search. These assumptions make the state model clear and exclude changing data from silently invalidating the argument.

Use the invariant at the loop head:

It states a valid boundary and absence of matches in the processed prefix. Initially i=0 and the prefix is empty, so both clauses hold. For preservation, assume the invariant and guard i<n. If the current entry is not the target, increment to i+1. The old prefix has no match and the newly included old position i also has no match; the new prefix therefore has none. The new boundary remains at most n.

The invariant supplies a partial-correctness argument: every returned result satisfies the contract. To prove termination, use the variant $V=n-i$. It is a nonnegative integer at each loop head. Any iteration continuing rather than returning increments i, so V decreases by exactly one. A nonnegative integer cannot decrease strictly forever, and the loop cannot continue beyond n unsuccessful comparisons. A successful branch terminates immediately.

An invariant alone need not imply any decrease. A faulty loop that repeatedly inspects the same nonmatching first item can preserve “no match before i” with i=0 forever. Its returned results, if any, may still satisfy a partial-correctness statement, but a total-correctness promise fails. Conversely, a loop can terminate and return a wrong position. Both obligations need independent reasoning.

Boundary details matter. After examining an entry, the processed region changes from indices less than i to indices at most i; after incrementing, that same region is described as indices less than the new i. Confusing old and new values is a common preservation error. Use names such as $i_{old}$ and $i_{new}=i_{old}+1$ when the distinction is unclear, and specify exactly where the predicate is asserted.

The same method applies to minimum search, counting, and accumulation. A running total invariant might say “the accumulator equals the sum of entries before i.” Initialisation uses an empty sum, preservation adds the next term, and exit gives the complete sum. A decreasing unprocessed-count variant establishes termination. Each algorithm needs its own predicate; merely copying the words initialisation and preservation without showing the transitions is not a proof.

Proofs and executable checks work together. Assertions can reveal a misstated invariant, and small edge cases can reveal a missing branch. A proof gives the reason the property holds for every allowed finite input, under the assumptions. If real code mutates a, uses a different stop condition, or returns after checking a later duplicate, compare that implementation with the proved transition rules rather than assuming the theorem transfers automatically.

Use Python 3.11 or later; all labs are standard-library scripts. See the Python primer for running files. For each lab predict the result, explain the mathematical obligation being checked, and diagnose a variation. Ten explanation points per lab divide into prediction 3, interpretation 4, and fault analysis 3. Assertions verify actual executions; your written proof must still cover arbitrary allowed inputs.

Fifty minutes: predict the finite-sum outputs and the polynomial’s first displayed counterexample. Run the script. Explain why nine successful sum checks do not prove the infinite family, while the value at forty refutes the prime conjecture. Reconstruct the sum induction in Section 4 after your second session. As a variation, change the sum range to exclude n and find the smallest failing nonnegative case. Preserve the counterexample and distinguish an implementation fault from a false theorem.

Download lab1_evidence.py

"""Successful finite checks support debugging; one valid counterexample refutes."""
from math import isqrt


def prime(n):
    return n >= 2 and all(n % divisor for divisor in range(2, isqrt(n) + 1))


def main():
    for n in range(9):
        actual = sum(range(n + 1))
        expected = n * (n + 1) // 2
        assert actual == expected
        print(f"n={n}: sum={actual}, formula={expected}")
    first_failure = next(n for n in range(51) if not prime(n * n + n + 41))
    value = first_failure * first_failure + first_failure + 41
    assert first_failure == 40 and value == 41 * 41
    print("Polynomial prime claim passes n=0 through 39.")
    print(f"Counterexample n={first_failure}: value={value}=41*41")
    print("The sum checks cover n=0..8; its general proof is separate.")


if __name__ == "__main__":
    main()

n=0: sum=0, formula=0
n=1: sum=1, formula=1
n=2: sum=3, formula=3
n=3: sum=6, formula=6
n=4: sum=10, formula=10
n=5: sum=15, formula=15
n=6: sum=21, formula=21
n=7: sum=28, formula=28
n=8: sum=36, formula=36
Polynomial prime claim passes n=0 through 39.
Counterexample n=40: value=1681=41*41
The sum checks cover n=0..8; its general proof is separate.

Fifty minutes, after Section 6: predict the loop-head rows for a successful late match, an absent target, a first-position duplicate, and the empty list. Run the script and label initialisation, preservation, successful return, and normal exit. Explain which assertion checks the invariant and which checks the variant decrease. Change the increment from one to two; locate a skipped-match case and explain why the old preservation argument no longer establishes absence over the whole processed prefix.

Download lab2_search_invariant.py

"""First-match search with assertions at the loop head and a separate variant."""


def first_match(items, target):
    n, i = len(items), 0
    while i < n:
        invariant = 0 <= i <= n and all(value != target for value in items[:i])
        assert invariant
        print(f"  head: i={i}, prefix={items[:i]}, invariant={invariant}, variant={n-i}")
        if items[i] == target:
            assert all(value != target for value in items[:i])
            return i
        previous_variant = n - i
        i += 1
        assert n - i < previous_variant
    assert i == n and all(value != target for value in items)
    print(f"  exit: i={i}, invariant=True, variant=0")
    return -1


def main():
    cases = [([2, 5, 2, 7], 7, 3), ([2, 5, 2, 7], 3, -1), ([4, 9, 4], 4, 0), ([], 9, -1)]
    for items, target, expected in cases:
        print("items=", items, "target=", target)
        result = first_match(items, target)
        assert result == expected
        print("  result=", result)
    print("Assertions check these executions; the lesson proves the general obligations.")


if __name__ == "__main__":
    main()

items= [2, 5, 2, 7] target= 7
  head: i=0, prefix=[], invariant=True, variant=4
  head: i=1, prefix=[2], invariant=True, variant=3
  head: i=2, prefix=[2, 5], invariant=True, variant=2
  head: i=3, prefix=[2, 5, 2], invariant=True, variant=1
  result= 3
items= [2, 5, 2, 7] target= 3
  head: i=0, prefix=[], invariant=True, variant=4
  head: i=1, prefix=[2], invariant=True, variant=3
  head: i=2, prefix=[2, 5], invariant=True, variant=2
  head: i=3, prefix=[2, 5, 2], invariant=True, variant=1
  exit: i=4, invariant=True, variant=0
  result= -1
items= [4, 9, 4] target= 4
  head: i=0, prefix=[], invariant=True, variant=3
  result= 0
items= [] target= 9
  exit: i=0, invariant=True, variant=0
  result= -1
Assertions check these executions; the lesson proves the general obligations.

Fifty minutes: the proposed odd-sum formula has an internally consistent algebraic step but a false base. Predict all four displayed rows and explain why that step cannot start induction. The recursion trace is deliberately bounded to five displayed calls so the lab does not hang; it illustrates a call that repeats the same n. Explain why the trace bound is not a termination proof of the faulty recursion, and why the repaired countdown has a valid natural-number measure.

Download lab3_faulty_arguments.py

"""Expose a missing induction base and a non-decreasing recursive measure."""


def main():
    print("Proposed identity: sum of first n odd numbers = n^2 + 1")
    for n in range(4):
        actual = sum(2 * i + 1 for i in range(n))
        candidate = n * n + 1
        step_matches = candidate + 2 * n + 1 == (n + 1) ** 2 + 1
        print(f"n={n}: actual={actual}, candidate={candidate}, proposed step consistent={step_matches}")
    print("Base at n=0 fails: 0 != 1. A valid algebraic step does not supply a base.")
    faulty_trace = [5] * 5
    correct_trace = list(range(5, -1, -1))
    print("Bounded illustration of faulty calls countdown(n):", faulty_trace)
    print("Correct calls countdown(n-1):", correct_trace)
    faulty_decreases = all(b < a for a, b in zip(faulty_trace, faulty_trace[1:]))
    correct_decreases = all(b < a for a, b in zip(correct_trace, correct_trace[1:]))
    assert not faulty_decreases and correct_decreases
    print("Natural-number measure strictly decreases:", faulty_decreases, correct_decreases)
    print("Five displayed faulty calls are a trace limit, not termination of that recursion.")


if __name__ == "__main__":
    main()

Proposed identity: sum of first n odd numbers = n^2 + 1
n=0: actual=0, candidate=1, proposed step consistent=True
n=1: actual=1, candidate=2, proposed step consistent=True
n=2: actual=4, candidate=5, proposed step consistent=True
n=3: actual=9, candidate=10, proposed step consistent=True
Base at n=0 fails: 0 != 1. A valid algebraic step does not supply a base.
Bounded illustration of faulty calls countdown(n): [5, 5, 5, 5, 5]
Correct calls countdown(n-1): [5, 4, 3, 2, 1, 0]
Natural-number measure strictly decreases: False True
Five displayed faulty calls are a trace limit, not termination of that recursion.

Exercises 1–12 take 140 planned minutes and earn five points each. The two optional extensions add 25 minutes. State assumptions, the proof’s scope, and why each decisive step follows. A proof template with empty obligations earns no credit for the missing argument.

Nine choices receive automatic feedback; the written proof outline supplies the tenth point after review. A useful answer states which obligation is met and which remains open.

Required, 25 minutes: in the open textbook linked by MIT Mathematics for Computer Science, read its proof-method and induction introductions. Label a proof’s hypotheses, base, induction hypothesis, and target. Compare a direct argument with an indirect one.

Required, 11 minutes: read the recursive-data/structural-induction discussion, focusing on the constructors of one finite structure. List the exact base and step cases, and identify the smaller objects to which the hypothesis applies.

Required, 9 minutes: read the state-machine or invariant discussion and identify its observation point. State separately what proves the desired state property and what establishes progress or termination. These short selections total the forty-five-minute reading budget; longer proofs are optional.

Optional: consult the official Python assert statement documentation when explaining the limits of executable assertions. The lesson’s proofs and diagrams are original.

A proof follows a statement’s logical structure: arbitrary inputs for universals, witnesses for existence, comparison of hypothetical solutions for uniqueness, and covering cases for piecewise definitions. Induction covers indexed chains or recursively built structures. Program correctness uses an invariant tied to a specific program point; termination needs a separate well-founded measure.

Checkpoint combining earlier ideas: search a list of requests for the first one satisfying $admin\lor(owner\land approved)$. Translate the predicate using Module 02, then replace equality-to-target in the search invariant by failure of this predicate. Prove that a returned index is the first eligible request and that −1 means none is eligible. Explain why a parenthesisation error changes the proved specification even if the search loop itself is correct.

Exit task: produce one direct proof, one complete induction, and one search correctness/termination argument without looking at the examples. Use exercises 60, lab explanations 30, and quiz 10. Every missing base, circular assumption, or failed progress condition should be corrected and explained before moving on. Module 05 uses these reasoning tools to justify counts rather than merely apply formulas.