量詞與明示論域

數學敘述

在明示論域 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 的整數元素，精確檢查大小、相等或非零整除述詞。結果不外推到全部整數、實數或無限論域，也不宣稱一階邏輯的完備性已形式證明。

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

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 命題 — 量化形成封閉陳述；本輪有限可判定題目可逐項驗證真值。
• 集合 — 量詞的限制論域由集合指定。

驗證界線

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

not_formalized

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

下一個義務

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

同源結構化資料

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