# 邏輯連接詞：以整除命題檢驗 ∨、→、↔ 與括號 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-logical-connectives/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-logical-connectives-01 · production-20261019-adopted-96 ## 目標與範圍 對整數 n，令 P(n) 為「4∣n」，Q(n) 為「2∣n」。(1) 判定「4∣12 ∨ 6∣12」的真假，說明析取是含括或；(2) 證明 ∀n∈ℤ (P(n)→Q(n))；(3) 證明 ∀n∈ℤ (Q(n)→P(n)) 為假，因而 ∀n∈ℤ (P(n)↔Q(n)) 為假；(4) 判定 P(3)→Q(3) 與「2+2=4 → 7 是奇數」的真假，說明蘊涵不是因果；(5) 比較 ¬Q(2)∧P(2) 與 ¬(Q(2)∧P(2)) 的真假。 依 MKO 的連接詞定義，在入門古典二值語境中以真值條件判定複合命題的真假。只用整除與奇偶的具體命題；不處理直覺主義、模態或相關邏輯；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - divides_def - imp_intro - forall_intro - quantifier_negation - order_basics - numeric_evaluation - G1 — 語境：入門古典二值邏輯；每個命題恰為真（T）或假（F）之一（mko-proposition 的語境）。連接詞依 MKO 定義。 - G2 — 整除：對整數 d、n，d∣n 表示存在整數 k 使 n=dk。對每個整數 n，P(n) 為「4∣n」，Q(n) 為「2∣n」。 - G3 — 具體命題：「6∣12」；「2+2=4」；「7 是奇數」，其中奇數指存在整數 m 使該數等於 2m+1。 - \neg,\ \land,\ \lor — 否定、合取、（含括）析取 - \to,\ \leftrightarrow — （材料）蘊涵、雙條件 - P(n),\ Q(n) — 4∣n 與 2∣n - d\mid n — 存在整數 k 使 n=dk - \mathrm{T},\ \mathrm{F} — 真、假 ## 規則與來源 - divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。 - imp_intro · prerequisite — →引入（釋放假設）：若在暫時假設 P 的作用域中推出 Q，則得到 P⇒Q；此後 P 不再可當作已知使用。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - order_basics · prerequisite — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。 - mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_conn · cited — 對命題 P、Q，¬P 表示否定，P∧Q 表示兩者皆成立，P∨Q 表示至少一者成立，P→Q 表示若 P 則 Q，P↔Q 表示兩方向皆成立。 · mko-logical-connectives - truth_table · prerequisite — 古典真值條件：¬P 為真 ⇔ P 為假；P∧Q 為真 ⇔ 兩者皆真；P∨Q 為真 ⇔ 至少一者為真（含兩者皆真）；P→Q 為假 ⇔ P 真且 Q 假，其餘情形為真；P↔Q 為真 ⇔ P→Q 與 Q→P 皆真，即 P、Q 真值相同。 - int_no_gap · prerequisite — 整數沒有空隙：對整數 k 與 m，必有 k≤m 或 k≥m+1。 ## 逐步主鏈 S01 · definition操作前 \neg P,\ P\land Q,\ P\lor Q,\ P\to Q,\ P\leftrightarrow Q 操作後 \text{truth value of each compound determined by those of}\ P,\ Q 條件：無 規則：mko_conn · 依賴：G1 葉節點依據：mko_conn + truth_table 依 MKO，¬P 是否定，P∧Q 要求兩者皆成立，P∨Q 要求至少一者成立，P→Q 表示若 P 則 Q，P↔Q 要求兩個方向。在古典二值語境（G1）中，這些定義寫成真值條件（truth_table）：複合命題的真假只由成分的真假決定，與成分之間有沒有因果或時間關係無關。 S02 · implies操作前 4\mid 12,\ 6\mid 12 操作後 \mathrm{T},\ \mathrm{T} 條件：無 規則：divides_def · 依賴：G2, G3 葉節點依據：divides_def + exists_intro + numeric_evaluation 12=4·3，3 是整數，所以 4∣12 為真；12=6·2，所以 6∣12 為真。兩個成分都為真。 S03 · implies操作前 4\mid 12\ \lor\ 6\mid 12 操作後 \mathrm{T} 條件：無 規則：truth_table · 依賴：S01, S02 葉節點依據：truth_table 依 ∨ 的真值條件，至少一者為真即為真；這裡兩者都為真，所以「4∣12 ∨ 6∣12」為真。若把 ∨ 誤讀成排他或（恰好一者為真），這個式子會被判為假；MKO 的 ∨ 是含括或，允許兩者同時成立。 S04 · implies操作前 \text{assume}\ 4\mid n\ (n\in\mathbb{Z}\ \text{arbitrary}) 操作後 n=4k\ \text{for some}\ k\in\mathbb{Z} 條件：無 規則：divides_def · 依賴：G2 葉節點依據：divides_def + exists_elim 要證 ∀n (P(n)→Q(n))：任取整數 n，不加額外假設，並在暫時假設 4∣n 的範圍內推理。依整除定義，有整數 k 使 n=4k（以新名字 k 表示這個見證）。 S05 · implies操作前 n=4k 操作後 n=2(2k),\ 2k\in\mathbb{Z},\ \text{so}\ 2\mid n 條件：無 規則：mul_assoc · 依賴：S04 葉節點依據：mul_assoc + divides_def + exists_intro + numeric_evaluation 4=2·2，依乘法結合律 4k=(2·2)k=2(2k)；2k 是整數（整數對乘法封閉），所以依整除定義 2∣n。 S06 · implies操作前 \text{under the assumption}\ 4\mid n:\ 2\mid n 操作後 \forall n\in\mathbb{Z}:\ P(n)\to Q(n) 條件：無 規則：imp_intro · 依賴：S04, S05 葉節點依據：imp_intro + forall_intro 在暫時假設 4∣n 下推出了 2∣n，依 →引入釋放假設得 P(n)→Q(n)；n 是任取的，依全稱推廣得 ∀n∈ℤ (P(n)→Q(n))。這只證了一個方向。 S07 · implies操作前 n=2 操作後 Q(2):\ 2=2\cdot 1,\ \mathrm{T} 條件：無 規則：divides_def · 依賴：G2 葉節點依據：divides_def + exists_intro + numeric_evaluation 檢查反方向 Q(n)→P(n)。取 n=2：2=2·1，1 是整數，所以 2∣2，Q(2) 為真。 S08 · case_split操作前 k\in\mathbb{Z}\ \text{with}\ 4k=2\ ? 操作後 k\le 0\ \lor\ k\ge 1 條件：k\in\mathbb{Z} 規則：int_no_gap · 依賴：G2 葉節點依據：int_no_gap + case_analysis P(2) 為真需要整數 k 使 4k=2。依 int_no_gap（m=0），每個整數 k 滿足 k≤0 或 k≥1，兩支在 S08.1、S08.2 處理。 S09 · implies操作前 Q(2)=\mathrm{T},\ \neg\exists k\in\mathbb{Z}:\ 4k=2 操作後 P(2)=\mathrm{F};\ Q(2)\to P(2)=\mathrm{F};\ \neg\forall n\,(Q(n)\to P(n)) 條件：無 規則：quantifier_negation · 依賴：S07, S08, S08.1, S08.2 葉節點依據：case_analysis + truth_table + quantifier_negation 兩支都得 4k≠2，所以沒有整數 k 使 4k=2，P(2) 為假。依 → 的真值條件，前件真、後件假時蘊涵為假，所以 Q(2)→P(2) 為假。n=2 是反例，依量詞否定 ∀n∈ℤ (Q(n)→P(n)) 為假。 S10 · implies操作前 \forall n\,(P(n)\to Q(n))\ \text{true},\ \forall n\,(Q(n)\to P(n))\ \text{false} 操作後 \forall n\in\mathbb{Z}:\ P(n)\leftrightarrow Q(n)\ \text{is false} 條件：無 規則：contradiction · 依賴：S06, S09 葉節點依據：contradiction + iff_intro + forall_elim 假設 ∀n (P(n)↔Q(n)) 為真。取 n=2 得 P(2)↔Q(2)，依雙條件的定義推出 Q(2)→P(2)，與 S09 矛盾。所以這個全稱雙條件為假。S06 證明的方向對所有 n 都成立，但只有一個方向不足以得到雙條件。 S11 · implies操作前 n=3 操作後 P(3)=\mathrm{F},\ Q(3)=\mathrm{F} 條件：無 規則：divides_def · 依賴：G2 葉節點依據：divides_def + int_no_gap + order_basics n=3 的兩個成分都為假：S11.1 證明沒有整數 k 使 4k=3，S11.2 證明沒有整數 k 使 2k=3。 S12 · implies操作前 P(3)=\mathrm{F},\ Q(3)=\mathrm{F} 操作後 P(3)\to Q(3)=\mathrm{T} 條件：無 規則：truth_table · 依賴：S11, S11.1, S11.2, S06 葉節點依據：truth_table + forall_elim 依 → 的真值條件，前件為假時蘊涵為真，所以 P(3)→Q(3) 為真；這也與 S06 在 n=3 的特例一致（∀消去）。雖然 2∤3，這個蘊涵仍為真：它的真假只看真值，不表示 4∣3 會「導致」什麼。 S13 · implies操作前 2+2=4,\ 7=2\cdot 3+1 操作後 (2+2=4)\to(7\ \text{is odd})=\mathrm{T} 條件：無 規則：truth_table · 依賴：G3, S01 葉節點依據：truth_table + exists_intro + numeric_evaluation 2+2=4 為真；7=2·3+1，3 是整數，所以 7 是奇數，為真。依 → 的真值條件，真→真為真。兩個命題之間沒有任何因果或推導關係，蘊涵仍為真：材料蘊涵只是一個真值條件，不表示因果，也不表示時間先後。 S14 · implies操作前 \neg Q(2)\land P(2)\quad\text{vs}\quad\neg(Q(2)\land P(2)) 操作後 \mathrm{F}\quad\text{vs}\quad\mathrm{T} 條件：無 規則：truth_table · 依賴：S07, S09 葉節點依據：truth_table Q(2) 為真（S07），P(2) 為假（S09）。在 ¬Q(2)∧P(2) 中，¬ 只作用於 Q(2)，最外層連接詞是 ∧：¬T∧F=F∧F=F。在 ¬(Q(2)∧P(2)) 中，最外層連接詞是 ¬：Q(2)∧P(2)=T∧F=F，取否定得 T。括號改變了最外層連接詞，也改變了真值。 S15 · implies操作前 \text{conclusions of S03, S06, S09, S10, S12, S13, S14} 操作後 \text{answers to parts (1) to (5)} 條件：無 規則：and_intro_elim · 依賴：S03, S06, S09, S10, S12, S13, S14 葉節點依據：and_intro_elim (1) 「4∣12 ∨ 6∣12」為真（S03）；(2) ∀n (P(n)→Q(n)) 已證（S06）；(3) ∀n (Q(n)→P(n)) 為假（S09），所以 ∀n (P(n)↔Q(n)) 為假（S10）；(4) P(3)→Q(3) 與「2+2=4 → 7 是奇數」都為真（S12、S13）；(5) ¬Q(2)∧P(2) 為假、¬(Q(2)∧P(2)) 為真（S14）。 ## 局部子步與引理 S08.1 · implies操作前 k\le 0 操作後 4k\le 0<2,\ \text{so}\ 4k\neq 2 條件：4>0 規則：order_basics · 依賴：S08 葉節點依據：order_basics + mul_zero 若 k<0，乘以正數 4 得 4k<0；若 k=0，4k=0。所以 4k≤0<2，4k≠2。 S08.2 · implies操作前 k\ge 1 操作後 4k\ge 4>2,\ \text{so}\ 4k\neq 2 條件：4>0 規則：order_basics · 依賴：S08 葉節點依據：order_basics + mul_one 若 k>1，乘以 4 得 4k>4；若 k=1，4k=4。所以 4k≥4>2，4k≠2。 S11.1 · implies操作前 4k=3,\ k\in\mathbb{Z} 操作後 \text{impossible: } k\le 0\Rightarrow 4k\le 0<3;\ k\ge 1\Rightarrow 4k\ge 4>3 條件：4>0 規則：int_no_gap · 依賴：S11 葉節點依據：int_no_gap + order_basics + case_analysis 依 int_no_gap，k≤0 或 k≥1。k≤0 時乘以 4>0 得 4k≤0<3；k≥1 時得 4k≥4>3。兩支都得 4k≠3，所以 4∤3，P(3) 為假。 S11.2 · implies操作前 2k=3,\ k\in\mathbb{Z} 操作後 \text{impossible: } k\le 1\Rightarrow 2k\le 2<3;\ k\ge 2\Rightarrow 2k\ge 4>3 條件：2>0 規則：int_no_gap · 依賴：S11 葉節點依據：int_no_gap + order_basics + case_analysis 依 int_no_gap（m=1），k≤1 或 k≥2。k≤1 時 2k≤2<3；k≥2 時 2k≥4>3。兩支都得 2k≠3，所以 2∤3，Q(3) 為假。 ## 逐步反向審查 - S15 · sufficient_goal_reduction · S03, S06, S09, S10, S12, S13, S14, and_intro_elim — 目標 G：五個部分的答案。足夠條件 H：所列各步的結論；H⇒G 只是並列。H 由 G1 到 G3 正向證成，沒有把 G 當作前提。 - S14 · premise_audit · S07, S09, truth_table — 兩式用的成分真值相同，差別只在結構。 - S13 · premise_audit · truth_table, numeric_evaluation, exists_intro — 只用到兩個成分的真值。 - S12 · premise_audit · truth_table, S06, forall_elim — 只需前件為假；Q(3) 為假用來說明「後件為假，蘊涵仍為真」。 - S11.2 · premise_audit · int_no_gap, order_basics, case_analysis — 兩支涵蓋全部整數。 - S11.1 · premise_audit · int_no_gap, order_basics, case_analysis — 兩支涵蓋全部整數。 - S11 · premise_audit · divides_def, int_no_gap, order_basics — 兩個「沒有見證」都在子步中以涵蓋全部整數的分情況證明。 - S10 · premise_audit · S06, S09, iff_intro, forall_elim, contradiction — 用到雙條件包含兩個方向（iff_intro）；不宣稱 P(n)↔Q(n) 對每個 n 都假：例如 n=4 時 4=4·1、4=2·2，兩者皆真，雙條件為真。 - S09 · premise_audit · S07, S08, case_analysis, truth_table, quantifier_negation — 一個反例足以否定全稱蘊涵；case_analysis 涵蓋了所有整數 k。 - S08.2 · premise_audit · order_basics, mul_one — 同 S08.1。 - S08.1 · premise_audit · order_basics, mul_zero — 用到 4>0 保持不等號方向；不宣稱反向。 - S08 · premise_audit · int_no_gap — 兩支涵蓋全部整數；這依賴 k 是整數（k=1/2 不在任何一支中）。 - S07 · premise_audit · divides_def, exists_intro — 一個整數見證 1 就足夠。 - S06 · premise_audit · S04, S05, imp_intro, forall_intro — S04 的 n 沒有額外條件，所以可以推廣；結論只是 P→Q，不宣稱 Q→P。 - S05 · premise_audit · mul_assoc, divides_def, exists_intro — 需要 2k 是整數作為見證；N3 是對恆等式 4k=2(2k) 的獨立核對。 - S04 · premise_audit · divides_def, exists_elim, imp_intro — 暫時假設只在 S04 到 S06 的範圍內使用，S06 會把它釋放。 - S03 · premise_audit · S02, truth_table — 只需一個成分為真；兩個都真不影響結論。 - S02 · premise_audit · divides_def, exists_intro, numeric_evaluation — 每個整除各需一個整數見證（3 與 2），可重算（N1、N2）。 - S01 · premise_audit · G1, mko_conn, truth_table — 此步只固定定義，不推出新事實。 ## 錯誤控制與反例 析取是含括或MKO 指出常見誤解是把析取當成排他或。4∣12 與 6∣12 都為真，所以「4∣12 ∨ 6∣12」為真（S03）；若當成排他或就會錯判為假。日常語言中「或」有時帶排他意味，數學的 ∨ 不帶。 蘊涵不是因果MKO 的另一個誤解是把蘊涵當成因果。P(3)→Q(3) 為真只因前件為假（S12）；「2+2=4 → 7 是奇數」為真只因兩者皆真（S13），兩者之間沒有因果關係。要證明「若 P 則 Q」對所有情形成立，仍需像 S04 到 S06 那樣的推理；但單一蘊涵的真假只看真值。 雙條件要兩個方向MKO 的第三個誤解是只證一個方向便宣稱雙條件。S06 對所有整數證明了 4∣n → 2∣n，但 n=2 使反方向失敗（S09），所以 ∀n (4∣n ↔ 2∣n) 為假（S10）。證明 P↔Q 必須分別證明 P→Q 與 Q→P。 - 「4∣12 或 6∣12」為假，因為兩者都成立 → reject — ∨ 是含括或，兩者皆真時析取為真（S03）。 - 已證 ∀n(4∣n→2∣n)，所以 ∀n(4∣n↔2∣n) → reject — n=2 時 2∣2 真而 4∣2 假，反方向失敗（S09、S10）。 - 「4∣3 → 2∣3」為假，因為 2∤3 → reject — 前件 4∣3 為假，蘊涵為真（S12）。 - ¬A∧B 與 ¬(A∧B) 的意思相同 → reject — 取 A 為 2∣2（真）、B 為 4∣2（假）：前者為假，後者為真（S14）。 ## 結論與限制 「4∣12 ∨ 6∣12」為真，因為 ∨ 是含括或。∀n∈ℤ (4∣n → 2∣n) 成立，但 ∀n∈ℤ (2∣n → 4∣n) 為假（反例 n=2），所以 ∀n∈ℤ (4∣n ↔ 2∣n) 為假。4∣3 → 2∣3 與「2+2=4 → 7 是奇數」都為真，蘊涵只看真值而不表示因果。¬(2∣2)∧(4∣2) 為假，¬((2∣2)∧(4∣2)) 為真，括號決定最外層連接詞。 - 真值條件是古典二值語境中的定義；在直覺主義邏輯中 → 與 ∨ 的意義不同，本稿不處理。 - N3 是在格點上的一次多項式恆等式核對，只交叉核對 S05 的 4k=2(2k)；一般性來自 S04 到 S06 的推理。 ## 驗證及來源綁定 13 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 8c4378aa84c06b4b7dd718820bdb2b5a2f72f9a464ab78ec19745a2813a16d7a - original source SHA-256: 8c4378aa84c06b4b7dd718820bdb2b5a2f72f9a464ab78ec19745a2813a16d7a - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-logical-connectives-01.json)