# 反例與論域資格

反例必須屬於被聲稱的論域且使全稱述詞失敗；域外值和找不到反例都不能自動證明原命題。

mko-counterexample · definition · v0.10.0



## 數學敘述

對全稱陳述 ∀x∈U P(x)，c 是有效反例當且僅當 c∈U 且 P(c) 為假。一個有效反例即可否定該全稱陳述；沒有找到反例本身不是證明，除非論域有限且已完整驗證所有元素。





## 代表公式（精確 TeX）

P(c)





## 成立條件


- 全稱陳述的論域及述詞已明示。
- 最小反例只指本輪有限整數反例集合的數值最小值；集合為空時明示不存在。





## 符號作用域


- P — 待檢驗的全稱述詞
- c — 候選反例





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

先查 c 是否在 U，再查 P(c) 是否失敗。即使同一個代數公式在域外也可計算，域外失敗值仍不是這個全稱命題的反例。

限制到 V⊆U 後，原反例可能離開 V 而失去資格；這只表示該見證不再有效，不等於新全稱陳述必定為真。

有限整數論域可以枚舉全部失敗值、篩選候選集合並選最小值。最小值和『不存在』都以完整失敗集合重算，不從抽樣失敗／成功推論無限論域。

以域外值反駁受限全稱，或以一段搜尋沒有找到反例當成普遍證明。





## 已採用的推導導讀

[反例與論域資格：n²+n+11 的質數性、失敗集合與最小反例](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-counterexample-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [量詞與明示論域](https://ocme.evemisslab.com/zh-Hant/mko/mko-quantifier/) — 反例否定的是綁定論域的全稱陳述。
- [數學證明](https://ocme.evemisslab.com/zh-Hant/mko/mko-proof/) — 需區分合法反駁、有限枚舉及一般證明義務。





## 驗證界線

本輪有限見證可精確驗證；沒有聲稱所有一般命題的反例搜尋可判定或完備。

not_formalized

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





## 下一個義務

綁定見證的集合成員資格、否定述詞和受限全稱反駁；有限最小值另明示存在性。





## 同源結構化資料

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

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