命題：判定候選語句是否為命題，並區分「是命題」與「已證明為真」

目標與範圍

在入門古典語境中，逐一判定下列候選是否為命題；是命題者再判定真假並給出理由：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≤r<b。
• 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。
• 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 是整數且 0<r<d，則 d∤n。

逐步主鏈

\text{a candidate sentence}

\text{proposition}\iff\text{well-formed declarative sentence with no unassigned free variable}

s_1:\ 7\ \text{is prime}

s_1\ \text{is a proposition}

7\ \text{is prime}

7\ge 2\ \land\ \neg\exists d\in\mathbb{Z}\,(2\le d\le 6\ \land\ d\mid 7)

d\in\{2,3,4,5,6\}

d\nmid 7\ \text{for each such}\ d

7\ge 2,\ \text{and no}\ d\ \text{with}\ 2\le d\le 6\ \text{divides}\ 7

s_1\ \text{is true, and now proved}

s_2:\ 4\ \text{is prime}

s_2\ \text{is a proposition, and}\ \neg s_2\ \text{holds}

s_3:\ \text{Is 7 prime?}

s_3\ \text{is not a proposition}

s_4:\ \text{Compute}\ 3+4.

s_4\ \text{is not a proposition}

s_5:\ x>0

s_5\ \text{is an open sentence, not a proposition}

x>0\ \text{with}\ x:=2\ \text{or}\ x:=-1

2>0\ (\mathrm{true}),\quad -1>0\ (\mathrm{false})

\forall x\in\mathbb{Z},\ x>0

\text{false: counterexample}\ x=0

\exists x\in\mathbb{Z},\ x>0

\text{true: witness}\ x=1

\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

局部子步與引理

n=dq+r,\ 0<r<d;\ \text{assume}\ d\mid n

n=dk+0,\ 0\le 0<d

n=dq+r\ (0<r<d),\quad n=dk+0

r=0,\ \text{contradicting}\ r>0;\ \text{hence}\ d\nmid n

逐步反向審查

• 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、反控制與修訂記錄）