邏輯連接詞：以整除命題檢驗 ∨、→、↔ 與括號

目標與範圍

對整數 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 — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• 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。

逐步主鏈

\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

4\mid 12,\ 6\mid 12

\mathrm{T},\ \mathrm{T}

4\mid 12\ \lor\ 6\mid 12

\mathrm{T}

\text{assume}\ 4\mid n\ (n\in\mathbb{Z}\ \text{arbitrary})

n=4k\ \text{for some}\ k\in\mathbb{Z}

n=4k

n=2(2k),\ 2k\in\mathbb{Z},\ \text{so}\ 2\mid n

\text{under the assumption}\ 4\mid n:\ 2\mid n

\forall n\in\mathbb{Z}:\ P(n)\to Q(n)

n=2

Q(2):\ 2=2\cdot 1,\ \mathrm{T}

k\in\mathbb{Z}\ \text{with}\ 4k=2\ ?

k\le 0\ \lor\ k\ge 1

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))

\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}

n=3

P(3)=\mathrm{F},\ Q(3)=\mathrm{F}

P(3)=\mathrm{F},\ Q(3)=\mathrm{F}

P(3)\to Q(3)=\mathrm{T}

2+2=4,\ 7=2\cdot 3+1

(2+2=4)\to(7\ \text{is odd})=\mathrm{T}

\neg Q(2)\land P(2)\quad\text{vs}\quad\neg(Q(2)\land P(2))

\mathrm{F}\quad\text{vs}\quad\mathrm{T}

\text{conclusions of S03, S06, S09, S10, S12, S13, S14}

\text{answers to parts (1) to (5)}

局部子步與引理

k\le 0

4k\le 0<2,\ \text{so}\ 4k\neq 2

k\ge 1

4k\ge 4>2,\ \text{so}\ 4k\neq 2

4k=3,\ k\in\mathbb{Z}

\text{impossible: } k\le 0\Rightarrow 4k\le 0<3;\ k\ge 1\Rightarrow 4k\ge 4>3

2k=3,\ k\in\mathbb{Z}

\text{impossible: } k\le 1\Rightarrow 2k\le 2<3;\ k\ge 2\Rightarrow 2k\ge 4>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、反控制與修訂記錄）