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

目標與範圍

設 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 是質數。

逐步主鏈

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

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

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

m(10)=121=11\cdot 11

m(10)=121=11\cdot 11

\neg P(10)

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

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

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

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

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

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

n\in V

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

0\le n\le 9

11\le m(n)\le 101

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

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

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

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

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

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

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

P(12)

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

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

F_U=\{10,11\}

\min F_U=10

10\in F_U,\ V\subseteq U

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

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

局部子步與引理

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=2,\ r\in\{0,1\}

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

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

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

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)

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)

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

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

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

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

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}

逐步反向審查

• 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、反控制與修訂記錄）