命題

數學敘述

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

代表公式（精確 TeX）

P

成立條件

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

符號作用域

• P — 命題變項

直觀、定義與常見誤解

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

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

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

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

已採用的推導導讀

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

前置知識

驗證界線

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

not_formalized

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

下一個義務

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

同源結構化資料

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