# 量詞與明示論域

全稱與存在量詞必須綁定論域；古典真值語義下，空論域的全稱為真、存在為假。

mko-quantifier · definition · v0.10.0



## 數學敘述

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





## 代表公式（精確 TeX）

P(x)





## 成立條件


- 論域 U 和述詞 P 的語義已明示；本輪採古典真值解讀。
- 題庫限定有限明示整數論域與可判定述詞，完整枚舉只封閉該有限論域。





## 符號作用域


- P — 已指定語義的述詞，P(x) 真值依輸入而定
- x — 述詞輸入；量詞綁定見完整陳述





## 直觀、定義與常見誤解

全稱要求所有允許元素都通過；存在只需一個允許見證。量詞順序與論域屬於陳述本身，不可任意交換或忽略。

U=∅ 時，沒有反例可違反全稱，因此全稱為真；存在無可用見證，因此為假。否定量詞時同時切換全稱／存在並否定述詞，不能只改符號。

本輪逐一列出有限 U 的整數元素，精確檢查大小、相等或非零整除述詞。結果不外推到全部整數、實數或無限論域，也不宣稱一階邏輯的完備性已形式證明。

把幾個通過例子當成無限全稱證明，或把否定全稱誤寫成所有元素皆不滿足。





## 已採用的推導導讀

[量詞與明示論域：在有限整數論域上判定全稱、存在及其否定](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-quantifier-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [命題](https://ocme.evemisslab.com/zh-Hant/mko/mko-proposition/) — 量化形成封閉陳述；本輪有限可判定題目可逐項驗證真值。
- [集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-set/) — 量詞的限制論域由集合指定。





## 驗證界線

有限可判定真值可完整重算；一般量詞推理與古典邏輯形式橋仍未附 Evidence。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

綁定 Forall、Exists、受限量詞、古典否定法則及空論域邊界。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/quantifier.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-quantifier/index.md)