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

目標與範圍

取輸入集合 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。

逐步主鏈

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)

局部子步與引理

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)

逐步反向審查

• 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。

錯誤控制與反例

半決定程序不一定是 decider

MKO 指出的常見誤解是把只接受 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、反控制與修訂記錄）