# 決定問題：在明示有限輸入集上證明試除程序是 decider

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-decision-problem/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-decision-problem-01 · production-20261019-adopted-96



## 目標與範圍

取輸入集合 X={0,1,2,3,4,5,6,7,8,9}、規格 P(x)：「x 是質數」與 yes-instance 集合 Y={x∈X ∣ P(x)}。在明示的 while 程式計算模型 W 中，證明試除程序 D1 對每個 x∈X 都終止，且 D1(x)=true 當且僅當 x∈Y，因此 D1 是 (X,Y) 的 decider；再說明只在 yes-instance 上停止的 D2 與只看奇偶的 D3 都不是 decider。

在 MKO 範圍內工作：固定的有限輸入集 X 與 Y⊆X（假設 a1），以及明示的計算模型與輸入表示（假設 a2）。結論只涵蓋這個 X；不由此推論整個自然數上的可計算性或不可判定性，不處理一般半決定程序理論，不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- set_builder
- divides_def
- order_basics
- numeric_evaluation
- prime_def
- while_semantics


- G1 — 輸入集合 X={0,1,2,3,4,5,6,7,8,9} 是明示列出的有限集合；規格 P(x) 為「x 是質數」；yes-instance 集合 Y={x∈X ∣ P(x)}，所以 Y⊆X（MKO 假設 a1）。
- G2 — 計算模型 W：以自然數變數為狀態的確定性 while 程式。輸入 x 以自然數值給出（例如二進位數字串）。基本操作為兩數比較、加 1、d≥1 時求餘數 x mod d、賦值與 return v，各算一步。若程式在有限步內執行到 return，就稱它在 x 上終止，輸出是 return 的值；永遠不執行 return 的執行不終止（MKO 假設 a2）。
- G3 — 候選程序。D1(x)：第 1 行 若 x<2 則 return false；第 2 行 d:=2；第 3 行 while d<x do（若 x mod d=0 則 return false；d:=d+1）；第 4 行 return true。D2(x)：照 D1 的程式文字執行；若 D1 會 return true 就 return true；若 D1 會 return false，改為執行 while true do skip（永不 return）。D3(x)：return（x mod 2=1）。


- X — 輸入集合 {0,1,2,3,4,5,6,7,8,9}
- P(x) — 規格：x 是質數
- Y — yes-instance 集合 {x∈X ∣ P(x)}
- W — 明示的 while 程式計算模型
- D_1,D_2,D_3 — 三個候選程序
- x \bmod d — x 除以 d 的餘數（d≥1）
- d\mid x — d 整除 x





## 規則與來源


- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_decision_problem_def · cited — 決定問題可表示為輸入集合 X 與 yes-instance 集合 Y⊆X，等價於命題規格 P:X→Prop。相對一個明示計算模型，decider D 必須對每個 x∈X 終止，且 D(x)=true 當且僅當 x∈Y。 · mko-decision-problem
- prime_def · prerequisite — 自然數 p 是質數，當且僅當 p≥2 且其正因數只有 1 與 p。因為 p≥1 的正因數 d 滿足 d≤p（p=dk 且 k≥1），這等價於：p≥2 且沒有整數 d 滿足 2≤d≤p−1 且 d∣p。對自然數 x 與 d≥1，d∣x 當且僅當 x mod d=0。
- while_semantics · prerequisite — W 的語義：敘述依序執行；if B then S 只在 B 為真時執行 S；while B do S 先測試 B，為真則執行 S 後再測試，為假則跳到迴圈之後；return v 以輸出 v 結束執行；while true do skip 永不結束。
- finite_exhaustion · prerequisite — 對明示列出的有限集合 D，∀x∈D, Q(x) 等價於 Q 對每個列出元素都成立的合取；逐一檢查全部元素即可證明它，只檢查部分元素則不行，而且結論只涵蓋 D。
- L_loop_term · lemma — 對每個自然數 x≥2，D1 在 x 上的 while 迴圈最多完成 x−2 輪，因此 D1 在 x 上終止。
- L_loop_inv · lemma — 對每個自然數 x≥2，D1 在 x 上每次測試 d<x 時，都有 2≤d≤x，且沒有整數 e 滿足 2≤e<d 且 e∣x。





## 逐步主鏈

S01 · definition操作前

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

操作後

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

條件：X=\{0,1,2,3,4,5,6,7,8,9\}

規則：set_builder · 依賴：G1

葉節點依據：set_builder + def_intro

把問題寫成一對 (X,Y)：Y 由規格 P 以集合建構式定義，x∈Y 表示 x∈X 且 P(x)。Y 是正確答案的描述，與任何候選程序無關；D1、D2、D3 只是之後要拿來和 Y 比對的實作（MKO 第一段：規格與實作分開）。



S02 · implies操作前

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

操作後

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

條件：X\ \text{finite and listed}

規則：prime_def · 依賴：S01, G1

葉節點依據：prime_def + divides_def + numeric_evaluation + finite_exhaustion

對 X 的十個元素逐一判定 P(x)。X 是明示有限集合，所以逐一檢查全部元素就得到 Y 的完整列表；判定細節在 S02.1 到 S02.3。結果 Y={2,3,5,7}。



S03 · equivalent操作前

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)

條件：W\ \text{fixed (G2)}

規則：def_unfold · 依賴：G2, mko_decision_problem_def

葉節點依據：def_unfold + mko_decision_problem_def

展開 MKO 的 decider 定義，得到兩個條款：(T) 對每個 x∈X 都終止；(C) 終止時輸出 true 恰好對應 x∈Y。兩個條款都量化在整個 X 上，而且都相對於固定的模型 W。之後分別為 D1 證明 (T) 與 (C)。



S04 · implies操作前

x\in\{0,1\}

操作後

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

條件：x<2

規則：while_semantics · 依賴：G3, S02.1

葉節點依據：while_semantics + prime_def

x=0 或 x=1 時，第 1 行的測試 x<2 為真，D1 立刻 return false，在有限步內終止。由 S02.1，這兩個輸入確實不在 Y，所以輸出與規格一致。



S05 · theorem_application操作前

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

規則：L_loop_term · 依賴：G3, G1

葉節點依據：while_semantics + nat_induction + order_basics

套用引理 L_loop_term：x≥2 時迴圈最多完成 x−2 輪，之後測試 d<x 失敗，執行第 4 行 return true，或在某輪中提早 return false。X 中最大的 x 是 9，所以最多 7 輪。與 S04 合起來，D1 對每個 x∈X 都終止，條款 (T) 成立。



S06 · theorem_application操作前

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)

條件：x\ge 2

規則：L_loop_inv · 依賴：G3

葉節點依據：nat_induction + divides_def + while_semantics

套用迴圈不變量 L_loop_inv：每次測試 d<x 時，d 在 2 與 x 之間，且 2 到 d−1 之間沒有 x 的因數。不變量把「迴圈已經檢查過什麼」寫成一個命題，讓 S07、S08 能由程式的出口推出 x 是否為質數。



S07 · implies操作前

D_1(x)=\mathrm{true}

操作後

x\in Y

條件：無

規則：prime_def · 依賴：S04, S06, G3

葉節點依據：prime_def + order_basics + while_semantics

D1 只在第 4 行輸出 true，而且由 S04，x<2 時不會到達第 4 行，所以 x≥2。到達第 4 行表示測試 d<x 失敗；不變量給 d≤x，依三分律得 d=x。不變量再給出：沒有 e 滿足 2≤e<x 且 e∣x，即 2 到 x−1 之間沒有因數。依 prime_def，x 是質數，x∈Y。



S08 · implies操作前

D_1(x)=\mathrm{false}

操作後

x\notin Y

條件：無

規則：case_analysis · 依賴：S04, S06, G3

葉節點依據：case_analysis + prime_def + divides_def + while_semantics

D1 只在兩處輸出 false。情況一：第 1 行，x<2，不是質數（S04）。情況二：迴圈中某次 x mod d=0；此時測試 d<x 剛通過，且不變量給 d≥2，所以 d 是滿足 2≤d≤x−1 的因數，x 不是質數。兩種情況涵蓋所有 return false 的位置，所以 x∉Y。



S09 · implies操作前

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

條件：D_1\ \text{terminates on}\ x

規則：iff_intro · 依賴：S04, S05, S07, S08

葉節點依據：iff_intro + contrapositive + forall_intro

取任意 x∈X。由 S04、S05，D1 在 x 上終止，輸出 true 或 false 其中之一。(⇒) 是 S07。(⇐) 若 x∈Y，輸出不可能是 false，否則由 S08 得 x∉Y，矛盾；所以輸出是 true。兩向合成 ⇔；x 是任意的，依全稱推廣對所有 x∈X 成立，條款 (C) 成立。



S10 · implies操作前

(\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

條件：無

規則：and_intro_elim · 依賴：S03, S04, S05, S09

葉節點依據：and_intro_elim + def_unfold + case_analysis

條款 (T) 由 S04（x<2）與 S05（x≥2）合成，這兩種情況涵蓋 X 的每個元素；條款 (C) 是 S09。合取後依 S03 的等價折回定義：D1 是 (X,Y) 在 W 中的 decider。



S11 · implies操作前

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\ \text{finite and listed}

規則：finite_exhaustion · 依賴：S02, S10, G3

葉節點依據：finite_exhaustion + numeric_evaluation + while_semantics

交叉核對：手動執行 D1 於全部十個輸入。例如 x=9：d=2 時 9 mod 2=1，d=3 時 9 mod 3=0，return false；x=7：d=2 到 6 的餘數 1、1、3、2、1，之後 d=7 測試失敗，return true。完整表格與 Y={2,3,5,7} 的成員表逐項相同。因為 X 有限且已全部列出，這張表本身也是條款 (C) 在 X 上的完整核對；但它只涵蓋 X（MKO 假設 a2）。



S12 · implies操作前

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})

條件：無

規則：quantifier_negation · 依賴：S03, S02.2, G3

葉節點依據：quantifier_negation + while_semantics + divides_def

在 x=4 上，D1 的程式文字於 d=2 時得到 4 mod 2=0，會 return false；D2 此時改為執行 while true do skip，永不 return。所以存在 x∈X 使 D2 不終止，依量詞否定，條款 (T) 不成立，D2 不是 decider。D2 恰好在 Y 上以 true 停止，是 Y 的半決定程序；這正是 MKO 指出的誤解：只保證在 yes-instance 上接受，尚不足以保證總 decider；D2 真正違反的是對 no-instance 的終止性，而 D1 也只接受 yes-instance，卻會在其餘輸入拒絕並終止。



S13 · implies操作前

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)

條件：無

規則：quantifier_negation · 依賴：S03, S02, G3

葉節點依據：quantifier_negation + numeric_evaluation

D3 在有限步內終止，所以 (T) 成立；但 9 mod 2=1，D3(9)=true，而 9∉Y（S02.2）；另外 D3(2)=false 而 2∈Y。存在反例，條款 (C) 不成立，D3 不是 decider。值得注意：在樣本 {3,4,5,6,7,8} 上 D3 與 Y 完全一致，所以抽樣一致不足以證明整個論域（MKO 第二段）。







## 局部子步與引理

S02.1 · implies操作前

x\in\{0,1\}

操作後

0\notin Y,\ 1\notin Y

條件：x<2

規則：prime_def · 依賴：S01

葉節點依據：prime_def + order_basics

質數必須 ≥2；0 與 1 都小於 2，所以 P(0)、P(1) 為假，0、1 不在 Y。



S02.2 · implies操作前

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

條件：2\le d\le x-1

規則：divides_def · 依賴：S01

葉節點依據：divides_def + prime_def + numeric_evaluation

依整除定義，2∣4、2∣6、2∣8、3∣9，而且 2 與 3 都滿足 2≤d≤x−1。依 prime_def 的等價形式，這四個數不是質數，不在 Y。



S02.3 · implies操作前

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

操作後

2,3,5,7\in Y

條件：x\ge 2; x\bmod d\ne 0\ \text{for}\ 2\le d\le x-1

規則：prime_def · 依賴：S01

葉節點依據：prime_def + divides_def + numeric_evaluation

x=2 時 2≤d≤1 的範圍是空的；3 mod 2=1；5 除以 2、3、4 的餘數為 1、2、1；7 除以 2、3、4、5、6 的餘數為 1、1、3、2、1。這些數都 ≥2 且在 2 到 x−1 之間沒有因數，依 prime_def 都是質數。



S05.1 · implies操作前

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

操作後

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

條件：無

規則：while_semantics · 依賴：G3, while_semantics

葉節點依據：while_semantics

第 2 行令 d=2。迴圈本體只有兩種結果：若 x mod d=0 則 return false，執行結束；否則執行 d:=d+1。本體中沒有其他改變 d 的敘述。



S05.2 · induction_step操作前

\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}

條件：x\ge 2

規則：nat_induction · 依賴：S05.1

葉節點依據：nat_induction + order_basics + while_semantics

對 k 歸納：k=0 時 d=2；若完成 k 輪後 d=2+k，再完成一輪就是 d=2+(k+1)（S05.1）。第 k 輪開始前要先通過測試 d<x，即 2+k<x，也就是 k≤x−3，所以可能的輪次只有 k=0 到 x−3，共 x−2 輪。最後一輪完成後 d=x，測試失敗，第 4 行 return。因此執行在有限步內結束，引理 L_loop_term 得證。



S06.1 · induction_base操作前

\text{first test},\ d=2

操作後

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

條件：x\ge 2

規則：nat_induction · 依賴：G3, while_semantics

葉節點依據：nat_induction + order_basics

第一次測試時 d=2。因為 x≥2，有 2≤d≤x；滿足 2≤e<2 的整數 e 不存在，所以「沒有這樣的 e 整除 x」空真成立。不變量在初始時成立。



S06.2 · induction_step操作前

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)

條件：d<x; x\bmod d\ne 0

規則：nat_induction · 依賴：S06.1, divides_def, while_semantics

葉節點依據：nat_induction + divides_def + order_basics + while_semantics

設某次測試時不變量成立，測試 d<x 為真，且本輪沒有 return，也就是 x mod d≠0，故 d∤x。本輪後 d′=d+1。由 d<x 得 d′≤x，且 d′≥3≥2。滿足 2≤e<d′ 的 e 要嘛 e<d（依假設不整除 x），要嘛 e=d（剛驗證不整除 x）。所以下一次測試時不變量仍成立。S06.1 與 S06.2 合起來證得 L_loop_inv。







## 逐步反向審查


- S13 · premise_audit · S02, quantifier_negation, numeric_evaluation — 一個反例就否定全稱的 (C)（N8、N9 可重算）。反過來，樣本一致不能證明 (C)，所以此處只用反例方向。
- S12 · premise_audit · S03, quantifier_negation, G3 — 一個不終止的輸入就足以否定全稱條款 (T)。這裡不需要也不宣稱 D2 在其他 no-instance 上的行為，雖然它在 0、1、6、8、9 上同樣不終止。
- S11 · premise_audit · S02, finite_exhaustion, numeric_evaluation — 表格必須包含 X 的每個元素才算完整核對；若只列一部分就只是抽樣。這張表不能外推到 X 之外的輸入。
- S10 · sufficient_goal_reduction · S03, S05, S09, and_intro_elim — 目標 G：D1 是 decider。足夠條件 H：(T)∧(C)，H⇔G 由 S03。H 由 S04 到 S09 從程式文字與定義正向證成，沒有把 G 當前提。
- S09 · premise_audit · S05, S07, S08, iff_intro, contrapositive, forall_intro — 本步為 D1 的一般論證使用已證終止性：只有在輸出確為 true 或 false 時，「不可能 false」才推出 true。D2 在每個 yes-instance 上確實回傳 true，沒有違反這個反向蘊含；它在 no-instance 上發散，違反的是獨立的全域終止條款 (T)（S12）。
- S08 · premise_audit · S04, S06, case_analysis, prime_def, divides_def — 分情況必須涵蓋程式中每個 return false，這由程式文字確認只有兩處。不宣稱反向；反向在 S09 處理。
- S07 · premise_audit · S04, S06, prime_def, order_basics — 需要不變量的兩部分（d≤x 與沒有小因數）以及第 4 行只能由迴圈出口到達。此步只證「輸出 true ⇒ x∈Y」，反向在 S09 另行處理。
- S06.2 · premise_audit · S06.1, divides_def, while_semantics, order_basics — 保持性需要本輪沒有 return 這個條件；若本輪 return，執行已結束，不再有下一次測試，所以不需要保持。對自然數 d<x 推 d+1≤x 用的是整數的次序。
- S06.1 · premise_audit · G3, while_semantics, order_basics — 需要 x≥2 與第 2 行的賦值；這是歸納的基底。
- S06 · premise_audit · L_loop_inv, G3 — 需要 x≥2（否則第 1 行已 return，迴圈不執行）；引理在 S06.1、S06.2 以初始成立與逐步保持證明，不是只在幾個樣本狀態檢查。
- S05.2 · premise_audit · S05.1, nat_induction, order_basics — 需要 S05.1 的「每輪加 1」與自然數歸納。上界 x−2 只是上界，不宣稱每個輸入都會跑滿；例如 x=9 在 d=3 就 return false。
- S05.1 · premise_audit · G3, while_semantics — 直接讀程式文字與語義；不宣稱每輪一定會 return，只說 d 的變化只有加 1 這一種。
- S05 · premise_audit · L_loop_term, G3 — 需要引理的前提 x≥2；引理在 S05.1、S05.2 證明。終止性來自 d 每輪加 1 且有上界，不是來自「試跑幾個輸入都停了」。
- S04 · premise_audit · G3, while_semantics, S02.1 — 需要程式文字與 if 的語義，以及 S02.1 的判定。這只處理 x<2 的情況；x≥2 的情況由 S05 到 S08 處理。
- S03 · inverse_equivalence · mko_decision_problem_def, def_unfold — 展開與折回定義互為反向，所以兩邊等價。只滿足其中一個條款（例如只在 yes-instance 上終止）不是 decider。
- S02.3 · premise_audit · prime_def, numeric_evaluation — 要證明「沒有」因數，必須檢查 2 到 x−1 的每一個 d，不能只試 2（N3、N4 是對這幾個 d 的完整有限核對）。
- S02.2 · premise_audit · divides_def, prime_def — 每個數只需一個在 2 到 x−1 之間的因數見證（N1、N2 可重算）。見證必須在這個範圍內：d=1 或 d=x 永遠整除 x，不能當見證。
- S02.1 · premise_audit · prime_def — 只用到定義中的條件 p≥2。不宣稱反向：x≥2 不足以推出 x 是質數。
- S02 · premise_audit · S01, prime_def, finite_exhaustion — 需要質數的定義與 X 的完整列表。結論是兩個集合相等，靠的是十個元素都被檢查過；若漏掉任一元素就不能寫等號。
- S01 · premise_audit · G1, set_builder, mko_decision_problem_def — 此步只命名，不推出新事實。Y⊆X 直接來自集合建構式只收 X 的元素；不能反過來用某個程序的輸出來定義 Y。





## 錯誤控制與反例

半決定程序不一定是 deciderMKO 指出的常見誤解是把只接受 yes-instance 的程序當成總 decider。D2 在每個 x∈Y 上都以 true 停止，看起來「答對了所有 yes」，但在 x=4 上永不停止，因此違反條款 (T)。decider 必須在每個輸入上都終止並給出答案；S09 的 (⇐) 方向正是靠終止性才成立。

抽樣一致與有限表格的界限D3 在 {3,4,5,6,7,8} 上與 Y 完全一致，卻在 2 與 9 上出錯：抽樣一致不足以證明整個論域。另一方面，S11 的完整表格只因為 X 有限且全部列出才算證明，而且只涵蓋 X；不能由這張表推論整個自然數上的質數判定（MKO 假設 a2 與第三段）。

規格先於實作Y 由規格 P 定義（S01、S02），不能用「D1 輸出 true 的輸入」來定義 Y，否則任何程序都會自動「正確」。正確性永遠是程序與獨立規格之間的比較。


- D2 對每個 x∈Y 都輸出 true，所以 D2 決定 (X,Y) → reject — D2 在 x=4 上永不終止，違反「對每個 x∈X 終止」的條款；它只是半決定程序。
- D3 在 3、4、5、6、7、8 上都與 Y 一致，所以 D3 是 X 上的 decider → reject — D3(9)=true 但 9=3·3∉Y；D3(2)=false 但 2∈Y。
- D1 的表格在 X={0,1,2,3,4,5,6,7,8,9} 上與 Y 一致，所以這張表證明了整個自然數上的質數判定 → reject — 有限表格只證明該有限 X（MKO 假設 a2）；對整個自然數的宣稱是新的宣稱，需要對所有輸入的論證與固定的表示。
- D1 不是 (X,Y) 的 decider，因為它沒有處理輸入 −3 → reject — −3∉X；域外輸入不參與目前問題（MKO 第二段），decider 只需在 X 上終止並正確。





## 結論與限制

在模型 W 中，Y={2,3,5,7}，試除程序 D1 對每個 x∈X 終止且 D1(x)=true ⇔ x∈Y，所以 D1 是 (X,Y) 的 decider。D2 只在 yes-instance 上停止，是半決定程序而不是 decider；D3 總是終止但在 9 與 2 上答錯，也不是 decider。結論只涵蓋 X={0,1,2,3,4,5,6,7,8,9}。


- S05 到 S09 的論證除了輪數上界外沒有用到 x≤9；若要宣稱 D1 決定整個自然數上的質數性，需另外固定所有自然數在 W 中的表示並把該宣稱獨立陳述與審查，本稿不作此宣稱。
- 模型 W 以文字描述；與 Turing machine 等正式模型之間的語義橋（MKO formal next）未在此建立。





## 驗證及來源綁定

9 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-decision-problem-01.json)