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

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

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

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



## 目標與範圍

在明示有限論域 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)。





## 逐步主鏈

S01 · definition操作前

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

條件：無

規則：restricted_quantifier · 依賴：G1, G2, G3, mko_quantifier_def

葉節點依據：mko_quantifier_def + restricted_quantifier

MKO 把論域與述詞都當作陳述本身的一部分，所以先固定 U={−2,−1,0,1,2,3} 與三個述詞 P(x)：x²<10、Q(x)：x²>x、E(x)：x²=2，採古典真值語義。受限量詞展開為：∀x∈U P(x) 指「對每個 x，若 x∈U 則 P(x)」；∃x∈U E(x) 指「有某個 x 同時滿足 x∈U 與 E(x)」。之後每一步都在這個明示論域上判定。



S02 · equivalent操作前

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

操作後

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

條件：無

規則：numeric_evaluation · 依賴：G1

葉節點依據：numeric_evaluation + neg_mul

對 U 的六個元素逐一精確計算平方：(−2)²=4、(−1)²=1、0²=0、1²=1、2²=4、3²=9。負數的平方用 (−u)(−u)=u·u。這張表之後由 P、Q、E 三個述詞共用。



S03 · implies操作前

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)

條件：無

規則：numeric_evaluation · 依賴：S02, G2

葉節點依據：numeric_evaluation + order_basics + and_intro_elim

P(x) 是 x²<10。由 S02，六個平方值 4、1、0、1、4、9 都小於 10（最大的是 9<10），所以 P 在 U 的每一個列出元素上都成立；再用合取把六個事實合在一起。



S04 · equivalent操作前

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

操作後

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

條件：U=\{-2,-1,0,1,2,3\}\ \text{listed completely}

規則：L_finite_forall · 依賴：S03, G1, L_finite_forall

葉節點依據：forall_elim + forall_intro + case_analysis + roster_membership

U 以列舉給出：a₁=−2、a₂=−1、a₃=0、a₄=1、a₅=2、a₆=3。依引理 L_finite_forall（n=6），∀x∈U P(x) 等價於六個 P(a_i) 的合取，而 S03 已證得這個合取，所以 φ₁ 為真。這是完整枚舉：結論成立正是因為 U 的每個元素都被檢查過。



S05 · implies操作前

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

操作後

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

條件：4\in\mathbb{Z}; 4\notin U

規則：contradiction · 依賴：S04, forall_elim, contradiction

葉節點依據：forall_elim + contradiction + numeric_evaluation + order_basics

φ₁ 為真不能外推到 ℤ。若 ∀x∈ℤ P(x) 成立，代入 4∈ℤ 得 4²<10，即 16<10，與 16≥10 矛盾，所以 ∀x∈ℤ, x²<10 為假。MKO 強調完整枚舉只判定指定有限論域上的陳述：4 不在 U 中，所以它不影響 φ₁，但它推翻了把論域換成 ℤ 之後的另一個陳述。



S06 · implies操作前

Q(0):\ 0^2>0

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S02, G2

葉節點依據：numeric_evaluation + order_basics + roster_membership

Q(x) 是 x²>x。取 x=0：0²=0，而 0>0 不成立（序的三分律：0=0 時 0>0 與 0<0 都不成立）。0 是 U 的列出元素，所以 0∈U 且 ¬Q(0)。x=1 也有 1>1 不成立，但一個見證已足夠。



S07 · implies操作前

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

操作後

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

條件：無

規則：exists_intro · 依賴：S06, exists_intro

葉節點依據：exists_intro

依 ∃引入，U 中的 0 使 ¬Q(0) 成立，所以 ∃x∈U ¬Q(x) 為真。存在陳述只需一個允許的見證。



S08 · equivalent操作前

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

操作後

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

條件：無

規則：L_restricted_negation · 依賴：S07, L_restricted_negation

葉節點依據：quantifier_negation + classical_implication + restricted_quantifier

依引理 L_restricted_negation 第 (i) 部分，∃x∈U ¬Q(x) 與 ¬∀x∈U Q(x) 等價。所以 φ₂ 的否定為真，φ₂ 為假。否定全稱時要同時把 ∀ 換成 ∃ 並否定述詞，論域 U 保持不變。



S09 · implies操作前

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

操作後

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

條件：2\in U

規則：contradiction · 依賴：S02, G2, forall_elim, contradiction

葉節點依據：forall_elim + contradiction + numeric_evaluation + order_basics

常見錯誤是把 ¬∀x∈U Q(x) 寫成 ∀x∈U ¬Q(x)（「所有元素都不滿足」）。核對後者：若它成立，代入 2∈U 得 ¬Q(2)，即 4>2 不成立；但 2²=4>2 成立，矛盾。所以 ∀x∈U ¬Q(x) 為假，而 S07、S08 證得正確的否定 ∃x∈U ¬Q(x) 為真。兩者真假不同，因此不等價。



S10 · implies操作前

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)

條件：無

規則：numeric_evaluation · 依賴：S02, G2

葉節點依據：numeric_evaluation + and_intro_elim

E(x) 是 x²=2。由 S02，六個平方值 4、1、0、1、4、9 都不等於 2，這些都是精確的整數比較。所以 E 在每個列出元素上都失敗。



S11 · equivalent操作前

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

條件：U\ \text{listed completely}

規則：L_finite_forall · 依賴：S10, L_finite_forall

葉節點依據：forall_elim + forall_intro + case_analysis + roster_membership

把引理 L_finite_forall 用在述詞 ¬E 上（引理對任何述詞 R 成立）：六個 ¬E(a_i) 的合取等價於 ∀x∈U ¬E(x)。



S12 · equivalent操作前

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

操作後

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

條件：無

規則：L_restricted_negation · 依賴：S11, L_restricted_negation

葉節點依據：quantifier_negation + de_morgan_logic + classical_implication + restricted_quantifier

依引理第 (ii) 部分，∀x∈U ¬E(x) 等價於 ¬∃x∈U E(x)。所以 φ₃ 為假，它的否定 ∀x∈U, x²≠2 為真。要證存在陳述為假，必須檢查全部允許元素；只找到一個失敗值不夠。



S13 · implies操作前

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

操作後

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

條件：2\ge 0

規則：exists_intro · 依賴：G2, sqrt_def, exists_intro

葉節點依據：sqrt_def + exists_intro

把同一個述詞 E 放到論域 ℝ：2≥0，所以 √2 存在，√2∈ℝ 且 (√2)²=2；依 ∃引入，∃x∈ℝ, x²=2 為真。φ₃ 在 U 上為假、在 ℝ 上為真，說明論域是陳述本身的一部分，不能省略或任意替換。



S14 · implies操作前

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

操作後

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

條件：無

規則：forall_intro · 依賴：restricted_quantifier, empty_set_def, classical_implication, forall_intro

葉節點依據：restricted_quantifier + empty_set_def + classical_implication + forall_intro

把論域換成空集合。展開為 ∀x(x∈∅⇒R(x))。任取 x：x∈∅ 為假，前件為假的蘊涵在古典語義下為真；x 是任意的，依 ∀引入，全稱為真。沒有任何元素能成為反例，所以不論 R 是什麼，∀x∈∅ R(x) 都為真。



S15 · implies操作前

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

操作後

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

條件：無

規則：quantifier_negation · 依賴：restricted_quantifier, empty_set_def, and_intro_elim, quantifier_negation

葉節點依據：restricted_quantifier + empty_set_def + and_intro_elim + forall_intro + quantifier_negation

∃x∈∅ R(x) 展開為 ∃x(x∈∅∧R(x))。對每個 x，合取的第一項 x∈∅ 為假，所以合取為假，即 ∀x ¬(x∈∅∧R(x))；依量詞否定律，這就是 ¬∃x(x∈∅∧R(x))。空論域沒有可用的見證，存在陳述為假。



S16 · implies操作前

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

條件：無

規則：and_intro_elim · 依賴：S04, S08, S09, S12, S14, S15

葉節點依據：and_intro_elim

彙整：φ₁ 為真（S04，完整枚舉）；φ₂ 為假，其否定是 ∃x∈U, x²≤x，見證 x=0（S08），而不是 ∀x∈U, x²≤x（S09 證其為假）；φ₃ 為假，其否定是 ∀x∈U, x²≠2（S12）；空論域上全稱為真、存在為假（S14、S15）。







## 局部子步與引理

S04.1 · implies操作前

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

操作後

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

條件：U=\{a_i\mid 1\le i\le n\}

規則：forall_elim · 依賴：roster_membership, forall_elim

葉節點依據：forall_elim + roster_membership + and_intro_elim

設 U={a_i ∣ 1≤i≤n}，R 為任意述詞。對每個 i，由列舉成員關係得 a_i∈U；對全稱 ∀x∈U R(x) 用 ∀消去代入 x=a_i，得 R(a_i)。把 n 個結果用合取合在一起。這是引理的「⇒」方向。



S04.2 · implies操作前

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

操作後

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

條件：U=\{a_i\mid 1\le i\le n\}

規則：forall_intro · 依賴：roster_membership, case_analysis, eq_replace, forall_intro

葉節點依據：forall_intro + case_analysis + roster_membership + eq_replace

假設合取成立。任取 x∈U，對 x 不加其他假設。由列舉成員關係，x=a_i 對某個 i 成立，共有 n 種情況。在情況 x=a_i 中，合取給出 R(a_i)，以相等的 x 代換 a_i 得 R(x)。n 種情況涵蓋 U 的全部元素，所以 R(x) 成立；x 是任意的，依 ∀引入得 ∀x∈U R(x)。S04.1 與 S04.2 合起來證得引理 L_finite_forall。



S08.1 · equivalent操作前

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

操作後

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

條件：無

規則：quantifier_negation · 依賴：restricted_quantifier, quantifier_negation

葉節點依據：restricted_quantifier + quantifier_negation

對任意述詞 R：先把受限全稱展開成 ∀x(x∈U⇒R(x))，再用無限制的量詞否定律 ¬∀x ψ(x) ⇔ ∃x ¬ψ(x)，其中 ψ(x) 是 x∈U⇒R(x)。



S08.2 · equivalent操作前

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

條件：無

規則：classical_implication · 依賴：S08.1, classical_implication

葉節點依據：classical_implication + de_morgan_logic + restricted_quantifier

古典語義下 ¬(A⇒B) ⇔ A∧¬B（因 A⇒B 等價於 ¬A∨B，再用德摩根律與雙重否定）。對每個 x 取 A 為 x∈U、B 為 R(x)，得 ∃x(x∈U∧¬R(x))，也就是 ∃x∈U ¬R(x)。S08.1 與 S08.2 證得引理第 (i) 部分。



S08.3 · equivalent操作前

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

操作後

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

條件：無

規則：de_morgan_logic · 依賴：restricted_quantifier, quantifier_negation, de_morgan_logic, classical_implication

葉節點依據：quantifier_negation + de_morgan_logic + classical_implication + restricted_quantifier + logic_chain

第 (ii) 部分：¬∃x(x∈U∧R(x)) ⇔ ∀x ¬(x∈U∧R(x))（量詞否定律）⇔ ∀x(x∉U ∨ ¬R(x))（德摩根律）⇔ ∀x(x∈U⇒¬R(x))（古典蘊涵 ¬A∨B ⇔ A⇒B），也就是 ∀x∈U ¬R(x)。S08.3 證得引理第 (ii) 部分。







## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-quantifier-01.json)