Proposition: deciding which candidate sentences are propositions, and separating 'is a proposition' from 'is proved true'

Goal and scope

In an introductory classical context, decide for each candidate whether it is a proposition, and for each proposition decide whether it is true, with reasons: s1 '7 is prime'; s2 '4 is prime'; s3 'Is 7 prime?'; s4 'Compute 3+4.'; s5 'x>0' (x an unassigned integer variable), together with closed versions of s5: substituting x=2 and x=−1, prefixing ∀x∈ℤ, and prefixing ∃x∈ℤ.

Uses the MKO's introductory classical context: a well-formed closed declarative sentence is a proposition and in this context is either true or false (MKO assumption a2). Treats only a few concrete candidates about integers; it does not discuss intuitionistic logic, self-referential paradoxes or the full syntax of a formal language, and does not change the canonical MKO or its English edition.

Givens and symbols

• divides_def
• division_algorithm
• order_basics
• quantifier_negation
• numeric_evaluation

• G1 — Context: introductory classical logic about integers with the usual arithmetic and order. A candidate sentence is a proposition exactly when it is a well-formed declarative sentence with no unassigned free variable; such a proposition is, in this context, exactly one of true or false (MKO assumptions a1 and a2).
• G2 — Candidates: s1 '7 is prime'; s2 '4 is prime'; s3 'Is 7 prime?'; s4 'Compute 3+4.'; s5 'x>0', where x is an unassigned integer variable.
• G3 — Definition of prime: an integer p is prime exactly when p≥2 and no integer d with 2≤d≤p−1 satisfies d∣p.

• P — a proposition
• s_1,\ s_2,\ s_3,\ s_4,\ s_5 — the five candidate sentences
• x>0 — an open sentence with the free variable x
• \forall x\in\mathbb{Z},\ \exists x\in\mathbb{Z} — universal and existential quantifiers, two ways of closing an open sentence
• d\mid n — d divides n: n=dk for some integer k

Rules and sources

• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• add_zero · prerequisite — Additive identity: u+0=u.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
• mko_prop · cited — This entry uses an introductory classical context: a proposition P may be true or false, but being a proposition does not mean that P has been proved true. · mko-proposition
• prop_test · prerequisite — Test for propositions (this context): a candidate is a proposition exactly when it is a well-formed declarative sentence with no unassigned free variable. Questions and commands are not declarative; a declarative sentence with an unassigned free variable is an open sentence, which becomes a proposition only after substitution or quantification closes it.
• prime_def · prerequisite — Prime: an integer p is prime ⇔ p≥2 and no integer d with 2≤d≤p−1 satisfies d∣p.
• int_no_gap · prerequisite — No gaps in the integers: for integers k and m, k≤m or k≥m+1.
• L_rem · lemma — For an integer n and a positive integer d: if n=dq+r with q an integer and 0<r<d, then d∤n.

Main derivation

\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

Substeps and lemmas

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

Reverse audits

• S13 · sufficient_goal_reduction · S02, S05, S06, S07, S08, S09, S10, S11, S12, and_intro_elim — Goal G: a verdict for each candidate. Sufficient condition H: the conclusions of S02 to S12; H⇒G just lists them. H is proved forwards from G1 to G3; G is never used as a premise.
• S12 · premise_audit · exists_intro, two_nonzero — One witness is enough to prove an existential statement.
• S11 · premise_audit · quantifier_negation, order_basics, exists_intro — One counterexample suffices to refute a universal statement; x=0 is not claimed to be the only one (x=−1 is another).
• S10 · premise_audit · order_basics, two_nonzero, numeric_evaluation — Each substitution result is a closed declarative sentence and hence a proposition; its truth is decided by the order properties.
• S09 · premise_audit · prop_test, G2 — It must be confirmed that the context assigns no value to x; if it did, the verdict would differ.
• S08 · premise_audit · prop_test, numeric_evaluation — The verdict depends only on the sentence type; the contrasting '3+4=7' can be recomputed.
• S07 · premise_audit · prop_test — The verdict depends only on the sentence type; s3 is not claimed to be the same object as s1.
• S06 · premise_audit · prop_test, prime_def, divides_def, exists_intro — Refuting s2 needs only the witness d=2; s2 is still a proposition, because that status depends only on form.
• S05 · sufficient_goal_reduction · S03, S04, and_intro_elim — Goal G: s1 is true. Sufficient condition H: the two conjuncts from S03; H⇒G by the equivalence S03. H is proved forwards in S04; G is never used as a premise.
• S04.2 · premise_audit · division_algorithm, contradiction — The key is uniqueness of the remainder; existence alone would not give the contradiction.
• S04.1 · premise_audit · divides_def, add_zero — This only rewrites d∣n in the form of a division with remainder (remainder 0).
• S04 · premise_audit · L_rem, int_no_gap, numeric_evaluation — The five identities can be recomputed (N1 to N5). Checking case by case is a proof here precisely because the range is finite and listed completely; this differs from supporting a universal statement over an infinite domain by finitely many examples.
• S03 · inverse_equivalence · prime_def — Unfolding and folding a definition are two-way.
• S02 · premise_audit · G2, prop_test — Only the form (declarative, closed) is checked; s1 is not claimed to be true here, its truth is proved separately in S03 to S05.
• S01 · premise_audit · G1, mko_prop, prop_test — This step only states the test and derives no new fact; the true-or-false dichotomy is limited to this context (MKO assumption a2).

Error controls and negative controls

Being a proposition is not being proved true

The MKO names the common mistake of reading 'is a proposition' as 'has been proved true'. s1 was a proposition already at S02 and got its proof only at S05; s2 is a proposition but false (S06), and what is proved is its negation ¬s2. So 'P is a proposition' only says that P can be asserted or denied; truth and proof are separate matters.

Questions, commands and open sentences

Another mistake identified in the MKO is treating questions, commands or unclosed open expressions as propositions. s3 and s4 assert nothing (S07, S08); s5 is declarative but x is unassigned, so its truth changes with x (S09, S10). Check the sentence type first, then whether any free variable is unassigned.

Say how an open sentence is closed

The single open sentence x>0 closes into different propositions: substituting x=2 gives a true one, x=−1 a false one, prefixing ∀ a false one and prefixing ∃ a true one (S10 to S12). Saying 'x>0 is true' is meaningless until the way of closing it is stated.

• 'Is 7 prime?' is a proposition because its answer is yes → reject — A question asserts nothing and is neither true nor false; what is true is the proposition s1 (S07).
• '4 is prime' is false, so it is not a proposition → reject — A false proposition is still a proposition; the status depends only on form (S06).
• x>0 is true → reject — x is unassigned; at x=−1 it is false and at x=2 it is true (S10).
• Since 1>0, 2>0 and 3>0, ∀x∈ℤ, x>0 → reject — x=0 is a counterexample (S11); finitely many positive cases cannot establish a universal statement over an infinite domain.

Result and limitations

s1 '7 is prime' is a proposition and true (proved); s2 '4 is prime' is a proposition but false (its negation proved); the question s3 and the command s4 are not propositions; s5 'x>0' is an open sentence and not itself a proposition. Its closed versions are propositions: 2>0 true, −1>0 false, ∀x∈ℤ, x>0 false (counterexample x=0), ∃x∈ℤ, x>0 true (witness x=1). Being a proposition is decided by form and is independent of having been proved true.

• The test prop_test is a working definition for the introductory classical context; self-referential sentences and a full definition of well-formedness in a formal language are not treated here.
• N6 is a finite check over d=2 to 6 and only recomputes the five cases already listed completely in S04; the proof itself is S04 with its sub-steps.

Verification and source binding

14 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: f92ed859a98fb4b70ab6353e1cfab4a7c1931edf858182744aa06e993740ad07
• original source SHA-256: f92ed859a98fb4b70ab6353e1cfab4a7c1931edf858182744aa06e993740ad07
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)