# 命題：判定候選語句是否為命題，並區分「是命題」與「已證明為真」 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-proposition/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-proposition-01 · production-20261019-adopted-96 ## 目標與範圍在入門古典語境中，逐一判定下列候選是否為命題；是命題者再判定真假並給出理由：s1「7 是質數」；s2「4 是質數」；s3「7 是質數嗎？」；s4「計算 3+4。」；s5「x>0」（x 是未指定的整數變數），以及 s5 的封閉版本：代入 x=2 與 x=−1、加上 ∀x∈ℤ、加上 ∃x∈ℤ。採 MKO 的入門古典語境：良構且封閉的直述句是命題，在此語境中非真即假（MKO 假設 a2）。只處理關於整數的少數具體候選；不討論直覺主義邏輯、自指悖論或形式語言的完整語法；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - divides_def - division_algorithm - order_basics - quantifier_negation - numeric_evaluation - G1 — 語境：入門古典邏輯；陳述對象是整數，使用一般的算術與大小順序。候選語句是命題，當且僅當它是良構的直述句且沒有未指定的自由變數；這樣的命題在此語境中恰為真或假之一（MKO 假設 a1、a2）。 - G2 — 候選：s1「7 是質數」；s2「4 是質數」；s3「7 是質數嗎？」；s4「計算 3+4。」；s5「x>0」，其中 x 是未指定的整數變數。 - G3 — 質數的定義：整數 p 是質數，當且僅當 p≥2 且沒有整數 d 滿足 2≤d≤p−1 且 d∣p。 - P — 一個命題 - s_1,\ s_2,\ s_3,\ s_4,\ s_5 — 五個候選語句 - x>0 — 含自由變數 x 的開放句 - \forall x\in\mathbb{Z},\ \exists x\in\mathbb{Z} — 全稱與存在量詞，封閉開放句的兩種方式 - d\mid n — d 整除 n：存在整數 k 使 n=dk ## 規則與來源 - divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。 - division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤rv 之一；u0 推出 uwvw。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - add_zero · prerequisite — 加法單位元：u+0=u。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。 - mko_prop · cited — 本條目採入門古典邏輯語境：命題 P 可以為真或為假；P 是命題不表示 P 已被證明為真。 · mko-proposition - prop_test · prerequisite — 命題判準（本語境）：候選是命題，當且僅當它是良構的直述句且沒有未指定的自由變數。疑問句與命令句不是直述句；含未指定自由變數的直述句是開放句，經代入或量化封閉後才成為命題。 - prime_def · prerequisite — 質數：整數 p 是質數 ⇔ p≥2 且沒有整數 d 滿足 2≤d≤p−1 且 d∣p。 - int_no_gap · prerequisite — 整數沒有空隙：對整數 k 與 m，必有 k≤m 或 k≥m+1。 - L_rem · lemma — 對整數 n 與正整數 d：若 n=dq+r，其中 q 是整數且 00 操作後 s_5\ \text{is an open sentence, not a proposition} 條件：無規則：prop_test · 依賴：G2, S01, prop_test 葉節點依據：prop_test s5 是直述句，但 x 是未指定的自由變數，依 prop_test 它是開放句：它的真假要看 x 取什麼值（S10 會看到 x=2 時為真、x=−1 時為假），所以在封閉語境中它本身不是命題。要得到命題，必須代入或量化（MKO 第三段）。 S10 · implies操作前 x>0\ \text{with}\ x:=2\ \text{or}\ x:=-1 操作後 2>0\ (\mathrm{true}),\quad -1>0\ (\mathrm{false}) 條件：無規則：order_basics · 依賴：S09 葉節點依據：order_basics + two_nonzero 代入是一種封閉方式。x:=2 得命題「2>0」，為真（0<1<2）；x:=−1 得命題「−1>0」，為假：因 0<1，兩邊加 −1 得 −1<0，依三一律排除 −1>0。同一個開放句經不同代入得到兩個不同的命題，真假也不同。 S11 · implies操作前 \forall x\in\mathbb{Z},\ x>0 操作後 \text{false: counterexample}\ x=0 條件：無規則：quantifier_negation · 依賴：S09 葉節點依據：quantifier_negation + exists_intro + order_basics 全稱量化是另一種封閉方式：「∀x∈ℤ, x>0」沒有自由變數，是命題。取 x=0：0=0，依三一律 0>0 不成立，所以 ∃x∈ℤ, ¬(x>0)，依量詞否定得 ¬∀x∈ℤ, x>0，因此原先的全稱命題為假。1>0、2>0、3>0 等正例再多也不能證明這個全稱命題，而一個反例就足以否定它。 S12 · implies操作前 \exists x\in\mathbb{Z},\ x>0 操作後 \text{true: witness}\ x=1 條件：無規則：exists_intro · 依賴：S09 葉節點依據：exists_intro + two_nonzero 存在量化：「∃x∈ℤ, x>0」是命題。取 x=1，1>0 成立（0<1），依 ∃引入，這個命題為真。 S13 · implies操作前 \text{verdicts of S02 to S12} 操作後 \text{propositions: }s_1,s_2,\text{closures of }s_5;\ \text{not propositions: }s_3,s_4,s_5 條件：無規則：and_intro_elim · 依賴：S02, S05, S06, S07, S08, S09, S10, S11, S12 葉節點依據：and_intro_elim 命題：s1（真，S05 已證）、s2（假，S06 已證其否定）、s5 的四個封閉版本（2>0 真、−1>0 假、∀ 版本假、∃ 版本真）。不是命題：s3（疑問句）、s4（命令句）、s5 本身（開放句）。每個候選的命題身分都在判定真假之前確定。 ## 局部子步與引理 S04.1 · implies操作前 n=dq+r,\ 00 規則：divides_def · 依賴：divides_def 葉節點依據：divides_def + add_zero 證明引理 L_rem：設 n=dq+r 且 00;\ \text{hence}\ d\nmid n 條件：d>0 規則：division_algorithm · 依賴：S04.1, division_algorithm 葉節點依據：division_algorithm + contradiction 依帶餘除法的唯一性（d 是正整數），n 除以 d 的商與餘數唯一；n=dq+r 與 n=dk+0 的餘數都在 0 與 d 之間（含 0、不含 d），所以 r=0，與 r>0 矛盾。因此暫時假設不成立，d∤n。S04.1 與 S04.2 合起來證得引理 L_rem。 ## 逐步反向審查 - S13 · sufficient_goal_reduction · S02, S05, S06, S07, S08, S09, S10, S11, S12, and_intro_elim — 目標 G：對每個候選給出判定。足夠條件 H：S02 到 S12 的各項結論；H⇒G 只是並列。H 由 G1 到 G3 正向證成，沒有把 G 當作前提。 - S12 · premise_audit · exists_intro, two_nonzero — 一個見證就足以證明存在命題。 - S11 · premise_audit · quantifier_negation, order_basics, exists_intro — 一個反例足以否定全稱；不宣稱 x=0 是唯一反例（x=−1 也是）。 - S10 · premise_audit · order_basics, two_nonzero, numeric_evaluation — 每個代入結果都是封閉的直述句，因此是命題；真假由順序性質判定。 - S09 · premise_audit · prop_test, G2 — 需要確認 x 沒有在語境中被指定；若語境先指定了 x，結論會不同。 - S08 · premise_audit · prop_test, numeric_evaluation — 判定只依句型；對照的「3+4=7」可獨立重算。 - S07 · premise_audit · prop_test — 判定只依句型；不宣稱 s3 與 s1 是同一個對象。 - S06 · premise_audit · prop_test, prime_def, divides_def, exists_intro — 否定 s2 只需一個見證 d=2；s2 仍是命題，因為命題身分只看形式。 - S05 · sufficient_goal_reduction · S03, S04, and_intro_elim — 目標 G：s1 為真。足夠條件 H：S03 展開後的兩個合取項；H⇒G 由 S03 的等價。H 由 S04 正向證成，沒有把 G 當作前提。 - S04.2 · premise_audit · division_algorithm, contradiction — 關鍵是餘數唯一；只有存在性不足以導出矛盾。 - S04.1 · premise_audit · divides_def, add_zero — 只是把 d∣n 寫成帶餘除法的形式（餘數為 0）。 - S04 · premise_audit · L_rem, int_no_gap, numeric_evaluation — 五個算式可獨立重算（N1 到 N5）。這裡逐一檢查構成證明，正是因為論域有限而且已完整列出；這不同於用有限個例子去支持一個無窮論域上的全稱命題。 - S03 · inverse_equivalence · prime_def — 展開與收回定義是雙向的。 - S02 · premise_audit · G2, prop_test — 只檢查形式（直述、封閉）；不宣稱 s1 為真，真假在 S03 到 S05 另行證明。 - S01 · premise_audit · G1, mko_prop, prop_test — 此步只寫出判準，不推出新事實；真假二分只限本語境（MKO 假設 a2）。 ## 錯誤控制與反例是命題不等於已證明為真MKO 指出常見誤解是把「是命題」理解成「已證明為真」。s1 在 S02 就已是命題，直到 S05 才有證明；s2 是命題，卻是假的（S06），被證明的是它的否定 ¬s2。所以「P 是命題」只是說 P 可以被斷言或否定，真假與證明要另外處理。疑問句、命令句與開放句MKO 的另一個誤解是把疑問句、命令句或未封閉的開放表達式直接當作命題。s3 與 s4 不斷言任何事情（S07、S08）；s5 雖是直述句，但 x 未指定，真假隨 x 改變（S09、S10）。判定時先看句型，再看有沒有未指定的自由變數。封閉方式要說清楚同一個開放句 x>0 可以封閉成不同的命題：代入 x=2 為真、代入 x=−1 為假、加 ∀ 為假、加 ∃ 為真（S10 到 S12）。只說「x>0 是真的」沒有意義，必須說明是哪一種封閉。 - 「7 是質數嗎？」是命題，因為它的答案是肯定的 → reject — 疑問句不斷言任何事情，本身無所謂真假；為真的是命題 s1（S07）。 - 「4 是質數」是假的，所以它不是命題 → reject — 假的命題仍是命題；命題身分只看形式（S06）。 - x>0 為真 → reject — x 未指定；x=−1 時為假，x=2 時為真（S10）。 - 因為 1>0、2>0、3>0，所以 ∀x∈ℤ, x>0 → reject — x=0 是反例（S11）；有限個正例不能建立無窮論域上的全稱命題。 ## 結論與限制 s1「7 是質數」是命題且為真（已證明）；s2「4 是質數」是命題但為假（已證明其否定）；s3 疑問句與 s4 命令句不是命題；s5「x>0」是開放句，本身不是命題。s5 的封閉版本都是命題：2>0 真、−1>0 假、∀x∈ℤ, x>0 假（反例 x=0）、∃x∈ℤ, x>0 真（見證 x=1）。是否為命題由形式決定，與是否已證明為真無關。 - 本稿的命題判準（prop_test）是入門古典語境中的工作定義；自指語句與形式語言中良構性的完整定義不在此處理。 - N6 是在 d=2 到 6 上的有限核對，只重算 S04 中已完整列出的五個情形；證明本身在 S04 與其子步。 ## 驗證及來源綁定 14 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: f92ed859a98fb4b70ab6353e1cfab4a7c1931edf858182744aa06e993740ad07 - original source SHA-256: f92ed859a98fb4b70ab6353e1cfab4a7c1931edf858182744aa06e993740ad07 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-proposition-01.json)