Variables and expressions: a value depends on the assignment, the scope and the number system

Goal and scope

Let E=x+1, F=(x+1)÷2 and H=Σ_{x=1}^{3}(x+1). (1) In ℤ, evaluate E at x=2 and at x=5 and prove that E has no fixed value independent of x; (2) evaluate F at x=4 in ℚ and in ℤ; (3) evaluate H when x=5 is assigned from outside; (4) decide whether (x+1)+x and 2x+1, and whether x·x and 2x, are equivalent on ℤ; (5) distinguish the expression x+1 from the equation x+1=3 and find the solution set of the equation in ℤ.

Uses only the usual operations of ℤ and ℚ with exact division (G1), one free variable x and one bound variable of a finite sum. It illustrates the MKO: the value of an algebraic expression is determined jointly by the assignment, the scope, the number system and the operation rules, and an expression without an equality sign is not an equation. It does not build a formal syntax or an evaluation function, does not treat several variables or function types, and does not change the canonical MKO or its English edition.

Givens and symbols

• add_assoc
• add_comm
• distributive
• mul_inverse_nonzero
• order_basics
• numeric_evaluation

• G1 — Systems and operations: ℤ⊂ℚ with the usual addition and multiplication; exact division u÷v in a system S is the unique w∈S with v·w=u, and is undefined in S when there is no such w (in ℚ, for v≠0, u÷v=u·(1/v)).
• G2 — Expressions: E=x+1, F=(x+1)÷2 and H=Σ_{x=1}^{3}(x+1), where Σ_{x=1}^{3} g(x) means g(1)+g(2)+g(3) and the x in H is bound by the summation sign.
• G3 — Objects to compare: (x+1)+x and 2x+1; x·x and 2x; and the equation x+1=3 over ℤ.

• x — the variable; its scope and number system are stated in each part
• U[x:=c] — the value of U after replacing the free occurrences of x by c
• u\div v — exact division: the unique w with v·w=u
• \sum_{x=1}^{3} g(x) — g(1)+g(2)+g(3), where x is a bound variable
• U\equiv_{\mathbb{Z}} V — U and V are equivalent on ℤ

Rules and sources

• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_var_expr · cited — The value of an algebraic expression is jointly determined by its variable assignments, scopes, types or number systems, and operation rules. An algebraic expression without an equality sign is not itself an equation. · mko-variable-expression
• mko_equation · cited — Given two expressions L(x) and R(x) in a common context, the solution set of L(x)=R(x) consists of all allowed x for which both sides are defined and equal. · mko-equation
• eval_assign · prerequisite — Evaluation: the value of an expression U under the assignment x:=c (c∈S) is obtained by replacing every free occurrence of x in U by c and computing with the operations of S; if some operation along the way is undefined in S, U has no value under that assignment.
• bound_var · prerequisite — Bound variables: the x in Σ_{x=1}^{3} g(x) is bound by the summation sign and takes only the values 1, 2, 3; an outside assignment to x does not replace bound occurrences; renaming the bound variable consistently (for example to k) does not change the value.
• expr_equiv · prerequisite — Equivalence of expressions: U and V are equivalent on S when, for every c∈S, U[x:=c] and V[x:=c] both have values and these are equal.
• int_no_gap · prerequisite — No gaps in the integers: for integers k and m, k≤m or k≥m+1.
• L_double · lemma — For every x∈ℤ: (x+1)+x=2x+1.

Main derivation

x+1,\ (x+1)\div 2,\ \sum_{x=1}^{3}(x+1)

\text{value}=U[x:=c]\ \text{computed in a stated}\ S

E[x:=2]\ \text{in}\ \mathbb{Z}

2+1=3

E[x:=5]\ \text{in}\ \mathbb{Z}

5+1=6

E[x:=2]=3,\ E[x:=5]=6

\neg\exists v\in\mathbb{Z}\ \forall c\in\mathbb{Z}:\ E[x:=c]=v

F[x:=4]\ \text{in}\ \mathbb{Q}

(4+1)\div 2=5\cdot\tfrac{1}{2}=\tfrac{5}{2}

F[x:=4]\ \text{in}\ \mathbb{Z}:\ w\in\mathbb{Z}\ \text{with}\ 2w=5\ ?

w\le 2\ \lor\ w\ge 3

\forall w\in\mathbb{Z}:\ 2w\neq 5

F[x:=4]\ \text{has no value in}\ \mathbb{Z},\ \text{while}\ F[x:=4]=\tfrac{5}{2}\ \text{in}\ \mathbb{Q}

H=\sum_{x=1}^{3}(x+1)

H=(1+1)+(2+1)+(3+1)

(1+1)+(2+1)+(3+1)

2+3+4=9

H[x:=5]

H[x:=5]=H=9\neq 18=(5+1)+(5+1)+(5+1)

(x+1)+x

2x+1

\text{for arbitrary}\ x\in\mathbb{Z}:\ (x+1)+x=2x+1

(x+1)+x\equiv_{\mathbb{Z}}2x+1

x\cdot x\ \text{vs}\ 2x

1\cdot 1=1\neq 2=2\cdot 1,\ \text{so}\ x\cdot x\not\equiv_{\mathbb{Z}}2x

x+1\quad\text{vs}\quad x+1=3

\{x\in\mathbb{Z}\mid x+1=3\}=\{2\}

\text{conclusions of S04, S07, S10, S12, S13, S14}

\text{value of }U=\text{function of assignment, scope, system and rules}

Substeps and lemmas

w\le 2

2w\le 4<5,\ \text{so}\ 2w\neq 5

w\ge 3

2w\ge 6>5,\ \text{so}\ 2w\neq 5

(x+1)+x

(x+x)+1

(x+x)+1

2x+1

Reverse audits

• S15 · sufficient_goal_reduction · S04, S07, S10, S12, S13, S14, and_intro_elim — Goal G: answers to the five parts of the problem. Sufficient condition H: the conclusions of S04, S07, S10, S12, S13 and S14; H⇒G just lists them. H is proved forwards from G1 to G3; G is never used as a premise.
• S14 · premise_audit · mko_equation, eq_congruence, S02, set_extensionality — The solution set is computed by an equivalence (adding −1 and adding 1 undo each other), and both sides are defined in ℤ; the step never treats the expression x+1 itself as an equation.
• S13 · premise_audit · expr_equiv, quantifier_negation, numeric_evaluation — One counterexample is enough to refute 'equal for all x'; it is not claimed that x=1 is the only place where they differ.
• S12 · premise_audit · S11, forall_intro, expr_equiv — It needs the x of S11 to be arbitrary; N11 is only an independent cross-check on a few grid points, and the generality comes from the rule-based derivation in S11.
• S11.2 · inverse_equivalence · distributive, mul_one, numeric_evaluation — Only identities are used, so the replacement of equals holds both ways.
• S11.1 · inverse_equivalence · add_assoc, add_comm — Associativity and commutativity are identities for all integers and hold read backwards too.
• S11 · inverse_equivalence · L_double — The two expressions name the same integer; every step of the lemma is a replacement of equals and can be reversed.
• S10 · premise_audit · S09, bound_var, eval_assign — It needs every x in H to be recognised as bound by the Σ; the conclusion is about H only and does not claim that the outside x has no effect in other expressions.
• S09 · inverse_equivalence · numeric_evaluation — Both sides are the same integer and can be recomputed (N8).
• S08 · inverse_equivalence · finite_sum_rules, bound_var — Unfolding and folding the summation sign are the two directions of one definition.
• S07 · premise_audit · S06, S06.1, S06.2, case_analysis, eval_assign — It needs the two branches to cover all integers; the conclusion is only about x=4 and does not claim that F has no value in ℤ for every x (for example at x=3, (3+1)÷2=2).
• S06.2 · premise_audit · order_basics — As in S06.1; no converse is claimed.
• S06.1 · premise_audit · order_basics, two_nonzero — 2>0 keeps the direction of the inequality; only 2w≠5 is concluded and no converse is claimed.
• S06 · premise_audit · G1, int_no_gap — The case split relies on w being an integer; in ℚ, w=5/2 lies between the two branches, which is exactly why S05 and S07 reach different conclusions.
• S05 · inverse_equivalence · eval_assign, mul_inverse_nonzero, numeric_evaluation — Both sides are the same rational number; the condition 2≠0 makes 1/2 exist, and uniqueness comes from multiplying by 1/2 and by 2 undoing each other.
• S04 · premise_audit · S02, S03, contradiction, eq_refl_symm_trans — Two different values are enough to refute 'has a fixed value'; the step neither needs nor claims anything about the full range of E.
• S03 · inverse_equivalence · eval_assign, numeric_evaluation — Both sides are the same integer and can be recomputed (N2).
• S02 · inverse_equivalence · eval_assign, numeric_evaluation — E[x:=2], 2+1 and 3 are different names for the same integer and can be recomputed independently (N1); this is only the value at x=2.
• S01 · premise_audit · G1, G2, mko_var_expr, eval_assign — This step only lists the data that evaluation needs and derives no new fact.

Error controls and negative controls

The value of E=x+1 depends on the assignment to x

The MKO names the common mistake of treating an expression with a variable as if it already had a fixed value. x+1 is 3 at x=2 and 6 at x=5 (S02, S03), and S04 proves it has no value independent of x. So 'x+1=3' can only be read as a requirement on x (an equation), not as 'the expression x+1 is 3'.

Without an equality sign there is no equation

Another mistake identified in the MKO is calling any text containing x an equation. x+1 has no equality sign and cannot be 'solved'; whoever says 'solving x+1 gives x=−1' has silently supplied the equation x+1=0. An equation needs two expressions and an equality sign, and its solution set also requires both sides to be defined in the stated system (S14).

Bound variables do not take outside values

The x in H=Σ_{x=1}^{3}(x+1) is bound by the summation sign. With x=5 assigned outside, H is still 9; replacing the bound occurrences by 5 as well wrongly gives 18 (S10). Renaming the bound variable to k, as Σ_{k=1}^{3}(k+1), shows that it has nothing to do with the outside x.

• The value of x+1 is 3 → reject — Only under the assignment x=2; at x=5 the value is 6 (S03, S04).
• x+1 is an equation and its solution is x=−1 → reject — x+1 has no equality sign; x=−1 solves a different equation, x+1=0, which the problem never stated.
• x·x and 2x agree at x=0 and x=2, so they are equivalent on ℤ → reject — At x=1, 1≠2 (S13); agreement at some values does not give equivalence.
• (x+1)÷2 at x=4 is 5/2 in every number system → reject — In ℤ no integer w has 2w=5, so there is no value (S07).
• With x=5 assigned outside, Σ_{x=1}^{3}(x+1)=18 → reject — The x in H is bound and is not replaced by the outside assignment; the value is still 9 (S10).

Result and limitations

In ℤ, E equals 3 at x=2 and 6 at x=5, so it has no fixed value. F at x=4 equals 5/2 in ℚ and has no value in ℤ. With x=5 assigned outside, H is still 9, because the x in H is bound. (x+1)+x and 2x+1 are equivalent on ℤ; x·x and 2x are not (at x=1, 1≠2). x+1 is an expression with no solution set; x+1=3 is an equation whose solution set in ℤ is {2}.

• This guide takes the verbal definitions eval_assign, bound_var and expr_equiv as premises; it does not build a formal syntax, a recursive definition of free variables or an evaluation function (the MKO's formal next step).
• N11 is a degree-one polynomial identity check on the grid {0,1}, used only as an independent cross-check of S11; the generality in this guide comes from the rule-based derivation of S11.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 7bae56c281b5a8252bb4564f48957ca0b1b4d33f1093e8dfcaed3df6d8e85309
• original source SHA-256: 4e7848b5ae3d6ec21f3cf5b0f6297ac58148c0066c80cbcda81b003b28355a4a
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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