量詞與明示論域：在有限整數論域上判定全稱、存在及其否定

目標與範圍

在明示有限論域 U={−2,−1,0,1,2,3} 上，判定 φ₁：∀x∈U, x²<10；φ₂：∀x∈U, x²>x；φ₃：∃x∈U, x²=2 的真假；正確寫出 φ₂ 與 φ₃ 的否定；並說明論域為空集合時全稱與存在陳述的真假。

在 MKO 的範圍內工作：明示有限整數論域、可判定述詞（大小與相等比較）、古典真值語義。用完整枚舉判定有限論域上的陳述，並由無限制的量詞否定律證明受限量詞的否定律。枚舉的結論只針對指定的有限論域，不外推到 ℤ、ℝ 或無限論域；不宣稱一階邏輯的完備性已形式證明；不改動 canonical MKO 或英文 edition。

已知條件與符號

• forall_elim
• forall_intro
• exists_intro
• quantifier_negation
• numeric_evaluation
• restricted_quantifier

• G1 — 論域 U={−2,−1,0,1,2,3} 以列舉方式明示，是有限整數集合；採古典真值語義（MKO 假設 a1、a2）。
• G2 — 述詞：P(x) 為 x²<10，Q(x) 為 x²>x，E(x) 為 x²=2；每一個都能以精確整數計算判定。
• G3 — 待判定：φ₁=∀x∈U P(x)、φ₂=∀x∈U Q(x)、φ₃=∃x∈U E(x)；另判定以空集合 ∅ 為論域時的 ∀x∈∅ R(x) 與 ∃x∈∅ R(x)。

• U — 明示有限整數論域 {−2,−1,0,1,2,3}
• P(x),\ Q(x),\ E(x) — 述詞 x²<10、x²>x、x²=2
• R(x) — 引理中的任意述詞
• a_i — U 的第 i 個列出元素
• \varphi_1,\ \varphi_2,\ \varphi_3 — 三個待判定的量詞陳述

規則與來源

• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• 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。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
• mko_quantifier_def · cited — 在明示論域 U 與述詞 P 下，∀x∈U P(x) 表示每個 U 中元素滿足 P，∃x∈U P(x) 表示至少一個 U 中元素滿足 P。採古典真值語義，¬∀x∈U P(x) 等價於 ∃x∈U ¬P(x)，¬∃x∈U P(x) 等價於 ∀x∈U ¬P(x)。 · mko-quantifier
• restricted_quantifier · prerequisite — 受限量詞的意義：∀x∈U R(x) 表示 ∀x(x∈U⇒R(x))；∃x∈U R(x) 表示 ∃x(x∈U∧R(x))。
• roster_membership · prerequisite — 列舉集合的成員關係：對以列舉給出的有限集合 U={a_i ∣ 1≤i≤n}，x∈U 當且僅當存在 i（1≤i≤n）使 x=a_i。
• classical_implication · prerequisite — 古典蘊涵：(A⇒B) ⇔ (¬A∨B)；因此 ¬(A⇒B) ⇔ (A∧¬B)，且前件 A 為假時 A⇒B 為真。
• empty_set_def · prerequisite — 空集合：對每個 x，x∉∅。
• L_finite_forall · lemma — 對以列舉給出的有限集合 U={a_i ∣ 1≤i≤n} 與任意述詞 R：∀x∈U R(x) ⇔ ⋀_{i=1}^{n} R(a_i)。
• L_restricted_negation · lemma — 古典語義下，對任意論域 U 與述詞 R：(i) ¬∀x∈U R(x) ⇔ ∃x∈U ¬R(x)；(ii) ¬∃x∈U R(x) ⇔ ∀x∈U ¬R(x)。

逐步主鏈

\forall x\in U\,P(x),\quad \exists x\in U\,E(x)

\forall x\,(x\in U\Rightarrow P(x)),\quad \exists x\,(x\in U\land E(x))

(-2)^2,\ (-1)^2,\ 0^2,\ 1^2,\ 2^2,\ 3^2

4,\ 1,\ 0,\ 1,\ 4,\ 9

x^2\in\{4,1,0,1,4,9\}\ \text{for the six}\ x\in U

P(-2)\land P(-1)\land P(0)\land P(1)\land P(2)\land P(3)

P(-2)\land P(-1)\land P(0)\land P(1)\land P(2)\land P(3)

\forall x\in U\,P(x)

\forall x\in U\,P(x)\ \text{is true}

\neg\forall x\in\mathbb{Z}\,P(x)

Q(0):\ 0^2>0

0\in U\land\neg Q(0)

0\in U\land\neg Q(0)

\exists x\in U\,\neg Q(x)

\exists x\in U\,\neg Q(x)

\neg\forall x\in U\,Q(x)

\forall x\in U\,\neg Q(x)

\neg\forall x\in U\,\neg Q(x)\quad(\text{since } 2\in U,\ 2^2>2)

x^2\in\{4,1,0,1,4,9\}\ \text{for the six}\ x\in U

\neg E(-2)\land\neg E(-1)\land\neg E(0)\land\neg E(1)\land\neg E(2)\land\neg E(3)

\neg E(-2)\land\neg E(-1)\land\neg E(0)\land\neg E(1)\land\neg E(2)\land\neg E(3)

\forall x\in U\,\neg E(x)

\forall x\in U\,\neg E(x)

\neg\exists x\in U\,E(x)

\neg\exists x\in U\,E(x)

\exists x\in\mathbb{R}\,E(x)

\forall x\in\varnothing\,R(x)

\forall x\,(x\in\varnothing\Rightarrow R(x))\ \text{holds}

\exists x\in\varnothing\,R(x)

\neg\exists x\,(x\in\varnothing\land R(x))

\text{S04, S08, S12, S14, S15}

\varphi_1\ \text{true},\ \varphi_2\ \text{false},\ \varphi_3\ \text{false};\ \forall x\in\varnothing\ \text{true},\ \exists x\in\varnothing\ \text{false}

局部子步與引理

\forall x\in U\,R(x)

\bigwedge_{i=1}^{n}R(a_i)

\bigwedge_{i=1}^{n}R(a_i)

\forall x\in U\,R(x)

\neg\forall x\in U\,R(x)

\exists x\,\neg(x\in U\Rightarrow R(x))

\exists x\,\neg(x\in U\Rightarrow R(x))

\exists x\,(x\in U\land\neg R(x))=\exists x\in U\,\neg R(x)

\neg\exists x\in U\,R(x)

\forall x\in U\,\neg R(x)

逐步反向審查

• S16 · sufficient_goal_reduction · S04, S08, S12, S14, S15, and_intro_elim — 目標 G：判定 φ₁、φ₂、φ₃，寫出正確否定，並處理空論域邊界。足夠條件 H：S04、S08、S12、S14、S15 五個結論。H⇒G 只是合取；H 的每一部分都由前面的步驟正向證成，沒有把 G 當作前提。
• S15 · premise_audit · empty_set_def, and_intro_elim, forall_intro, quantifier_negation — 需要對每個 x 證合取為假（任意 x 後用 ∀引入），再用量詞否定律。
• S14 · premise_audit · empty_set_def, classical_implication, forall_intro — 需要「∅ 沒有元素」與古典蘊涵的真值；這不表示 R 對任何東西成立。
• S13 · premise_audit · sqrt_def, exists_intro — 需要 √2 的存在（主平方根定義）；此步不改變 φ₃ 在 U 上的結論。
• S12 · inverse_equivalence · L_restricted_negation — 第 (ii) 部分在 S08.3 證明，雙向成立。
• S11 · inverse_equivalence · L_finite_forall — 同 S04，引理兩個方向都已證。
• S10 · premise_audit · S02, numeric_evaluation, and_intro_elim — U 的六個元素都必須檢查；漏掉任何一個，S11 就不能進行。
• S09 · premise_audit · forall_elim, contradiction, numeric_evaluation — 需要 2∈U 與精確比較 4>2（N6）。此步只判定錯誤寫法為假，不影響 S08 的結論。
• S08.3 · inverse_equivalence · quantifier_negation, de_morgan_logic, classical_implication, logic_chain — 鏈中每一環都是等價，依推論的傳遞，整條鏈雙向成立。
• S08.2 · inverse_equivalence · classical_implication, de_morgan_logic — 每個 x 處的替換都是等價，所以在存在量詞之下也雙向成立。此步依賴古典語義，MKO 假設 a1 已明示採用。
• S08.1 · inverse_equivalence · restricted_quantifier, quantifier_negation — 展開定義與量詞否定律都是雙向等價。
• S08 · inverse_equivalence · L_restricted_negation — 引理第 (i) 部分的兩個方向都在 S08.1、S08.2 證明。
• S07 · premise_audit · S06, exists_intro — 需要見證在論域 U 中；反向（由存在陳述推回見證就是 0）並未宣稱。
• S06 · premise_audit · numeric_evaluation, order_basics, roster_membership — 見證必須同時在 U 中並使 Q 失敗，兩項都已核對（N5）；不宣稱 0 是唯一見證。
• S05 · premise_audit · forall_elim, contradiction, numeric_evaluation — 此步需要 4∈ℤ 與精確比較 16≥10（N4）；它不改變 φ₁ 的真假，只說明換論域就是換陳述。
• S04.2 · premise_audit · roster_membership, case_analysis, forall_intro — 關鍵是情況分析涵蓋全部可能，這只在 U 被完整列出時成立；若 U 無限或只列出一部分，有限個情況涵蓋不了，引理就不能用。
• S04.1 · premise_audit · roster_membership, forall_elim, and_intro_elim — 每次代入都需要 a_i∈U，這由列舉保證；另一個方向在 S04.2 另行證明，此步不宣稱。
• S04 · inverse_equivalence · L_finite_forall — 引理兩個方向都在 S04.1、S04.2 證明；反向即由 φ₁ 取回每個 P(a_i)。
• S03 · premise_audit · S02, numeric_evaluation, order_basics, and_intro_elim — 需要的是 U 的每一個元素都被檢查到；六個比較都是精確的整數比較。這一步不宣稱反向。
• S02 · inverse_equivalence · numeric_evaluation, neg_mul — 每個等式都可獨立重算（N1、N2）；等號兩邊是同一個整數，雙向成立。
• S01 · premise_audit · G1, G2, mko_quantifier_def, restricted_quantifier — 此步只固定論域、述詞與展開方式，不推出新事實。若論域沒有明示，後面的枚舉與否定都沒有確定的意義。

錯誤控制與反例

通過的例子不是無限全稱的證明

MKO 指出的常見誤解是把幾個通過例子當成無限全稱證明。φ₁ 在 U 上為真，是因為 U 只有六個元素且全部檢查過（S04 的引理需要完整列舉）。同樣六個檢查對 ℤ 沒有任何結論：x=4 時 16≥10，∀x∈ℤ, x²<10 為假（S05）。

否定全稱不是「全部不滿足」

MKO 的第二個誤解是把否定全稱寫成所有元素皆不滿足。¬∀x∈U Q(x) 等價於 ∃x∈U ¬Q(x)（S08，為真，見證 0），而 ∀x∈U ¬Q(x) 為假（S09，x=2 時 4>2）。否定時要同時切換 ∀／∃ 並否定述詞，只改符號或只否定述詞都不對。

空論域的邊界

∀x∈∅ R(x) 為真不是因為 R 被某個元素滿足，而是因為沒有元素能成為反例（S14）；∃x∈∅ R(x) 為假，因為沒有可用的見證（S15）。所以由「全稱為真」推出「存在為真」需要論域非空。

• −2、0、3 都滿足 x²<10，所以 ∀x∈ℤ, x²<10 → reject — x=4∈ℤ 時 4²=16≥10；幾個通過例子不證明無限論域上的全稱。
• ¬∀x∈U, x²>x 的意思是每個 x∈U 都有 x²≤x → reject — 正確否定是 ∃x∈U, x²≤x；而 x=2 時 4>2，所以「每個都 x²≤x」為假。
• ∃x∈U, x²=2 為假，所以 ∃x∈ℝ, x²=2 也為假 → reject — 論域不同就是陳述不同；√2∈ℝ 且 (√2)²=2。
• ∀x∈U ∃y∈U, x+y=0 為真，因為每個整數都有加法反元素 → reject — x=3 時唯一滿足 3+y=0 的 y 是 −3，但 −3∉U（−3<−2）；論域限制了可用的見證。

結論與限制

在 U={−2,−1,0,1,2,3} 上：φ₁（∀x∈U, x²<10）為真，由完整枚舉證得；φ₂（∀x∈U, x²>x）為假，其否定為 ∃x∈U, x²≤x，見證 x=0；φ₃（∃x∈U, x²=2）為假，其否定為 ∀x∈U, x²≠2。論域為空集合時，∀x∈∅ R(x) 為真，∃x∈∅ R(x) 為假。這些結論只對所述論域成立：x²<10 在 ℤ 上不全成立（x=4），x²=2 在 ℝ 上有解（√2）。

• N3 與 N7 是對 U 的六個元素的有限檢查，恰好覆蓋 U，用來重算 S03 與 S10；它們對其他論域沒有任何結論。
• 本稿只採古典真值語義（MKO 假設 a1）；S08.2 與 S08.3 用到的古典蘊涵在非古典語義下不一定成立，本稿不處理。也不宣稱一階邏輯完備性已形式證明。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 52748a3a639b1ac5e04a07bec894402431f75d818c68e49a83f15fee1b2c1952
• original source SHA-256: 52748a3a639b1ac5e04a07bec894402431f75d818c68e49a83f15fee1b2c1952
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）