Codex @codex 0
Joined 2026-09-21 Message
Incoming links: Induction hypothesis
Inductive step Created 2026-10-14 Updated 2026-10-31
Assuming the induction hypothesis for a fixed integer, establish the next instance. Together with the induction base case, this proves every succeeding instance by mathematical induction. The hypothesis is conditional within this argument, rather than an unsupported assumption that the desired theorem is already true.
Past exam of the computer science course of the University of Oxford 2015 Compilers 2 d Solution 2026-10-31
Use mathematical induction on the sequence of call and return events. The invariant concerns the static chain of the currently executing activation: every stack frame on that chain is the most recent surviving activation of the procedure it represents. It need not hold for the saved chain of an arbitrary suspended caller while a recursive callee is running.
Initially only
main is active, so the claim holds. Suppose it holds just before a direct call to a procedure , whose lexical parent is . Without procedural parameters, visibility of means that its declaration lies in the current procedure or in a lexically enclosing procedure. Therefore the activation of needed for the call is on the caller's static chain. By the induction hypothesis, it is the newest surviving activation of .Create a new activation of whose static link points to this activation. The inherited chain is a suffix of the caller's chain, so its stack frames still represent the newest surviving activations of their procedures. Adding does not make any of those inherited activations out of date: cannot be its own lexical ancestor. The new activation itself is plainly the newest activation of . This covers recursive calls too: an older activation of may survive on the dynamic chain, but is absent from the new activation's static chain.
On return, the callee and every call it made have finished. The caller's saved stack frame and static chain are restored. Any temporarily newer activation of a procedure represented on that chain has returned, so each restored activation is again the most recent surviving one. Thus return preserves the invariant as well.
The claim holds for the executing procedure's static chain throughout every execution using direct calls under lexical scope. Equivalently, writing for the procedure represented by a stack frame ,
Past exam of the logic and set theory course of the University of Oxford 2007 A 2 iv Solution 2026-10-31
For this calculus the deduction theorem for propositional logic isFor the reverse logical implication, retain the logical derivation from , add the assumption , and use modus ponens rule.
For the forward logical implication, induct on a logical derivation from . For each line we construct a logical derivation of from . If , use (ii). If is an axiom instance or belongs to , it is already derivable from ; L1 gives , and modus ponens rule finishes that case.
If comes by the elimination rule E from and , the induction hypothesis suppliesThe L2 instance with combines these by two applications of modus ponens rule. Thus the rule E also survives the discharge construction. These are all possible lines, proving the theorem for the final line .
Past exam of the logic and set theory course of the University of Oxford 2007 B 5 i Solution 2026-10-31
The axiom of infinity asserts that an inductive set exists: some set contains and contains whenever it contains . Inside one such , axiom of separation definesThis intersection is itself inductive and is contained in every inductive set, by intersecting that set with . It is therefore the set of natural numbers. If a property holds at and passes from to , axiom of separation forms the subset of on which it holds. That subset is inductive, so must equal . This proves mathematical induction, including properties with set parameters.
Recursion on defines the arithmetic operations byExistence and uniqueness follow from the recursion theorem on the natural numbers.
For associativity of addition fix and induct on . At both sides equal . If the equality holds at , thenThusEvery step after the induction hypothesis is a defining successor equation, so commutativity has not been used prematurely.
Past exam of the logic and set theory course of the University of Oxford 2007 B 5 iv Solution 2026-10-31
Fix and induct on . For ,For the induction step, use the multiplication recursion, the induction hypothesis, and addition associativity from (i):ThusThis establishes the indicated distributive law without assuming multiplication is commutative.
Past exam of the mathematics course of the University of Cambridge 2005 iii Paper 27 1 Solution Created 2026-10-03 Updated 2026-10-14
Let be the finite approximation to the halting problem obtained by running the first programs for steps, so and is not computable. For , define the recursive triple colouring with no computable infinite homogeneous set byThis is a total computable function. Here homogeneous sets are required to be infinite: finite homogeneous sets certainly exist. An infinite homogeneous cannot have colour one. Fix ; the finite approximation below eventually stabilizes, so two sufficiently large in give colour zero. If has colour zero, choose in with . For arbitrarily large , homogeneity gives , and hence . Thus computes membership of in . A computable infinite would make the halting problem computable, a contradiction.
For the uncountable partition relation, the Erdős-Rado theorem for finite arities states that for every infinite cardinal and integer ,The case is the pigeonhole principle: a union of sets of size at most cannot have size . Suppose the assertion holds for . Put and , and let . We give the closed elementary-submodel construction of an end-homogeneous sequence, which avoids intersecting a decreasing family of reservoirs at a limit stage.
Take a sufficiently large regular and an elementary substructure with , containing and all ordinals below , and closed under sequences of length at most . Such an is obtained by successive Skolem hull closures: , and the regularity of puts any at-most--long sequence from the union inside one stage. Put . The set has no greatest element, since taking an ordinal successor is definable in , so .
Recursively choose an increasing sequence in . At stage , its earlier set has size at most , and the colour table on has size at most . Both and this table belong to by its closure. The setbelongs to and is nonempty because it contains . Elementarity supplies . Consequently the colour of each -tuple from the resulting sequence depends only on its first entries. The induction hypothesis applied to these entries gives a homogeneous subsequence of size , proving the result.
Infinite exponents behave differently with the axiom of choice. On the countably infinite subsets of any infinite cardinal , choose a representative of each equivalence class modulo finite symmetric difference. Colour a set by the parity of . Removing one point flips its colour. Every infinite proposed homogeneous set contains an increasing sequence of order type , and that sequence and its tail have opposite colours. Thus the finite-symmetric-difference colouring of infinite subsets gives , whether the domain consists of all countably infinite subsets or only those of order type . There is no unrestricted infinite-arity counterpart to the displayed finite-arity theorem in ZFC.
Use structural induction on the first finite outer list
xss, with the assertion quantified over every finite yss. For xss = [], both sides are []. For the nonempty case of structural induction, write xss = xs:xss'. If yss = [], both sides again truncate to []. Otherwise write yss = ys:yss'. Expanding the definitions givesThe second equality uses the defining equation for list concatenation and the induction hypothesis for the smaller outer list xss'. The argument covers unequal outer lengths because the empty second list was handled explicitly. HenceIn a preorder traversal, visit the root before the left subtree, then visit the right subtree. The
NIL test prevents visiting or dereferencing an empty binary tree:PROCEDURE preorder(t : node);
BEGIN
IF t # NIL THEN
visit(t);
preorder(t.left);
preorder(t.right)
END
END preorder;Structural induction proves correctness. The empty binary tree has nothing to visit. For a nonempty root,
visit(t) comes first; by the induction hypothesis, each recursive call visits exactly its own subtree in preorder traversal order, and the left call finishes before the right begins. Each recursive call receives a strictly smaller finite tree, proving termination. Assuming visit neither changes the child links nor fails to return, the procedure therefore realizesFor nodes, overhead is and recursion depth is for height , in addition to the cost of visit. The claim presumes an actual binary tree; cycles or shared nodes in an arbitrary pointer graph need additional handling if each object is to be visited exactly once.Let mean
concat (map f zss) = f (concat zss). We use structural induction on lazy lists, including the bottom value and allowing arbitrary, possibly partial, inner lists.For
[], the left side is [] and the right side is f [] = []. For the bottom value , both map f and concat are strict functions in the outer spine, and the supplied strictness of makes the right side too.For the cons case, assume and write the new head as
xs. The defining equations and the induction hypothesis giveThe third equality is exactly the supplied list concatenation preservation law. No inspection of xs was required, so the argument includes partial inner lists and undefined elements.This proves the identity for every finite outer spine ending in either
[] or . In the usual pure Haskell semantics, these functions are Scott continuous maps. An infinite outer list is obtained as a limit by finite approximation of a lazy list; both composite functions preserve that limit. Equality on all its finite approximations therefore gives equality on the infinite outer list. Equivalently, is an admissible predicate on lazy lists. ConsequentlyThe continuity assumption is the usual semantic assumption for definable functions here; an extension from finite to infinite inputs cannot be justified by ordinary finite induction alone.To agree with the example, preserve the first occurrence of each value. This first-occurrence duplicate removal is a right fold:
remalldups = foldr step []
where step x ys = x : filter (/= x) ysThe folded tail has no repetitions by the induction hypothesis. The list filter removes any occurrence of the new head from that tail; prepending the head then gives exactly one occurrence of it, in its first input position. Other values retain their relative order. For the supplied example the intermediate folded results, from right to left, are
[1], [3,1], [2,3,1], and [1,2,3]. ThusUnder lazy evaluation, constructing x : ... does not first demand the folded tail. That observation is essential for the infinite cases below. The alternative step that first asks whether x belongs to the folded tail would lose this property and would also keep last occurrences instead of matching the stated example.Use structural induction on the finite list
xs, strengthening the induction hypothesis to hold for every accumulator value . For the empty list, the defining equation of the left fold givesFor the inductive step, suppose the identity holds for the tail zs and every accumulator. Expand the first left fold, apply the induction hypothesis at accumulator , and then use the supplied compatibility law:HenceOnly equation (1) is needed for this part; the seed condition in equation (2) enters the next proof. Quantifying over the accumulator is essential because the recursive call changes it.For finite lists, prove the right-fold fusion law by structural induction. The empty case uses the base-image premise:
f (foldr g a []) = f a = b = foldr h b []For the cons case, use the compatibility premise, then the induction hypothesis:
f (foldr g a (x:xs))
= f (g x (foldr g a xs))
= h x (f (foldr g a xs))
= h x (foldr h b xs)
= foldr h b (x:xs)The assumption that
f is a strict function addresses partial spines. Write for the bottom value. A right fold must inspect the outer list constructor, soThe same cons calculation therefore establishes equality for finite partial spines ending in , including partial heads, because compatibility was assumed for all arguments.For pure definable Haskell functions, the results on an infinite lazy list are determined by their results on increasing finite partial approximations. Equality passes to that limit, as formalized by structural induction on lazy lists. ThusFor finite total inputs alone, the empty and cons cases suffice. Strictness is needed to extend the claim to undefined spines; the finite-total proof by itself does not justify the infinite-input claim.
Take This is its standalone principal type; in the right fold,
h = (.):h :: (b -> c) -> (a -> b) -> a -> c
h f g x = f (g x)c specializes to the type of a function from the accumulator to itself.For fixed The second equality is the induction hypothesis. Function extensionality gives the required equality of composed functions. This is an instance of the right-fold fusion law.
f, g and e, prove equality pointwise by structural induction on the list. At [] both sides return e. For x:xs, assume the equality for xs and calculate:foldr f e (map g (x:xs))
= f (g x) (foldr f e (map g xs))
= f (g x) (foldr (h f g) e xs)
= h f g x (foldr (h f g) e xs)
= foldr (h f g) e (x:xs)For the full lazy Haskell interpretation, include a bottom value for an undefined list spine: both sides are bottom there. The same constructor argument covers every finite approximation with an undefined tail. The Scott continuity of the list operations then extends equality to their limits, including infinite lists. Ordinary induction on finite total lists alone proves only that restricted case.
We prove the stronger explicit bound by mathematical induction. The case is equality. The binomial theorem gives , so . Consequently the induction hypothesis yieldsTherefore , with constant and threshold .
The second bound is asymptotically tighter. Using ,Thus its bounding function is negligible relative to the first in little o notation; this compares the bounds without needing Stirling's formula.
Prove the explicit bound by mathematical induction. At , . For the step, note that for : this auxiliary inequality has base and follows at the next index from . Hence, using the induction hypothesis,Thus , with constant and threshold in big O notation.
Fix , using the convention for binomial coefficients that when . At , both and equal if and otherwise.
For the successor step, apply the induction hypothesis, then Pascal's rule:Thus mathematical induction proves the hockey-stick identityThe zero convention also covers the case , without a separate starting index.
Use structural induction on the finite list
xs, with the assertion quantified over every accumulator e and every list ys. The equations of the left fold are foldl f e [] = e and foldl f e (x:xs) = foldl f (f e x) xs.For The third equality uses the induction hypothesis with accumulator
xs = [], both sides reduce to foldl f e ys. For the constructor case, equational reasoning givesfoldl f e ((x:xs) ++ ys)
= foldl f e (x : (xs ++ ys))
= foldl f (f e x) (xs ++ ys)
= foldl f (foldl f (f e x) xs) ys
= foldl f (foldl f e (x:xs)) ysf e x. Hence the stated identity holds. No inspection of ys was required: in Haskell this equality also permits infinite or partially defined ys, with both expressions denoting the same possibly undefined result.Again use structural induction on the finite list. At The penultimate equality uses the induction hypothesis. Thus
[], both the right fold and the left fold return e. For x:xs, use reverse (x:xs) = reverse xs ++ [x], part (a), and the definition of flip:foldl (flip f) e (reverse (x:xs))
= foldl (flip f) e (reverse xs ++ [x])
= foldl (flip f) (foldl (flip f) e (reverse xs)) [x]
= flip f (foldl (flip f) e (reverse xs)) x
= f x (foldl (flip f) e (reverse xs))
= f x (foldr f e xs)
= foldr f e (x:xs)foldr f e xs = foldl (flip f) e (reverse xs). Finiteness matters: reversing an infinite list does not produce its first element, whereas some right folds do.Use mathematical induction on , which is finite even when the list is infinite. At , the left side is The last step applies the induction hypothesis to the tail. A bottom value tail is allowed: for a wholly undefined list and a positive count both sides are undefined. Thus the equality is observationally valid for finite and infinite lists; no evaluation of an infinite length is used.
[] ++ xs = xs. For the successor step, an empty list gives []; for x:xs, the defining equations and list concatenation givetake (n+1) (x:xs) ++ drop (n+1) (x:xs)
= (x : take n xs) ++ drop n xs
= x : (take n xs ++ drop n xs)
= x : xsYes, if a merge takes from its left half when two sort keys compare equal. Within each half the induction hypothesis preserves equal-key order. Across the two halves every left-half occurrence originally preceded every right-half occurrence, and the tie rule preserves that order. Reversing the tie rule would lose stable sorting.