Decision problem: proving that a trial-division procedure is a decider on an explicit finite input set

Goal and scope

Take the input set X={0,1,2,3,4,5,6,7,8,9}, the specification P(x): 'x is prime', and the yes-instance set Y={x∈X ∣ P(x)}. In the explicit while-program model W, prove that the trial-division procedure D1 terminates on every x∈X and that D1(x)=true exactly when x∈Y, so D1 is a decider for (X,Y); then show that D2, which halts only on yes-instances, and D3, which tests only parity, are not deciders.

Works inside the MKO's scope: a fixed finite input set X with Y⊆X (assumption a1) and an explicit computational model and input representation (assumption a2). The conclusion covers this X only; it draws no conclusion about computability or undecidability over all natural numbers, does not treat the general theory of semi-decision procedures, and does not change the canonical MKO or its English edition.

Givens and symbols

• set_builder
• divides_def
• order_basics
• numeric_evaluation
• prime_def
• while_semantics

• G1 — The input set X={0,1,2,3,4,5,6,7,8,9} is an explicitly listed finite set; the specification P(x) is 'x is prime'; the yes-instance set is Y={x∈X ∣ P(x)}, so Y⊆X (MKO assumption a1).
• G2 — Computational model W: deterministic while-programs whose states are values of natural-number variables. The input x is given as a natural-number value (for example its binary numeral). The basic operations are comparing two numbers, adding 1, the remainder x mod d for d≥1, assignment and 'return v', each counted as one step. A program terminates on x if it executes a return after finitely many steps, and its output is the returned value; a run that never executes return does not terminate (MKO assumption a2).
• G3 — Candidate procedures. D1(x): line 1, if x<2 then return false; line 2, d:=2; line 3, while d<x do (if x mod d=0 then return false; d:=d+1); line 4, return true. D2(x): run the text of D1; if D1 would return true, return true; if D1 would return false, instead execute 'while true do skip' (never returns). D3(x): return (x mod 2=1).

• X — the input set {0,1,2,3,4,5,6,7,8,9}
• P(x) — the specification: x is prime
• Y — the yes-instance set {x∈X ∣ P(x)}
• W — the explicit while-program computational model
• D_1,D_2,D_3 — the three candidate procedures
• x \bmod d — the remainder of x on division by d (d≥1)
• d\mid x — d divides x

Rules and sources

• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_decision_problem_def · cited — A decision problem is an input set X with a yes-instance set Y⊆X, equivalently a proposition-valued specification P:X→Prop. Relative to an explicit computational model, a decider D must terminate on every x∈X and satisfy D(x)=true exactly when x∈Y. · mko-decision-problem
• prime_def · prerequisite — A natural number p is prime exactly when p≥2 and its only positive divisors are 1 and p. Since a positive divisor d of p≥1 satisfies d≤p (p=dk with k≥1), this is equivalent to: p≥2 and no integer d with 2≤d≤p−1 divides p. For natural x and d≥1, d∣x exactly when x mod d=0.
• while_semantics · prerequisite — Semantics of W: statements run in order; 'if B then S' runs S only when B is true; 'while B do S' tests B, runs S and tests again when B is true, and continues after the loop when B is false; 'return v' ends the run with output v; 'while true do skip' never ends.
• finite_exhaustion · prerequisite — For an explicitly listed finite set D, ∀x∈D, Q(x) is equivalent to the conjunction of Q(d) over the listed elements d; checking every element proves it, checking only some does not, and the conclusion covers D only.
• L_loop_term · lemma — For every natural number x≥2, the while loop of D1 on x completes at most x−2 passes, so D1 terminates on x.
• L_loop_inv · lemma — For every natural number x≥2, whenever D1 on x tests d<x, we have 2≤d≤x and no integer e with 2≤e<d divides x.

Main derivation

P(x):\ x\ \text{is prime},\quad x\in X

Y=\{x\in X\mid P(x)\}

Y=\{x\in X\mid P(x)\}

Y=\{2,3,5,7\}

D\ \text{decides}\ (X,Y)\ \text{in}\ W

(\forall x\in X,\ D\ \text{terminates on}\ x)\ \wedge\ (\forall x\in X,\ D(x)=\mathrm{true}\iff x\in Y)

x\in\{0,1\}

D_1\ \text{terminates on}\ x,\ D_1(x)=\mathrm{false},\ x\notin Y

x\in X,\ x\ge 2

D_1\ \text{terminates on}\ x\ \text{after at most}\ x-2\le 7\ \text{loop passes}

x\ge 2

\text{at every test of}\ d<x:\ 2\le d\le x\ \wedge\ \neg\exists e\,(2\le e<d\ \wedge\ e\mid x)

D_1(x)=\mathrm{true}

x\in Y

D_1(x)=\mathrm{false}

x\notin Y

D_1(x)=\mathrm{true}\Rightarrow x\in Y,\quad D_1(x)=\mathrm{false}\Rightarrow x\notin Y

\forall x\in X,\ D_1(x)=\mathrm{true}\iff x\in Y

(\forall x\in X,\ D_1\ \text{terminates})\ \wedge\ (\forall x\in X,\ D_1(x)=\mathrm{true}\iff x\in Y)

D_1\ \text{decides}\ (X,Y)\ \text{in}\ W

x=0,1,2,3,4,5,6,7,8,9

D_1(x)=\mathrm{F},\mathrm{F},\mathrm{T},\mathrm{T},\mathrm{F},\mathrm{T},\mathrm{F},\mathrm{T},\mathrm{F},\mathrm{F}\ =\ [x\in Y]

x=4\in X:\ D_1\ \text{would return false}

D_2\ \text{does not terminate on}\ 4\ \Rightarrow\ \neg(\forall x\in X,\ D_2\ \text{terminates})

D_3(x)=[x\bmod 2=1]

D_3(9)=\mathrm{true},\ 9\notin Y\ \Rightarrow\ \neg(\forall x\in X,\ D_3(x)=\mathrm{true}\iff x\in Y)

Substeps and lemmas

x\in\{0,1\}

0\notin Y,\ 1\notin Y

x\in\{4,6,8,9\}

4=2\cdot 2,\ 6=2\cdot 3,\ 8=2\cdot 4,\ 9=3\cdot 3\ \Rightarrow\ 4,6,8,9\notin Y

x\in\{2,3,5,7\}

2,3,5,7\in Y

d=2\ \text{at the first test}

\text{each pass either returns or replaces}\ d\ \text{by}\ d+1

\text{after}\ k\ \text{completed passes without return:}\ d=2+k

\text{a pass starts only if}\ 2+k<x,\ \text{so at most}\ x-2\ \text{passes complete}

\text{first test},\ d=2

2\le 2\le x\ \wedge\ \{e:2\le e<2\}=\varnothing

2\le d\le x,\ \neg\exists e\,(2\le e<d\wedge e\mid x),\ d<x,\ x\bmod d\ne 0

d'=d+1:\ 2\le d'\le x\ \wedge\ \neg\exists e\,(2\le e<d'\wedge e\mid x)

Reverse audits

• S13 · premise_audit · S02, quantifier_negation, numeric_evaluation — One counterexample refutes the universal clause (C) (recomputable as N8, N9). Conversely, agreement on a sample cannot prove (C), so only the counterexample direction is used.
• S12 · premise_audit · S03, quantifier_negation, G3 — One non-terminating input suffices to refute the universal clause (T). Nothing else about D2 is needed, although it also fails to terminate on 0, 1, 6, 8 and 9.
• S11 · premise_audit · S02, finite_exhaustion, numeric_evaluation — The table counts as a complete check only because it contains every element of X; a partial table would be a sample. It cannot be extrapolated to inputs outside X.
• S10 · sufficient_goal_reduction · S03, S05, S09, and_intro_elim — Goal G: D1 is a decider. Sufficient condition H: (T)∧(C), with H⇔G by S03. H is proved forwards in S04 to S09 from the program text and the definitions; G is never used as a premise.
• S09 · premise_audit · S05, S07, S08, iff_intro, contrapositive, forall_intro — The generic argument for D1 uses its proved termination: only when the result is known to be true or false does 'not false' imply true. D2 does return true on every yes-instance and does not violate that reverse implication; it diverges on no-instances and fails the separate total-termination clause (T) in S12.
• S08 · premise_audit · S04, S06, case_analysis, prime_def, divides_def — The case split must cover every 'return false' in the program, and the program text confirms there are only two. No converse is claimed here; it is handled in S09.
• S07 · premise_audit · S04, S06, prime_def, order_basics — It needs both parts of the invariant (d≤x and no small divisor) and that line 4 is reachable only through the loop exit. This step proves only 'output true ⇒ x∈Y'; the converse is handled separately in S09.
• S06.2 · premise_audit · S06.1, divides_def, while_semantics, order_basics — Preservation needs the condition that the pass did not return; if it did, the run has ended and there is no next test to preserve the invariant for. Passing from d<x to d+1≤x uses the order of the integers.
• S06.1 · premise_audit · G3, while_semantics, order_basics — It needs x≥2 and the assignment on line 2; this is the base of the induction.
• S06 · premise_audit · L_loop_inv, G3 — It needs x≥2 (otherwise line 1 has already returned and the loop never runs); the lemma is proved in S06.1 and S06.2 by establishment and preservation, not by checking a few sample states.
• S05.2 · premise_audit · S05.1, nat_induction, order_basics — It needs 'add 1 per pass' from S05.1 and natural induction. The bound x−2 is only an upper bound; it is not claimed that every input uses all passes; for example x=9 returns false at d=3.
• S05.1 · premise_audit · G3, while_semantics — Read directly from the program text and the semantics; it does not claim every pass returns, only that the sole change to d is adding 1.
• S05 · premise_audit · L_loop_term, G3 — It needs the lemma's hypothesis x≥2; the lemma is proved in S05.1 and S05.2. Termination comes from d increasing by 1 per pass with an upper bound, not from having tried a few inputs that happened to stop.
• S04 · premise_audit · G3, while_semantics, S02.1 — It needs the program text, the semantics of 'if', and the decision in S02.1. It handles only x<2; the case x≥2 is handled in S05 to S08.
• S03 · inverse_equivalence · mko_decision_problem_def, def_unfold — Unfolding and folding a definition are inverse moves, so the two sides are equivalent. Satisfying only one clause (for example halting only on yes-instances) does not make a decider.
• S02.3 · premise_audit · prime_def, numeric_evaluation — To show there is no divisor, every d from 2 to x−1 must be checked, not only d=2 (N3 and N4 are the complete finite checks over exactly these d).
• S02.2 · premise_audit · divides_def, prime_def — Each number needs only one divisor witness between 2 and x−1 (recomputable as N1, N2). The witness must lie in that range: d=1 and d=x always divide x and do not count.
• S02.1 · premise_audit · prime_def — Only the clause p≥2 of the definition is used. No converse is claimed: x≥2 alone does not make x prime.
• S02 · premise_audit · S01, prime_def, finite_exhaustion — It needs the definition of prime and the complete list of X. The conclusion is an equality of sets, and it rests on all ten elements having been checked; leaving out any element would not justify the equality.
• S01 · premise_audit · G1, set_builder, mko_decision_problem_def — This step only names and derives no new fact. Y⊆X holds because set-builder notation only collects elements of X; Y may not be defined backwards from the outputs of some program.

Error controls and negative controls

A semidecision procedure need not be a decider

The misconception identified in the MKO is treating a procedure that accepts only yes-instances as a total decider. D2 halts with true on every x∈Y and seems to 'get every yes right', but it never halts on x=4, violating clause (T). A decider must terminate with an answer on every input; the (⇐) direction of S09 holds only because of termination.

The limits of sampling and of finite tables

D3 agrees with Y on {3,4,5,6,7,8} but is wrong on 2 and 9: agreement on a sample does not prove the whole domain. On the other hand, the complete table in S11 counts as a proof only because X is finite and fully listed, and it covers X only; it does not establish primality testing on all natural numbers (MKO assumption a2 and paragraph 3).

The specification comes before the implementation

Y is defined by the specification P (S01, S02); it must not be defined as 'the inputs on which D1 outputs true', or every program would be 'correct' automatically. Correctness is always a comparison between a program and an independent specification.

• D2 outputs true on every x∈Y, so D2 decides (X,Y) → reject — D2 never terminates on x=4, violating the clause 'terminates on every x∈X'; it is only a semi-decision procedure.
• D3 agrees with Y on 3, 4, 5, 6, 7 and 8, so D3 is a decider on X → reject — D3(9)=true but 9=3·3∉Y; D3(2)=false but 2∈Y.
• D1's table agrees with Y on X={0,1,2,3,4,5,6,7,8,9}, so the table proves primality testing on all natural numbers → reject — A finite table establishes only that finite X (MKO assumption a2); a claim over all natural numbers is a new claim needing an argument for every input and a fixed representation.
• D1 is not a decider for (X,Y) because it does not handle the input −3 → reject — −3∉X; inputs outside the domain are not part of the problem (MKO paragraph 2), and a decider only has to terminate correctly on X.

Result and limitations

In the model W, Y={2,3,5,7}, and the trial-division procedure D1 terminates on every x∈X with D1(x)=true ⇔ x∈Y, so D1 is a decider for (X,Y). D2 halts only on yes-instances and is a semi-decision procedure, not a decider; D3 always terminates but answers wrongly on 9 and 2, so it is not a decider either. The conclusion covers X={0,1,2,3,4,5,6,7,8,9} only.

• The argument in S05 to S09 uses x≤9 only for the pass bound; claiming that D1 decides primality on all natural numbers would require fixing the representation of every natural number in W and stating and reviewing that claim separately, which this guide does not do.
• The model W is described in prose; the semantic bridge to a formal model such as Turing machines (MKO formal next) is not built here.

Verification and source binding

9 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 8c1298a85a7e15de57c25d5f9f4225a8395a15a17de10382e9374e299407f3f6
• original source SHA-256: 50e70577152ab8bc0e89748c30ba626dddea3df36bb2c9b31d40e16c3abd912b
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)