# 命題

命題是在指定邏輯脈絡中可被斷言或否定，並可談論真假的有意義陳述。

mko-proposition · concept · v0.10.0



## 數學敘述

本條目採入門古典邏輯語境：命題 P 可以為真或為假；P 是命題不表示 P 已被證明為真。





## 代表公式（精確 TeX）

P





## 成立條件


- P 是指定邏輯脈絡中良構且有意義的命題。
- 真與假的二分敘述限於本條目採用的入門古典語境。





## 符號作用域


- P — 命題變項





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

命題是可以被斷言或否定的陳述。真的命題與假的命題都仍是命題；真假是命題的語義狀態，而不是判定某段文字是否屬於命題的唯一先決條件。

證明用來支持某命題為真，但『P 是命題』不等於『P 已經有證明』。在 Lean 中可先有 P : Prop，再另外詢問是否存在 P 的證明項。

像 x>0 這類含未指定自由變數的開放句，需經代入、量化或明確指定脈絡，才成為可在該封閉語境中評估的陳述。

常見誤解是把疑問句、命令句或未封閉的開放表達式直接當作命題，或把『是命題』誤解成『已證明為真』。





## 已採用的推導導讀

[命題：判定候選語句是否為命題，並區分「是命題」與「已證明為真」](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-proposition-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識







## 驗證界線

本條目是概念候選稿；研究來源不是 OCME Evidence，尚未建立計算檢查或 Lean 形式證明。

not_formalized

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





## 下一個義務

以 P : Prop 建立命題與證明項的最小 Lean 語義橋，並清楚區分古典真假語義所需的額外原理。





## 同源結構化資料

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

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