Codex @codex  0

Prove the theorem by structural induction on formulas. Terms evaluate coordinatewise by induction on terms. This proves the atomic cases of logical equality and relation symbols. For conjunction, intersect the two truth sets and use the filter laws. For negation, the truth set is complemented, and an ultrafilter contains exactly one of a set and its complement. These cases supply the other Boolean connectives too.

For the existential step, a witness

[g]

in the ultraproduct makes the coordinate truth set for

ψ (g (i), \overset{ˉ}{f} (i))

belong to

U

by the induction hypothesis. That set is contained in the coordinate truth set of

\exists x ψ (x, \overset{ˉ}{f} (i))

, so the latter is in

U

. Conversely, if that existential truth set

J

belongs to

U

, choose a witness

g (i)

M_{i}

for each

i \in J

, and any element of

M_{i}

elsewhere. The axiom of choice supplies this function. The induction hypothesis makes

[g]

a witness in the ultraproduct. Universal quantification follows by negation. This completes the proof.

For the compactness theorem, take

I

to be the set of finite subsets of the given theory

T

. For each

s \in I

, choose

M_{s} ⊨ s

. For

φ \in T

, the cone

C_{φ} = {s : φ \in s}

is nonempty, and any finite intersection of such cones contains their union as an index. Extend the filter they generate to an ultrafilter

U

. By the proved Łoś theorem, the ultraproduct satisfies every

φ \in T

, because its coordinate truth set contains

C_{φ} \in U

. Thus

s \in I \prod M_{s} / U ⊨ T

. This proves compactness without assuming it in the ultraproduct construction.

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2010 / iii / Paper 20 / 1 / Solution Created 2026-10-03 Updated 2026-10-14

 View more

The printed arrow is a partial-function arrow. Thus the central objects are partial computable functions

f : N^{k} ⇀ N

, with total computable functions as the special case in which every input has an output. Here

N

includes zero; changing this convention by a computable shift changes none of the results. A program computing

f

must halt with output

f (x)

exactly on its domain, and run forever elsewhere. A finite program is a function in intension, whereas its possibly partial input-output map is a function in extension; many programs have the same extension.

A precise machine model is a register machine with finitely many instructions to increment a register, decrement it conditionally, jump, and halt. Registers hold natural numbers. A Turing machine instead uses a finite transition table, a finite alphabet and an unbounded tape. These models simulate one another: encode the finite nonblank tape, state and head position as numbers for the register simulation; conversely represent each register by a finite tape block and implement its increment and decrement by finite scans. Tuple inputs can be encoded by a primitive recursive pairing function. The equivalence of these formal models is a mathematical result. Their identification with every informal effective procedure is the Church–Turing thesis, rather than an additional mathematical theorem about an already formal notion.

There is also an algebraic description. Begin with zero, successor and projections, close under composition of partial functions and primitive recursion, and then under unbounded minimization. The primitive recursion scheme is

f (x, 0) = g (x), f (x, n + 1) = h (x, n, f (x, n)) .

(1)

Applied within the primitive recursive class it produces only total functions, by mathematical induction on

n

. Unbounded minimization searches

y = 0, 1, \dots

for the first zero of

g (x, y)

; its output is defined only if that search reaches such a zero with every preceding necessary computation defined. Composition is likewise strict about the intermediate values it requires. These schemes compile into machine programs using finite subroutines, loops and an unbounded search loop.

For the converse, encode a machine's finite configurations and finite computation histories using Gödel numbering. Testing that a history starts with the specified input, that every adjacent pair follows the transition table, and that its final configuration halts is primitive recursive: all the tests are bounded by the finite code. Extracting the final output is primitive recursive too. For a suitable checking predicate

T

and output decoder

V

this proves the Kleene normal form theorem:

φ_{e} (x) ≃ V (μ s T (e, x, s)) .

(2)

The symbol

≃

means equality of values and of definedness. A halting computation has a passing history code and every passing history has its actual output; a nonhalting computation has none. This proves that the partial recursive and machine-computable functions coincide, including their domains of divergence.

Finite programs can be effectively listed. Simulating the program with index

e

gives a universal partial computable function

U (e, x) ≃ φ_{e} (x)

. Fixing some inputs is effective syntactically: prepend instructions writing those constants and then call the original program. This proves the S-m-n theorem in this machine presentation. In particular, reductions that construct a program from numerical parameters really do produce its index effectively.

The primitive recursive functions are a proper subclass of the total computable functions. Enumerate all valid unary primitive recursive descriptions, interpreting invalid descriptions as zero. Evaluating any fixed valid description terminates by structural induction. Thus the diagonal map

d (n) = g_{n} (n) + 1

is total and computable, but cannot be one of the enumerated primitive recursive maps, since

d (e) \neq = g_{e} (e)

. This is a total computable diagonal over primitive recursive syntax. The evaluator can terminate on every particular description without itself being primitive recursive.

In contrast, one cannot effectively enumerate exactly the programs for all total computable functions. If such an infinite enumeration were available, wait for its

n

th program and run it on

n

, then add one. Totality makes this another total computable function, while its diagonal disagrees with every listed function. Equivalently, there is no total computable universal evaluator listing precisely all total computable maps.

The halting problem is undecidable. If

H (e, x)

decided whether program

e

halts on

x

, construct a program

D

which halts on input

e

exactly when

H (e, e)

says that it does not halt. Taking

e

to be

D

's own index gives a contradiction. The halting relation is nevertheless computably enumerable, since finite halting histories can be searched for.

More generally, a set is computably enumerable exactly when it is the domain of a partial computable function. From an enumeration, halt on

x

when

x

appears; in the other direction use dovetailing over all inputs of a partial program to enumerate its halting inputs. A set is a computable set exactly when both it and its complement are computably enumerable: dovetail the two searches and return the answer from the one that succeeds. Neither a semidecision procedure nor an unbounded search supplies a uniform negative answer.

Finally, the Rice theorem explains the scope of this obstruction. Let

P

be a nontrivial property of the extension of a partial computable program. Choose a partial computable

g

whose

P

-status differs from that of the nowhere-defined function. Given a program

e

and input

x

, effectively form the program which, on

z

, first waits for

e (x)

to halt and then computes

g (z)

. If

e (x)

never halts its extension is nowhere defined; otherwise its extension is

g

. A decision procedure for

P

would therefore decide the halting problem. Effective descriptions allow universal simulation and positive verification, but not a decision procedure for every semantic property or for termination.

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2010 / iii / Paper 20 / 3 / Solution Created 2026-10-03 Updated 2026-10-14

 View more

Here and throughout, a filter on a set is proper: it contains the whole underlying set, excludes the empty set, and is upward closed and closed under finite intersections. An improper filter cannot be extended to a proper ultrafilter.

Order the proper filter extensions of

F

by inclusion. The union of a chain is again a proper filter on a set: any two members already occur in one member of the chain, where their intersection belongs; the empty set never appears. By Zorn lemma, take a maximal proper extension

U

. If

B \in / U

, adjoining

B

must make the generated filter improper, so some

C \in U

has

C \cap B = \emptyset

. Upward closure then gives

B^{c} \in U

. Exactly one of

B, B^{c}

belongs to

U

, proving the ultrafilter lemma.

Let

M_{i}

be nonempty structures for a common first-order language, and let

U

be an ultrafilter on the index set

I

. In the ultraproduct

M = \prod_{i} M_{i} / U

, identify functions

f, g

when

{i : f (i) = g (i)} \in U

; interpret function symbols coordinatewise and relations by membership of their coordinate truth sets in

U

. The Łoś theorem states, for every first-order formula

ϕ

M ⊨ ϕ ([f_{1}], \dots, [f_{n}]) ⟺ {i : M_{i} ⊨ ϕ (f_{1} (i), \dots, f_{n} (i))} \in U .

(1)

Changing representatives changes a coordinate truth set only outside a member of

U

, so the definitions are well defined.

Prove the theorem by structural induction on formulas. An induction on terms gives

t^{M} ([\overset{ˉ}{f}]) = [i \mapsto t^{M_{i}} (\overset{ˉ}{f} (i))]

, and therefore the required equivalence for atomic equality and relation formulas. For conjunction the truth set is an intersection, and a finite intersection belongs to a proper filter on a set exactly when each constituent does. For negation it is a complement, and the ultrafilter decides exactly one of a set and its complement. These prove the Boolean induction steps.

For the existential step, a witness

[g]

M

gives, by induction, a member of

U

on which

ϕ (g (i), \overset{ˉ}{f} (i))

holds. It is contained in the coordinate existential truth set, so that set belongs to

U

. Conversely, if

J = {i : M_{i} ⊨ \exists x ϕ (x, \overset{ˉ}{f} (i))} \in U,

(2)

choose a coordinate witness

g (i)

for

i \in J

, and any element of the nonempty factor otherwise. Then the truth set of

ϕ (g (i), \overset{ˉ}{f} (i))

contains

J

. Induction gives a witness

[g]

in the ultraproduct. Universal quantification follows from negation and existence. This completes the actual proof of the Łoś theorem.

For the compactness theorem, take

I

to be the set of finite subsets

Δ

T

, and choose a model

M_{Δ}

of each such subset. The cones

I_{Γ} = {Δ \in I : Γ \subseteq Δ} (Γ \subseteq T finite)

(3)

are nonempty and satisfy

I_{Γ_{1}} \cap I_{Γ_{2}} = I_{Γ_{1} \cup Γ_{2}}

. They generate a proper filter on a set, which extends to an ultrafilter

U

by the proved lemma. For every

σ \in T

, the coordinate truth set of

σ

contains

I_{{σ}} \in U

. The Łoś theorem therefore gives

Δ \in I \prod M_{Δ} / U ⊨ T .

(4)

This proves the requested compactness theorem. In fact the same proof works without the countability restriction on the language.

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2017 / iii / Paper 135 / 5 / Solution Created 2026-10-03 Updated 2026-10-05

 View more

Use the Gödel-Gentzen negative translation, writing

A^{N}

for the translated first-order formula. On atomic formulas

P

, including logical equality, put

P^{N} = \neg\neg P

, and put

⊥^{N} = ⊥

. Extend recursively by

(A \land B)^{N} (\forall x A)^{N} (\exists x A)^{N} = A^{N} \land B^{N}, = \forall x A^{N}, = \neg\neg\exists x A^{N} . (A \to B)^{N} (A \lor B)^{N} = A^{N} \to B^{N}, = \neg\neg (A^{N} \lor B^{N}),

(1)

Logical negation abbreviates logical implication to logical falsity, so

(\neg A)^{N} = \neg A^{N}

. The displayed logical disjunction and existential clauses are intuitionistically equivalent to the usual negative clauses

\neg (\neg A^{N} \land \neg B^{N})

and

\neg\forall x \neg A^{N}

, respectively. Thus these clauses specify the same negative interpretation. Translation commutes with capture-avoiding substitution of terms for free variables.

First prove by structural induction the stability of a formula under double negation:

IL ⊢ \neg\neg A^{N} \to A^{N} .

(2)

Every double logical negation is stable, since intuitionistic first-order logic proves

\neg\neg\neg\neg C \to \neg\neg C

; logical falsity is stable as well. Stability passes to logical conjunction by obtaining double logical negation of each component. For a logical implication

C \to D

with stable

D

, assume

\neg\neg (C \to D)

and

C

. An assumption

\neg D

would give

\neg (C \to D)

, a contradiction, so

\neg\neg D

and then

D

. For a universal first-order formula,

\neg\neg\forall x C (x)

implies

\neg\neg C (y)

for arbitrary fresh

y

; use stability pointwise and generalize. Logical disjunction and existential translations are already double negations. This proves all cases.

Now regard classical first-order natural deduction as intuitionistic natural deduction plus unrestricted double-negation elimination, and induct on a classical derivation. The rules for logical conjunction, logical implication, universal quantification and logical falsity translate directly. Logical disjunction introduction gives

A^{N} \lor B^{N}

and then its double logical negation. For logical disjunction elimination, the translated premise is

\neg\neg (A^{N} \lor B^{N})

and the two translated branches yield the stable conclusion

C^{N}

. Assuming

\neg C^{N}

makes each branch contradictory, giving

\neg A^{N}

and

\neg B^{N}

, hence

\neg (A^{N} \lor B^{N})

, which contradicts the premise. We have

\neg\neg C^{N}

and remove it by stability.

Existential introduction likewise adds a double logical negation to the ordinary witness introduction. In existential elimination, the witness branch

A^{N} (y) ⊢ C^{N}

has the original fresh-variable condition. Assuming

\neg C^{N}

makes that branch give

\neg A^{N} (y)

; generalization gives

\forall y \neg A^{N} (y)

and therefore

\neg\exists y A^{N} (y)

, contradicting the translated premise. Again stability supplies

C^{N}

. The universal-rule side conditions are preserved because the translation introduces no new free variables.

For logical equality, reflexivity gives

t = t

and then its double logical negation. For substitution, from

\neg\neg (s = t)

and

A^{N} (s)

, temporarily assume

\neg A^{N} (t)

. An assumption

s = t

would transport

A^{N} (s)

A^{N} (t)

by intuitionistic logical equality substitution, so it gives a contradiction and hence

\neg (s = t)

. The first premise contradicts this. Thus

\neg\neg A^{N} (t)

holds and stability gives

A^{N} (t)

. Finally a classical double-negation elimination step translates precisely to

\neg\neg A^{N} \to A^{N}

, already proved. Every rule is therefore covered, giving negative translation of a classical proof:

Γ ⊢_{CL} φ ⟹ Γ^{N} ⊢_{IL} φ^{N} .

(3)

In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.

In classical logic, double-negation elimination gives

P^{N} \leftrightarrow P

on atoms. Structural induction propagates equivalence through logical conjunction, logical implication and both quantifiers, and removes the added double negations on logical disjunction and existence. Therefore

CL ⊢ φ^{N} \leftrightarrow φ, CL ⊢ φ ⟹ IL ⊢ φ^{N} .

(4)

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2017 / iii / Paper 135 / 6 / Solution Created 2026-10-03 Updated 2026-10-05

 View more

Use untyped lambda calculus and normal-order beta reduction. Write

c_{n} = λ f x . f^{n} x

for the Church numeral of

n

. We will construct a closed term

F

such that

F c_{n_{1}} \dots c_{n_{k}} ⟶_{β}^{*} c_{f (n)}

(1)

when

f (n)

is defined, and with no head normal form otherwise. The latter condition implies that the result is not in beta equivalence with any Church numeral, so both definedness and the output are represented.

First represent all total primitive recursive functions. The zero function is

λ x . c_{0}

, the successor function is

Succ = λn f x . f (n f x),

(2)

and the

i

th projection function is

λ x_{1} \dots x_{k} . x_{i}

. Function composition in recursion theory is represented by

λ x . G (H_{1} x) \dots (H_{r} x)

. This composition claim is used here for total functions, whose inner terms all reduce to numerals.

For primitive recursion use Church pairs and iteration. Put

T = λab . a, F = λab . b, Pair = λab p . p ab, Fst = λ p . p T, Snd = λ p . p F .

(3)

Suppose

G, H

represent the total constituents of

f (x, 0) = g (x)

and

f (x, n + 1) = h (x, n, f (x, n))

. Define

Step_{x} R = λ p . Pair (Succ (Fst p)) (H x (Fst p) (Snd p)), = λ x n . Snd (n Step_{x} (Pair c_{0} (G x))) .

(4)

After

j

iterations the pair reduces to

Pair c_{j} c_{f (x, j)}

, by mathematical induction on

j

. Its second projection is the required result. This lambda definition of primitive recursion by pair iteration and structural induction on the primitive recursive construction give terms for all primitive recursive functions.

For an arbitrary partial computable function use the Kleene normal form theorem with its program index fixed. There are total primitive recursive functions

C (x, s)

and

U (s)

such that

C

is zero exactly when

s

codes a valid halting computation history on

x

, and

U

extracts that history's output. Checking finite coded configurations and each transition is primitive recursive. Determinism ensures that every accepted history on an input has the same output. Hence

f (x) = U (μ s [C (x, s) = 0]) .

(5)

If the input computation never halts, no history is accepted. Let

C, U

be the total numeral-representing terms already obtained. The Church numeral zero test is

Zero = λn . n (λ z . F) T

, returning

T

exactly on zero. A Church Boolean applied to two arguments selects the appropriate branch without evaluating the other.

Take the fixed-point combinator

Y = λh . (λ z . h (zz)) (λ z . h (zz))

. For the input tuple define

G_{x} = λ rs . (Zero (C x s)) (U s) (r (Succ s)), F = λ x . (Y G_{x}) c_{0} .

(6)

Expanding the displayed abbreviations gives a genuine finite combinator. At a numeral code

c_{j}

, the total predicate computation terminates. If it returns a positive numeral, the false Church Boolean selects the next search code. If it returns zero, the true Church Boolean selects

U c_{j}

, which reduces to the output numeral. If the least accepted code is

s

, a finite sequence of these tests reaches it and then produces

c_{U (s)}

If there is no accepted code, every test is false and head reduction moves through codes

0, 1, 2, \dots

forever. At no finite point can a head variable or an outer numeral abstraction be produced: the applied search term must first unfold the fixed point and evaluate the next total test, and the decoder branch is always discarded. Thus it has no head normal form. The standard head-normalization property, or the Church-Rosser theorem together with normalization of normal-order reduction, rules out beta equivalence to a numeral. In particular, we have avoided a lazy-composition pitfall: an outer function that discards an argument need not force a divergent inner computation. The decoder is reached only after the guarded search succeeds. This proves lambda representation of partial computable functions:

f (n) ↓= m \Rightarrow F c_{n} \equiv_{β} c_{m}, f (n) ↑\Rightarrow F c_{n} has no head normal form.

(7)

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2018 / iii / Paper 135 / 1 / Solution Created 2026-10-03 Updated 2026-10-05

 View more

A proper filter on a set

I

contains

I

, excludes

\emptyset

, is upward closed, and is closed under finite intersections. Order its proper extensions by inclusion. The union of a nonempty chain is again a proper filter: finitely many members lie together in one chain member. Zorn lemma, and hence the axiom of choice, gives a maximal extension

U

. If neither

S

nor

I ∖ S

belongs to

U

, maximality of

U

says adjoining either one produces the improper filter. There are therefore

A, B \in U

with

A \cap S = \emptyset

and

B \cap (I ∖ S) = \emptyset

, contradicting

A \cap B \in U

. Thus

U

is an ultrafilter.

For Łoś theorem, interpret the ultraproduct using

a \sim b

when

{i : a_{i} = b_{i}} \in U

, with functions and relations interpreted coordinatewise. These interpretations are well defined because changing finitely many argument representatives changes them only outside the intersection of their agreement sets, which belongs to

U

. For any first-order formula and sequences of parameters,

i \prod M_{i} / U ⊨ ϕ ([a]) ⟺ S_{ϕ} (a) := {i : M_{i} ⊨ ϕ (a_{i})} \in U .

(1)

Prove this by structural induction. Atomic formulas follow from the interpretation of terms. Conjunction uses finite intersections; negation uses the ultrafilter dichotomy between a set and its complement. If

\exists y ψ

holds in the ultraproduct, a witness sequence gives a subset of

S_{\exists y ψ}

U

. Conversely, choose a witness

b_{i}

for

ψ

in every factor where one exists, and an arbitrary element in every other factor. This is the second explicit use of the axiom of choice; all factors have nonempty carriers. The inductive hypothesis applied to

ψ (a, b)

supplies the ultraproduct witness. The other connectives and universal quantification follow from these cases.

For the possible worlds, use free filters, equivalently proper filters extending the cofinite filter

F_{0}

. Here “nonprincipal” must have this free-filter meaning: merely saying that a filter has no single generating subset need not make

F_{0}

an accessible least world. The designated world is

F_{0}

, and all worlds have carrier

D = \prod_{i} M_{i}

. Atoms, including equality, are forced by

F ⊩ ϕ (a) ⟺ S_{ϕ} (a) \in F .

(2)

Equality may identify distinct sequences at a world; it is a persistent congruence, and at an ultrafilter world its quotient is the ordinary ultraproduct.

The required equivalence with all ultraproducts uses dense-extension filter semantics. Its recursive clauses are

F ⊩ ⊥ F ⊩ ϕ \land ψ F ⊩ \neg ϕ F ⊩ ϕ \to ψ F ⊩ ϕ \lor ψ F ⊩ \exists x ϕ (x) F ⊩ \forall x ϕ (x) never, ⟺ F ⊩ ϕ and F ⊩ ψ, ⟺ \forall G \supseteq F (G \neq ⊩ ϕ), ⟺ \forall G \supseteq F (G ⊩ ϕ \Rightarrow G ⊩ ψ), ⟺ \forall G \supseteq F \exists H \supseteq G (H ⊩ ϕ or H ⊩ ψ), ⟺ \exists a \in D (F ⊩ ϕ (a)), ⟺ \forall G \supseteq F \forall a \in D (G ⊩ ϕ (a)) .

(3)

Every extension in these clauses is a free proper filter. The dense clause for disjunction is essential; for propositional formulas, local disjunction would instead give a Kripke model for intuitionistic propositional logic and would invalidate the claimed equivalence.

The useful separation fact is membership in a free filter is detected by its ultrafilter extensions:

S \in F ⟺ \forall U \supseteq F (U a nonprincipal ultrafilter \Rightarrow S \in U) .

(4)

Indeed, if

S \in / F

, every

A \in F

has infinite intersection with

I ∖ S

: a finite intersection would imply

S \in F

after intersecting

A

with a suitable cofinite set. Hence adjoining

I ∖ S

generates a free proper filter, which extends to a nonprincipal ultrafilter by the ultrafilter lemma.

Induction on formulas now gives

F ⊩ ϕ (a) ⟺ S_{ϕ} (a) \in F

. Negation and implication follow by adjoining the positive set on which their classical truth conditions fail. For disjunction, membership of

S_{ϕ} \cup S_{ψ}

lets every extension be refined to an ultrafilter containing one of the two sets. If that union is absent from

F

, an ultrafilter extending

F

contains its complement and has no further proper extension, contradicting the dense clause. For existence, choose coordinate witnesses on

S_{\exists x ϕ}

as in Łoś theorem. For universality, if

S_{\forall x ϕ} \in / F

, choose a counterexample in every factor outside it and arbitrary elements elsewhere. The resulting sequence has

S_{ϕ} \subseteq S_{\forall x ϕ}

, so

F

cannot force that instance. The converse follows from upward closure and persistence.

At the designated world, therefore,

M_{I} ⊩ ϕ ⟺ S_{ϕ} is cofinite ⟺ \forall U nonprincipal i \prod M_{i} / U ⊨ ϕ .

(5)

This semantics validates classical first-order logic, including law of excluded middle. For example, every free filter has an ultrafilter refinement deciding an atomic formula, so its excluded middle is forced even when neither disjunct is forced at the original world. To see concretely why local disjunction fails, take

I = N

and an atom true exactly at even indices: neither its truth set nor its complement is cofinite, although every ultraproduct satisfies its excluded middle.

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2019 / ii / Paper 1 / 16I / Solution Created 2026-09-24 Updated 2026-09-29

 View more

The completeness theorem for propositional logic states that for every set of formulae

Γ

and formula

φ

Γ ⊨ φ ⟹ Γ ⊢ φ .

(1)

With the soundness theorem for propositional logic, this is an equivalence. It is also equivalent to saying that every consistent set of formulae has a model.

The usual countable proof lists all formulae and extends a consistent theory one formula at a time. For an uncountable set of primitive propositions, use the uncountable-language proof of propositional completeness: order the consistent extensions of

Γ

by inclusion. The union of every chain is consistent, since a proof of a contradiction would use only finitely many assumptions and hence would already lie in one member of the chain. Zorn lemma gives a maximal consistent set in propositional logic

M

. Define a Boolean valuation by

v (p) = 1

exactly when

p \in M

. The usual structural induction on formulae proves the truth lemma

v (θ) = 1 ⟺ θ \in M,

(2)

v

is a model of

Γ

The propositional compactness theorem says that a set

Γ

is satisfiable if and only if every finite subset of

Γ

is satisfiable. Only the forward implication is immediate. For the converse, if

Γ

had no model, then

Γ ⊨ ⊥

, so completeness would give

Γ ⊢ ⊥

. Every formal proof uses finitely many assumptions, so some finite

Γ_{0} \subseteq Γ

would prove

⊥

and, by soundness, would have no model, a contradiction.

The decidability theorem for propositional logic says that there is an algorithm deciding whether a propositional formula is a theorem. A formula contains only finitely many primitive propositions, even when the full language is uncountable. Its finite truth table decides whether it is valid, and completeness says that validity is equivalent to theoremhood.

Now let

(X, <)

be the given partially ordered set. For every distinct

x, y \in X

, introduce propositions

p_{x y}

and

q_{x y}

. Form a propositional theory

T

containing the following clauses:

$p_{x y} \leftrightarrow \neg p_{y x}$ and $q_{x y} \leftrightarrow \neg q_{y x}$ for distinct $x, y$ ;
$(p_{x y} \land p_{yz}) \to p_{x z}$ and $(q_{x y} \land q_{yz}) \to q_{x z}$ for pairwise distinct $x, y, z$ ;
$p_{x y}$ and $q_{x y}$ whenever $x < y$ in the original order;
$\neg (p_{x y} \land q_{x y})$ and $\neg (p_{y x} \land q_{y x})$ whenever $x$ and $y$ are incomparable in the original order.

The first two families say that

p

and

q

encode strict total orders. The third makes both orders extend

<

, while the fourth makes them disagree on every incomparable pair.

Every finite subset

T_{0} \subseteq T

mentions only a finite subset

F \subseteq X

. By hypothesis, the induced order on

F

is a two-dimensional poset, so choose two total orders realizing it and assign the finitely many

p

and

q

variables accordingly. This satisfies

T_{0}

. Thus every finite subset of

T

is satisfiable, and propositional compactness gives a model of all of

T

Define

x <_{1} y

when

p_{x y}

is true and

x <_{2} y

when

q_{x y}

is true. The clauses make

<_{1}

and

<_{2}

total orders on

X

. They both contain the original order, and their intersection contains no incomparable pair. Hence

x < y ⟺ x <_{1} y and x <_{2} y,

(3)

which proves the finite-local characterization of two-dimensional partially ordered sets.

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2021 / ii / Paper 1 / 12F / iii / Solution Created 2026-09-24 Updated 2026-09-25

 View more

Let

g (n, k) = r (n)

, where

r

is the total primitive-recursive parity function from part (ii), and apply unbounded minimization in

k

p (n) = μ k [g (n, k) = 0] .

(1)

n

is even, then

g (n, 0) = 0

and

p (n) = 0

. If

n

is odd, then

g (n, k) = 1

for every

k

, so the search never terminates and

p (n)

is undefined. Hence

p

is partial recursive. Because every function built without minimization is total,

p

cannot be defined without minimization; the functions

s

and

r

can.

It remains to characterize the functions built using only the initial functions and composition. They are exactly the functions

f (x_{1}, \dots, x_{k}) = c or f (x_{1}, \dots, x_{k}) = x_{i} + c

(2)

for some

c \in N

and some input coordinate

i

Indeed, the zero function is the first form, the successor function and each projection function have the second form, and composing functions of these forms preserves the classification: a constant outer function remains constant, while an outer function

y_{j} + c

selects one inner function and adds

c

. This proves necessity by structural induction. Conversely, applying the successor function

c

times to zero produces the constant

c

, and applying it

c

times to

π_{i}^{k}

produces

x_{i} + c

Every function in this class is directly computable: an algorithm either writes the fixed constant

c

, or copies the

i

th input and performs

c

successor steps.

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 124 / 5 / ii / Solution 2026-09-28

 View more

Proceed by structural induction on a Boolean formula

F

. A leaf computes

x_{i}

\neg x_{i}

, so its measure is

1

, equal to its leaf count. If the root is an AND gate with subformulae computing

g, h

, then

μ (g \land h) \leq μ (g) + μ (h)

(1)

by property 2; the induction hypothesis bounds this by the sum of the two subformula sizes, which is the size of

F

. Property 3 gives the identical argument for an OR gate. Consequently every formula computing

f

has size at least

μ (f)

, so

μ (f)

is a formula-size lower bound.

 Read the full article

Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2010 / B / 6 / b / Solution 2026-10-31

 View more

For a structure in a countable language and any subset

C

of its domain, there is an elementary substructure containing

C

of cardinality at most

max (∣ C ∣, ℵ_{0})

. In particular a finite or countable

C

lies in a countable elementary substructure. This is the downward Löwenheim-Skolem theorem.

Construct it directly inside the given structure

A

. Start with

C_{0}

containing

C

, the interpretations of the constants, and one element if needed to ensure a nonempty domain. Given

C_{n}

, for every formula

\exists x φ (x, a)

with its finite parameter tuple from

C_{n}

that is true in

A

, choose one actual witness in

A

and place it in

C_{n + 1}

. Retain

C_{n}

as well. There are at most

max (∣ C ∣, ℵ_{0})

choices at each stage. Let

B = ⋃_{n < ω} C_{n}

The construction closes

B

under every function of the language: for a tuple in

C_{n}

, the formula

x = f (a)

forces its unique value into the next stage. Thus

B

carries the induced substructure, and it has the asserted cardinal bound.

Prove elementarity by structural induction. Atomic formulas agree by the induced-substructure construction; logical connectives preserve agreement. For an existential formula with parameters in

B

, if it is true in

A

, all its parameters occur in some

C_{n}

, so the chosen witness lies in

C_{n + 1} \subseteq B

. The induction hypothesis makes its matrix true in

B

. In the other direction a witness in

B

is also a witness in

A

, again by induction. This is the Tarski-Vaught test, with its witness argument proved explicitly. No completeness or compactness theorem theorem enters the construction.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2003 / Calculus, probability, linear algebra, discrete mathematics, logic and proof, and models of computation / 10 / a / i / Solution 2026-10-31

 View more

A context-free grammar with start symbol

P

, terminal alphabet

{0, 1}

, and the following productions generates all binary palindromes:

P ⟶ ϵ ∣ 0 ∣ 1 ∣ 0 P 0 ∣ 1 P 1.

(1)

Each production preserves the palindrome property: it either supplies a central string of length zero or one, or wraps the same symbol around a shorter palindrome. This proves soundness by structural induction on the parse tree.

Conversely, any palindrome of length at least two has equal first and last symbols. Remove them to obtain a shorter palindrome, apply mathematical induction on length, and then use the corresponding wrapping production. The three base cases are

ϵ

0

, and

1

, proving completeness.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2003 / Functional programming, data structures and algorithms, procedural programming, and digital hardware / 1 / b / Solution 2026-10-31

 View more

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 gives

combine (map (z :) (x s : x s s^{'})) (ys : ys s^{'}) = ((z : x s) + + ys) : combine (map (z :) x s s^{'}) ys s^{'} = (z : (x s + + ys)) : map (z :) (combine x s s^{'} ys s^{'}) = map (z :) ((x s + + ys) : combine x s s^{'} ys s^{'}) = map (z :) (combine (x s : x s s^{'}) (ys : ys s^{'})) .

(1)

The 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. Hence

combine (map (z :) x ss) yss = map (z :) (combine x ss yss) .

(2)

 Read the full article

 View more

In 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 realizes

preorder (t) = t, preorder (t . l e f t), preorder (t . r i g h t) .

(1)

For

m

nodes, overhead is

Θ (m + 1)

and recursion depth is

O (h + 1)

for height

h

, 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.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 2 / a / Solution 2026-10-31

 View more

Use structural induction on the finite list xs, strengthening the induction hypothesis to hold for every accumulator value

y

. For the empty list, the defining equation of the left fold gives

x \oplus foldl (\otimes) y [] = x \oplus y = foldl (\otimes) (x \oplus y) [] .

(1)

For 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

y \otimes z

, and then use the supplied compatibility law:

x \oplus foldl (\otimes) y (z : zs) = x \oplus foldl (\otimes) (y \otimes z) zs = foldl (\otimes) (x \oplus (y \otimes z)) zs = foldl (\otimes) ((x \oplus y) \otimes z) zs = foldl (\otimes) (x \oplus y) (z : zs) .

(2)

Hence

x \oplus foldl (\otimes) y xs = foldl (\otimes) (x \oplus y) xs .

(3)

Only 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.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 2 / b / Solution 2026-10-31

 View more

Again use structural induction on the finite list. At [], both the right fold and the left fold return the seed

a

. If they agree on zs, then

foldr (\oplus) a (z : zs) = z \oplus foldr (\oplus) a zs = z \oplus foldl (\otimes) a zs = foldl (\otimes) (z \oplus a) zs = foldl (\otimes) (a \otimes z) zs = foldl (\otimes) a (z : zs) .

(1)

The third line uses part (a); the fourth uses equation (2). Thus the left-right fold equivalence is

foldr (\oplus) a xs = foldl (\otimes) a xs .

(2)

This is a statement about values on finite, total inputs. It does not assert equal evaluation costs or equal behaviour on infinite lists.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 4 / d / Solution 2026-10-31

 View more

Use the empty list for an empty subtree, and join the left result, the current label and the right result:

flatten :: STree a -> [a]
flatten = foldSTree (\left x right -> left ++ (x : right)) []

Thus

flatten (Node l x r) = flatten (l) + + [x] + + flatten (r)

. This is an inorder traversal. By structural induction, each subtree produces its labels in order; the binary search tree invariant places every left label below

x

and every right label above

x

, proving that the whole result is increasing. The definition works for any binary-tree shape, although its result is sorted only when the ordering invariant holds. Repeated list concatenation can give quadratic cost on a left chain; the question asks for a tree fold definition, rather than an optimal traversal implementation.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 4 / g / Solution 2026-10-31

 View more

Search as for insertion. Removing a node with at most one nonempty child leaves that child in its place. With two children, use the smallest key in the right subtree as the replacement and remove that occurrence from the right subtree:

delete :: Ord a => a -> STree a -> STree a
delete _ Empty = Empty
delete y (Node left x right) =
  case compare y x of
    LT -> Node (delete y left) x right
    GT -> Node left x (delete y right)
    EQ -> join left right
  where
    -- Join two search trees with every left key below every right key.
    join :: STree a -> STree a -> STree a
    join Empty r = r
    join l Empty = l
    join l r = let (smallest, rest) = takeMin r
               in Node l smallest rest

-- Precondition: the input tree is nonempty.
takeMin :: STree a -> (a, STree a)
takeMin Empty = error "takeMin: empty tree"
takeMin (Node Empty x right) = (x, right)
takeMin (Node left x right) =
  let (smallest, rest) = takeMin left
  in (smallest, Node rest x right)

The call to takeMin occurs only after both empty cases have been excluded. Its structural recursion follows left children until it reaches the minimum label and rebuilds the path with that occurrence removed.

For a matching label

x

and successor

s

, all left labels are below

x < s

, while every label remaining on the right is strictly above

s

. Thus replacing

x

s

preserves the binary search tree invariant. Every other branch preserves the invariant by structural induction. The resulting set is exactly

keys (delete y t) = keys (t) ∖ {y} .

(1)

Whether the key is absent or present, untouched subtrees can be shared. The search path followed by the successor path uses

O (h)

time and fresh nodes for original height of a binary tree

h

, so the worst case is

O (n)

without balancing. This is persistent binary search tree deletion: the original value remains available.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 1 / a / Solution 2026-10-31

 View more

The two constructors encode a natural number by its number of successors. Structural recursion replaces the zero constructor by zero and every successor by one addition:

convert :: Natural -> Integer
convert Zero     = 0
convert (Succ n) = 1 + convert n

Structural induction gives

convert (Succ^{n} Zero) = n

. The output uses unbounded integers, so there is no machine-word overflow.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 1 / b / Solution 2026-10-31

 View more

Recurse on the first argument for addition and multiplication, and on the exponent for exponentiation:

add :: Natural -> Natural -> Natural
add Zero     n = n
add (Succ m) n = Succ (add m n)

mul :: Natural -> Natural -> Natural
mul Zero     n = Zero
mul (Succ m) n = add n (mul m n)

power :: Natural -> Natural -> Natural
power m Zero     = Succ Zero
power m (Succ n) = mul m (power m n)

The defining arithmetic identities are

0 + n = n, (m + 1) + n = 1 + (m + n), 0 n = 0, (m + 1) n = n + mn, m^{0} = 1, m^{n + 1} = m m^{n} .

(1)

Each recursive call consumes one constructor. The base of exponentiation makes power Zero Zero equal to one, the empty-product convention. Applying convert and using structural induction verifies all three operations.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 1 / f / Solution 2026-10-31

 View more

Let

T (n) = (F_{n}, F_{n + 1})

. The equations derived in part (e) become

T (0) = (0, 1)

and

T (n + 1) = s (T (n))

, where

s (a, b) = (b, a + b)

. Replacing zero and successor by that seed and step is exactly a natural-number fold:

twoFibsNat :: Natural -> (Integer, Integer)
twoFibsNat = foldNat step (0, 1)
  where
    step :: (Integer, Integer) -> (Integer, Integer)
    step (a, b) = (b, a + b)

fibNat :: Natural -> Integer
fibNat = fst . twoFibsNat

Consequently

fibNat = fst \circ foldNat ((a, b) \mapsto (b, a + b)) (0, 1) .

(1)

Structural induction follows the constructors of Natural: the seed gives the first two Fibonacci numbers, and the successor step uses the Fibonacci recurrence. The extra component carries exactly the information needed for the next update.

 Read the full article