# 反例與論域資格：n²+n+11 的質數性、失敗集合與最小反例

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

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

derivation-mko-counterexample-01 · production-20261019-adopted-96



## 目標與範圍

設 U={n∈ℤ ∣ 0≤n≤12}、V={n∈ℤ ∣ 0≤n≤9}、m(n)=n²+n+11、P(n)：「m(n) 是質數」。判定 φ_U：∀n∈U P(n)；求失敗集合 F_U 與最小反例；判定候選值 −11 的資格；並判定 φ_V：∀n∈V P(n)。

在 MKO 的範圍內工作：明示有限整數論域與可判定述詞。示範反例的兩個條件（在論域中、述詞失敗）、受限後的資格變化、完整失敗集合與最小反例，以及以對每個元素都有效的論證證明有限全稱。不對 ℕ 或 ℤ 上的 n²+n+11 作任何全稱宣稱；「每個整數 a≥2 有質因數」作為前提；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- divides_def
- division_algorithm
- order_basics
- numeric_evaluation
- prime_def


- G1 — U={n∈ℤ ∣ 0≤n≤12}，V={n∈ℤ ∣ 0≤n≤9}；兩者都是明示的有限整數論域，且 V⊆U。
- G2 — m(n)=n²+n+11；P(n)：「m(n) 是質數」，對每個整數都可精確判定。φ_U：∀n∈U P(n)；φ_V：∀n∈V P(n)。
- G3 — 待判定資格的候選值：c=−11（對 φ_U），以及 c=10（對 φ_V）。


- U,\ V — 論域：0≤n≤12 與 0≤n≤9 的整數
- m(n) — n²+n+11
- P(n) — 述詞「m(n) 是質數」
- F_U,\ F_V — 失敗集合 {n∈U ∣ ¬P(n)} 與 {n∈V ∣ ¬P(n)}
- p\mid m,\ p\nmid m — p 整除 m；p 不整除 m





## 規則與來源


- divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
- division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
- 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 — 明確整數或有理數算式的精確求值；可以獨立重算。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- mko_counterexample_def · cited — 對全稱陳述 ∀x∈U P(x)，c 是有效反例當且僅當 c∈U 且 P(c) 為假。一個有效反例即可否定該全稱陳述；沒有找到反例本身不是證明，除非論域有限且已完整驗證所有元素。 · mko-counterexample
- mko_quantifier_neg · cited — 在明示論域與古典真值語義下，¬∀x∈U P(x) 等價於 ∃x∈U ¬P(x)，¬∃x∈U P(x) 等價於 ∀x∈U ¬P(x)。 · mko-quantifier
- prime_def · prerequisite — 整數 m≥2 是質數，指它的正因數只有 1 與 m；m≥2 不是質數（合數）當且僅當存在整數 a 使 1<a<m 且 a∣m。
- prime_divisor_exists · prerequisite — 每個整數 a≥2 都有質因數 p（p∣a），且正整數 a 的正因數不超過 a。（可由良序原理得到：a 的最小大於 1 的因數是質數；本稿當作前提。）
- rem_divides · prerequisite — 對整數 a 與正整數 b，b∣a 當且僅當帶餘除法 a=bq+r（0≤r<b）的餘數 r=0（由帶餘除法的唯一性）。
- divides_combo · prerequisite — 若 p∣u 且 p∣v，則 p∣u+v 且 p∣u−v；若 p∣a 且 a∣m，則 p∣m。
- L_residue · lemma — 對整數 p≥1 與整數 n，寫 n=pq+r（0≤r<p），則 m(n)=p(pq²+2qr+q)+m(r)；因此 p∣m(n) ⇔ p∣m(r)。
- L_no_small_factor · lemma — 對每個整數 n，2、3、5、7 都不整除 m(n)=n²+n+11。
- L_trial · lemma — 若整數 m≥2，且沒有滿足 p²≤m 的質數 p 整除 m，則 m 是質數。





## 逐步主鏈

S01 · definition操作前

c\ \text{is a valid counterexample to}\ \forall n\in U\,P(n)

操作後

c\in U\ \land\ \neg P(c)

條件：無

規則：mko_counterexample_def · 依賴：G1, G2, mko_counterexample_def

葉節點依據：mko_counterexample_def

依 MKO，c 是 φ_U 的有效反例，當且僅當兩件事都成立：c 在論域 U 中，而且 P(c) 為假。檢查順序是先查論域資格，再查述詞是否失敗。



S02 · equivalent操作前

m(10)=10^2+10+11

操作後

m(10)=121=11\cdot 11

條件：無

規則：numeric_evaluation · 依賴：G2

葉節點依據：numeric_evaluation

精確計算：10²+10+11=100+10+11=121，而 11·11=121。



S03 · implies操作前

m(10)=121=11\cdot 11

操作後

\neg P(10)

條件：1<11<121; 11\mid 121

規則：prime_def · 依賴：S02, prime_def

葉節點依據：prime_def + divides_def + numeric_evaluation

121≥2，且 a=11 滿足 1<11<121 與 11∣121（121=11·11）。依質數定義，121 是合數，所以 P(10) 為假。完全平方數 121 也是合數，沒有例外。



S04 · implies操作前

0\le 10\le 12,\ \neg P(10)

操作後

10\in U\land\neg P(10)

條件：無

規則：mko_counterexample_def · 依賴：S01, S03, G1

葉節點依據：set_builder + mko_counterexample_def + and_intro_elim

先查資格：10 是整數，且 0≤10≤12，依集合建構式 10∈U。再查失敗：S03 給出 ¬P(10)。兩個條件都成立，所以 10 是 φ_U 的有效反例。



S05 · implies操作前

10\in U\land\neg P(10)

操作後

\neg\forall n\in U\,P(n)

條件：無

規則：mko_quantifier_neg · 依賴：S04, exists_intro, mko_quantifier_neg

葉節點依據：exists_intro + mko_quantifier_neg

由 ∃引入得 ∃n∈U ¬P(n)；依受限量詞的否定律（mko-quantifier），這等價於 ¬∀n∈U P(n)。一個有效反例就足以否定全稱陳述 φ_U，不需要先知道全部失敗值。



S06 · implies操作前

c=-11:\ m(-11)=121

操作後

-11\notin U,\ \text{so}\ -11\ \text{is not a counterexample to}\ \varphi_U

條件：無

規則：mko_counterexample_def · 依賴：S01, G1, G2, G3

葉節點依據：set_builder + mko_counterexample_def + order_basics

公式在域外也能計算：(−11)²+(−11)+11=121−11+11=121，是合數。但資格先於失敗：−11<0，不滿足 0≤n≤12，所以 −11∉U。依 S01 的定義，−11 不是 φ_U 的反例；它的失敗值與 φ_U 無關。



S07 · theorem_application操作前

n\in V

操作後

2\nmid m(n),\ 3\nmid m(n),\ 5\nmid m(n),\ 7\nmid m(n)

條件：n\in\mathbb{Z}

規則：L_no_small_factor · 依賴：G2, L_no_small_factor

葉節點依據：division_algorithm + rem_divides + divides_combo + case_analysis

要判定 φ_V，不能靠「搜尋沒找到」，必須對 V 的每個元素給出理由。第一個工具是引理 L_no_small_factor：對每個整數 n，2、3、5、7 都不整除 m(n)。V 的元素都是整數，所以引理適用。引理在子步 S07.1 到 S07.5 證明。



S08 · implies操作前

0\le n\le 9

操作後

11\le m(n)\le 101

條件：n\ge 0

規則：order_basics · 依賴：G1, G2, order_basics

葉節點依據：order_basics + square_nonneg + numeric_evaluation

對 0≤n≤9：n≥0 給出 n²≥0 與 n²+n≥0，所以 m(n)≥11；由 n≤9 且 n≥0 得 n²=n·n≤9·n≤81，所以 m(n)≤81+9+11=101。



S09 · theorem_application操作前

11\le m(n)\le 101,\quad 2,3,5,7\nmid m(n)

操作後

P(n)\ \text{for an arbitrary}\ n\in V

條件：m(n)\ge 2

規則：L_trial · 依賴：S07, S08, L_trial

葉節點依據：prime_def + order_basics + numeric_evaluation

取任意 n∈V。若質數 p 滿足 p²≤m(n)≤101，則 p≤10（因為 11²=121>101），所以 p∈{2,3,5,7}；S07 說這四個都不整除 m(n)。又 m(n)≥11≥2（S08）。依引理 L_trial，m(n) 是質數，即 P(n)。



S10 · implies操作前

P(n)\ \text{for an arbitrary}\ n\in V

操作後

\forall n\in V\,P(n)

條件：無

規則：forall_intro · 依賴：S09, forall_intro

葉節點依據：forall_intro

S07 到 S09 對任意 n∈V 證明了 P(n)，除 0≤n≤9 之外沒有對 n 加任何假設。依 ∀引入，φ_V 為真。這是對有限論域 V 每個元素都有效的論證，不是「搜尋沒有找到反例」；N11 以 isprime 對 n=0 到 9 逐一重算，作為獨立的完整核對。



S11 · implies操作前

m(11)=11^2+11+11

操作後

m(11)=143=11\cdot 13,\ 11\in U,\ \neg P(11)

條件：1<11<143

規則：prime_def · 依賴：G1, G2, prime_def

葉節點依據：prime_def + set_builder + numeric_evaluation

11²+11+11=121+22=143=11·13，而 1<11<143，所以 143 是合數；0≤11≤12，所以 11∈U。11 是 φ_U 的第二個有效反例。



S12 · theorem_application操作前

m(12)=12^2+12+11=167

操作後

P(12)

條件：167\ge 2

規則：L_trial · 依賴：L_no_small_factor, L_trial, G2

葉節點依據：rem_divides + numeric_evaluation + order_basics

m(12)=144+12+11=167。滿足 p²≤167 的質數是 p≤12 的 2、3、5、7、11（13²=169>167）。依 L_no_small_factor，2、3、5、7 不整除 167；又 167=11·15+2，餘數 2≠0，所以 11∤167。依引理 L_trial，167 是質數，P(12) 成立。



S13 · implies操作前

U=V\cup\{10,11,12\}

操作後

F_U=\{n\in U\mid\neg P(n)\}=\{10,11\}

條件：無

規則：set_extensionality · 依賴：S03, S10, S11, S12, G1

葉節點依據：set_extensionality + case_analysis + set_builder

U 的元素是 0 到 12 的整數，分成 V（0 到 9）與 10、11、12 三個元素，這涵蓋全部情況。P 在 V 上都成立（S10），在 12 成立（S12），在 10 與 11 失敗（S03、S11）。所以失敗集合恰為 {10,11}：兩個方向的包含都由逐一情況核對得到。這是有限論域的完整驗證。



S14 · implies操作前

F_U=\{10,11\}

操作後

\min F_U=10

條件：F_U\neq\varnothing

規則：order_basics · 依賴：S13

葉節點依據：order_basics + numeric_evaluation

依 MKO 假設 a2，最小反例是有限失敗集合的數值最小值。F_U={10,11} 非空，且 10<11，所以最小反例是 10。這個值由完整的 F_U 算出，不是由抽樣中第一個遇到的失敗值猜出。



S15 · implies操作前

10\in F_U,\ V\subseteq U

操作後

10\notin V,\ F_V=F_U\cap V=\varnothing

條件：無

規則：set_operations_def · 依賴：S10, S13, G1, G3

葉節點依據：set_operations_def + set_builder

限制到 V：10>9，所以 10∉V，它對 φ_V 失去反例資格；11 也一樣。V 的失敗集合 F_V={n∈V ∣ ¬P(n)}=F_U∩V=∅，所以 φ_V 沒有反例，最小反例明示為「不存在」。注意 φ_V 為真是由 S10 的論證得到，不是因為 10 失去資格；失去見證本身不證明任何全稱陳述。



S16 · implies操作前

\text{S05, S06, S10, S13, S14, S15}

操作後

\neg\varphi_U,\ F_U=\{10,11\},\ \min F_U=10,\ -11\ \text{ineligible},\ \varphi_V\ \text{true}

條件：無

規則：and_intro_elim · 依賴：S05, S06, S10, S13, S14, S15

葉節點依據：and_intro_elim

彙整：φ_U 為假（S05，有效反例 10）；F_U={10,11}，最小反例 10（S13、S14）；−11 雖使公式失敗卻不在 U 中，不是反例（S06）；φ_V 為真（S10），F_V=∅，沒有最小反例（S15）。







## 局部子步與引理

S07.1 · implies操作前

n=pq+r,\ 0\le r<p

操作後

m(n)=p(pq^2+2qr+q)+m(r),\quad p\mid m(n)\Leftrightarrow p\mid m(r)

條件：p\ge 1

規則：distributive · 依賴：division_algorithm, distributive, divides_combo

葉節點依據：division_algorithm + distributive + add_assoc + mul_comm + divides_combo

依帶餘除法寫 n=pq+r（0≤r<p）。展開：(pq+r)²+(pq+r)+11=p²q²+2pqr+r²+pq+r+11=p(pq²+2qr+q)+(r²+r+11)=p(pq²+2qr+q)+m(r)（N4 對這個多項式恆等式做格點核對）。因為 p 整除 p(pq²+2qr+q)，依整除的和差性質：若 p∣m(n)，相減得 p∣m(r)；若 p∣m(r)，相加得 p∣m(n)。這證得輔助引理 L_residue。



S07.2 · implies操作前

p=2,\ r\in\{0,1\}

操作後

m(0)=11=2\cdot 5+1,\ m(1)=13=2\cdot 6+1;\ 2\nmid m(n)

條件：無

規則：L_residue · 依賴：L_residue, rem_divides, case_analysis

葉節點依據：rem_divides + case_analysis + numeric_evaluation + division_algorithm

p=2：餘數 r 只能是 0 或 1。m(0)=11=2·5+1，m(1)=13=2·6+1，餘數都是 1≠0，所以 2∤m(0)、2∤m(1)。依 L_residue，對每個整數 n 都有 2∤m(n)。



S07.3 · implies操作前

p=3,\ r\in\{0,1,2\}

操作後

m(r)\in\{11,13,17\},\ \text{remainders}\ 2,1,2;\ 3\nmid m(n)

條件：無

規則：L_residue · 依賴：L_residue, rem_divides, case_analysis

葉節點依據：rem_divides + case_analysis + numeric_evaluation + division_algorithm

p=3：r=0、1、2 時 m(r)=11、13、17；11=3·3+2、13=3·4+1、17=3·5+2，餘數 2、1、2 都不是 0，所以 3 不整除這三個值。依 L_residue，對每個整數 n 都有 3∤m(n)。



S07.4 · implies操作前

p=5,\ r\in\{0,1,2,3,4\}

操作後

m(r)\in\{11,13,17,23,31\},\ \text{remainders}\ 1,3,2,3,1;\ 5\nmid m(n)

條件：無

規則：L_residue · 依賴：L_residue, rem_divides, case_analysis

葉節點依據：rem_divides + case_analysis + numeric_evaluation + division_algorithm

p=5：r=0 到 4 時 m(r)=11、13、17、23、31，除以 5 的餘數依序是 1、3、2、3、1，都不是 0。依 L_residue，對每個整數 n 都有 5∤m(n)。



S07.5 · implies操作前

p=7,\ r\in\{0,1,2,3,4,5,6\}

操作後

m(r)\in\{11,13,17,23,31,41,53\},\ \text{remainders}\ 4,6,3,2,3,6,4;\ 7\nmid m(n)

條件：無

規則：L_residue · 依賴：L_residue, rem_divides, case_analysis

葉節點依據：rem_divides + case_analysis + numeric_evaluation + division_algorithm

p=7：r=0 到 6 時 m(r)=11、13、17、23、31、41、53，除以 7 的餘數依序是 4、6、3、2、3、6、4，都不是 0。依 L_residue，對每個整數 n 都有 7∤m(n)。S07.2 到 S07.5 合起來證得引理 L_no_small_factor。



S09.1 · implies操作前

m\ge 2,\ m\ \text{not prime}

操作後

m=ab,\ 2\le a\le b,\ a^2\le m

條件：a>0

規則：prime_def · 依賴：prime_def, order_basics

葉節點依據：prime_def + divides_def + order_basics

設 m≥2 不是質數。依定義有整數 a，1<a<m 且 a∣m；令 b=m/a，則 b 是整數，且由 a<m 得 b>1、由 a>1 得 b<m。若 a>b 就交換兩者，所以可設 2≤a≤b。兩邊乘正數 a 得 a²≤ab=m。



S09.2 · implies操作前

m=ab,\ 2\le a,\ a^2\le m

操作後

\exists\ \text{prime}\ p:\ p\mid m\land p^2\le m

條件：無

規則：prime_divisor_exists · 依賴：S09.1, prime_divisor_exists, divides_combo

葉節點依據：prime_divisor_exists + divides_combo + order_basics

a≥2，所以 a 有質因數 p，且 p≤a。由 p∣a 與 a∣m 得 p∣m；由 0<p≤a 得 p²≤a²≤m。所以：若 m≥2 不是質數，就有質數 p 滿足 p²≤m 且 p∣m。



S09.3 · equivalent操作前

m\ \text{not prime}\Rightarrow\exists\ \text{prime}\ p:\ p\mid m\land p^2\le m

操作後

(\forall\ \text{prime}\ p:\ p^2\le m\Rightarrow p\nmid m)\Rightarrow m\ \text{prime}

條件：m\ge 2

規則：contrapositive · 依賴：S09.2, contrapositive

葉節點依據：contrapositive + quantifier_negation

取 S09.2 的逆否命題：若沒有滿足 p²≤m 的質數整除 m（且 m≥2），則 m 是質數。否定「存在這樣的 p」用量詞否定律得到「每個 p²≤m 的質數都不整除 m」。S09.1 到 S09.3 證得引理 L_trial。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S05, S06, S10, S13, S14, S15, and_intro_elim — 目標 G：四項判定。足夠條件 H：S05、S06、S10、S13、S14、S15 的結論；H⇒G 只是合取。H 的每一部分都由前面正向證成，沒有把 G 當作前提。
- S15 · premise_audit · S10, S13, set_operations_def — F_V=∅ 需要 S10（V 中沒有失敗值）；只靠 10∉V 推不出 F_V=∅。
- S14 · premise_audit · S13, order_basics — 需要 F_U 已完整確定（S13）；否則無法排除更小的失敗值。
- S13 · premise_audit · S03, S10, S11, S12, set_extensionality, case_analysis — 情況劃分必須涵蓋 U 的全部 13 個元素；只要漏掉一個，F_U 就沒有完整確定。
- S12 · premise_audit · L_no_small_factor, L_trial, rem_divides — 需要列全 p≤12 的質數；11 不在 L_no_small_factor 的範圍內，所以另以餘數判定（N15、N16）。
- S11 · premise_audit · prime_def, set_builder, numeric_evaluation — 兩個條件都已核對（N12、N13）。
- S10 · premise_audit · S09, forall_intro — 需要 n 是 V 的任意元素；若證明偷用了特定 n 的性質，就不能推廣。
- S09.3 · inverse_equivalence · contrapositive, quantifier_negation — 命題與其逆否命題等價，兩向成立；否定存在量詞的量詞否定律也是等價。
- S09.2 · premise_audit · prime_divisor_exists, divides_combo, order_basics — 質因數的存在是本稿的前提（可由良序原理證明），不在此重證。
- S09.1 · premise_audit · prime_def, divides_def, order_basics — 需要 a>0 才能保持不等式方向；b 的範圍由 m=ab 與 1<a<m 推出。
- S09 · premise_audit · S07, S08, L_trial — 需要列全 p²≤101 的質數：10 以下的質數 2、3、5、7（N10 核對 11²>101）；漏掉任何一個都會使論證不完整。
- S08 · premise_audit · order_basics, square_nonneg — 乘以非負數保持不等式方向，這需要 n≥0；上界 101 可重算（N9）。不宣稱反向。
- S07.5 · premise_audit · L_residue, rem_divides, case_analysis — 七種餘數涵蓋所有整數；七個餘數都已計算（N8）。普遍結論來自「有限個餘數情況涵蓋全部整數」這個論證，不是來自對 n 的抽樣。
- S07.4 · premise_audit · L_residue, rem_divides, case_analysis — 五種餘數涵蓋所有整數；五個餘數都已計算（N7）。
- S07.3 · premise_audit · L_residue, rem_divides, case_analysis — 三種餘數涵蓋所有整數；三個餘數都已計算（N6）。
- S07.2 · premise_audit · L_residue, rem_divides, case_analysis — 兩種餘數涵蓋所有整數（帶餘除法）；每種情況的餘數都已精確計算（N5）。
- S07.1 · premise_audit · division_algorithm, distributive, divides_combo — 需要帶餘除法的分解與展開恆等式；得到的 ⇔ 兩個方向分別由相減與相加給出理由。
- S07 · premise_audit · L_no_small_factor — 只需 n 是整數；引理不說 m(n) 是質數，只排除四個小質因數。
- S06 · premise_audit · set_builder, mko_counterexample_def, numeric_evaluation — 判定只需第一個條件失敗（N3 只重算公式值）；不宣稱 φ_U 因此為真，φ_U 已由 S05 判為假。
- S05 · premise_audit · exists_intro, mko_quantifier_neg — 需要見證在 U 中；否定全稱只需一個見證。不宣稱反向。
- S04 · premise_audit · set_builder, S03, mko_counterexample_def — 兩個條件必須同時成立；只有 ¬P(10) 而沒有 10∈U 不夠。
- S03 · premise_audit · prime_def, divides_def — 只需要一個真因數 11；不宣稱反向。
- S02 · inverse_equivalence · numeric_evaluation — 兩邊是同一個整數，可獨立重算（N1、N2）。
- S01 · premise_audit · mko_counterexample_def, G1, G2 — 此步只寫出定義，不推出新事實；兩個條件缺一不可。





## 錯誤控制與反例

先查論域資格MKO 指出的誤解之一是以域外值反駁受限全稱。−11 代入公式得 121，是合數，但 −11∉U，所以不是 φ_U 的反例（S06）。判定順序永遠是先查 c∈U，再查 P(c) 是否失敗。

沒找到反例不是證明MKO 的另一個誤解是把一段搜尋沒找到反例當成普遍證明。逐一試 n=0 到 9 都得到質數，但 n=10 就失敗；若只搜尋到 9 就宣稱「對所有 n 成立」是錯的。φ_V 的證明是 S07 到 S10 對 V 的每個元素都有效的論證；對無限論域，任何有限搜尋都不構成證明。

失去見證不等於新全稱成立MKO 第二段：限制到子集後，原反例可能離開子集而失去資格，但這不表示新全稱為真。例如 W={11,12}⊆U：10∉W 失去資格，可是 11∈W 仍使 P 失敗，所以 ∀n∈W P(n) 仍為假。φ_V 為真是因為 S10 的證明，不是因為 10∉V。


- m(−11)=121 是合數，所以 −11 是 ∀n∈U P(n) 的反例 → reject — −11<0，所以 −11∉U；域外的失敗值不是反例。
- n=0 到 9 都使 n²+n+11 為質數，所以對所有自然數 n 都成立 → reject — n=10 時 n²+n+11=121=11·11，不是質數。
- 10∉V，所以 ∀n∈V P(n) 已得證 → reject — 失去一個見證不證明全稱；W={11,12} 時 10 也不在 W 中，但 ∀n∈W P(n) 仍因 11 而為假。φ_V 需要 S07 到 S10 的論證。
- φ_V 的最小反例是 10 → reject — 10∉V；F_V=∅，所以 φ_V 沒有反例，最小反例不存在。





## 結論與限制

φ_U（∀n∈U, n²+n+11 是質數，U 為 0 到 12）為假：失敗集合 F_U={10,11}（121=11·11、143=11·13），最小反例是 10。候選值 −11 雖然給出 121，但 −11∉U，不是反例。φ_V（V 為 0 到 9）為真：對每個 n∈V，11≤m(n)≤101，且 2、3、5、7 都不整除 m(n)，所以 m(n) 是質數；F_V=∅，沒有最小反例。


- N5 到 N8 是對每個 p 的全部餘數 r 的有限檢查；普遍結論 L_no_small_factor 依賴 S07.1 的 L_residue 與「餘數情況涵蓋全部整數」，不是只靠這些檢查。
- 「每個整數 a≥2 有質因數」在本稿是前提，未在此證明。N11、N17 以 isprime 做獨立重算，論證不依賴它們。





## 驗證及來源綁定

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


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

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