邏輯連接詞

數學敘述

對命題 P、Q，¬P 表示否定，P∧Q 表示兩者皆成立，P∨Q 表示至少一者成立，P→Q 表示若 P 則 Q，P↔Q 表示兩方向皆成立。

代表公式（精確 TeX）

P\land Q

成立條件

• P 與 Q 是具有明確命題語境的命題。

符號作用域

• P — 左命題
• Q — 右命題
• ∧ — 合取連接詞

直觀、定義與常見誤解

合取 P∧Q 只有在 P、Q 都成立時成立；析取 P∨Q 採含括或，允許兩者同時成立。

材料蘊涵 P→Q 是命題關係，不自動表示時間先後或因果；雙條件 P↔Q 則要求兩方向的蘊涵。

符號的作用域與括號會改變複合命題的結構，閱讀時必須先辨識最外層連接詞。

常見誤解是把析取當成排他或、把蘊涵當成因果，或只證一個方向便宣稱雙條件。

已採用的推導導讀

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

前置知識

• 命題 — 邏輯連接詞以一個或兩個命題形成複合命題。

驗證界線

真值表可檢查有限命題指派，但不構成全部推理規則的形式證明。

not_formalized

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

下一個義務

分別綁定 Not、And、Or、箭頭與 Iff 的精確形式聲明及證據。

同源結構化資料

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