Goal and scope
Fix the object f:D→ℤ with D={0,1,2,3} and f(x)=2x−1. Decide: the words 'double the input, then subtract 1' correspond to 2x−1; the table T1={(0,−1),(1,1),(2,3),(3,5)} represents f; the set of ordered pairs is the graph of f; the affine rule is recovered uniquely from the two rows (1,1) and (3,5); the table T2, with (3,5) replaced by (3,6), represents neither f nor any affine rule; T3, with a repeated input, is not a function table; g(x)=2x−1 defined on ℤ is not the same function as f; and a table supplies no values at unlisted points.
The worked exercises use integer-coefficient affine rules and completely listed finite tables or ordered pairs (MKO assumption a1); the auxiliary two-point affine lemma is stated for real coefficients and real coordinates; every check is made on the listed domain only, and unlisted points and the appearance of a graph supply no values (assumption a2). General semantics of diagrams and a fuller typed semantic bridge are not treated; the canonical MKO and its English edition are not changed.
Main derivation
S01 · definition
Before
\text{several representations}After
\text{object }f:D\to\mathbb{Z},\ D=\{0,1,2,3\},\ \text{row }(x,y)\ \text{means}\ f(x)=yConditions: none
Rule: mko_repr · Uses: G1, G2, mko_repr
Leaf basis: mko_repr + def_intro
By the MKO, the object, domain and interpretation rules must be fixed before deciding any correspondence. The object is f from G1, the domain is four integers, and the reading of tables is given by G2. Every later decision compares against these fixed settings, not appearances.
S02 · equivalent
Before
W:\ \text{double the input, then subtract 1}After
x\mapsto 2x-1
Conditions: none
Rule: def_unfold · Uses: G3, G1
Leaf basis: def_unfold
Follow the order of operations in the words: doubling first gives 2x, then subtracting 1 gives 2x−1. The order matters: 'subtract 1, then double' is 2(x−1)=2x−2, which gives −2 at x=0 instead of −1.
S03 · equivalent
Before
f(0),f(1),f(2),f(3)
After
-1,\ 1,\ 3,\ 5
Conditions: none
Rule: numeric_evaluation · Uses: G1
Leaf basis: numeric_evaluation
Compute at the four points of the domain: 2·0−1=−1, 2·1−1=1, 2·2−1=3, 2·3−1=5.
S04 · implies
Before
\text{inputs of }T_1:\ 0,1,2,3After
\text{each }x\in D\ \text{appears exactly once in }T_1Conditions: none
Rule: function_def · Uses: G4, G1, function_def
Leaf basis: function_def + finite_counting_basics
The inputs of T1 are 0, 1, 2, 3, exactly the four elements of D, each once. So T1 gives each x∈D exactly one output and defines a function on D (call it h₁).
S05 · implies
Before
h_1(x)\ \text{vs}\ f(x)\ \text{for }x\in DAfter
h_1=f\ \text{(}T_1\ \text{represents }f\text{)}Conditions: \text{same domain }D
Rule: function_def · Uses: S03, S04, G2, mko_repr_notes
Leaf basis: function_def + numeric_evaluation
Compare row by row: (0,−1) with f(0)=−1, (1,1) with f(1)=1, (2,3) with f(2)=3, (3,5) with f(3)=5; all four rows match. h₁ and f have the same domain D and the same value at every point, so by the definition of equality of functions h₁=f. This is the MKO's explicit semantic bridge: a common domain with every row matching.
S06 · equivalent
Before
\Gamma_f=\{(x,f(x))\mid x\in D\}After
\Gamma_f=\{(0,-1),(1,1),(2,3),(3,5)\}=T_1Conditions: none
Rule: set_builder · Uses: S03, G1, G4
Leaf basis: set_builder + set_extensionality
Ordered-pair representation: the graph of f is the set of all (x,f(x)); by S03 it lists four pairs, exactly the rows of T1, so as sets Γ_f=T1.
S07 · implies
Before
(x_1,y_1),(x_2,y_2),\ x_1\neq x_2
After
a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1\ \text{(unique)}Conditions: x_1\neq x_2
Rule: L_two_point · Uses: L_two_point
Leaf basis: mul_inverse_nonzero + eq_congruence
By Lemma L_two_point (uniqueness and existence proved in S07.1 and S07.2): two points with different x-coordinates determine exactly one affine rule.
S08 · implies
Before
(1,1),(3,5)\in T_1,\ 1\neq 3
After
a=\tfrac{5-1}{3-1}=2,\ b=1-2=-1;\ \text{rows }(0,-1),(2,3)\ \text{also satisfy }y=2x-1Conditions: 1\neq 3
Rule: L_two_point · Uses: S07, G4, S03
Leaf basis: L_two_point + numeric_evaluation
First confirm that the x-coordinates differ, 1≠3; then the lemma gives a=4/2=2 and b=1−2·1=−1, recovering y=2x−1. Two points only determine a candidate rule; the remaining rows (0,−1) and (2,3) must still be checked: 2·0−1=−1 and 2·2−1=3, both match.
S09 · implies
Before
T_2\ \text{row }(3,6),\ f(3)=5After
T_2\ \text{does not represent }f\ \text{nor any affine rule}Conditions: none
Rule: quantifier_negation · Uses: G4, S03, S07
Leaf basis: quantifier_negation + L_two_point + numeric_evaluation
The row of T2 at x=3 is 6, but f(3)=5; one mismatching row negates 'every row matches', so T2 does not represent f. Further, any affine rule representing T2 would pass through (0,−1) and (1,1) (with 0≠1), so by L_two_point it could only be y=2x−1, which gives 5≠6 at x=3; hence no affine rule represents T2. Matching the first three rows is not enough.
S10 · implies
Before
T_3\ni(1,1),(1,2)
After
T_3\ \text{is not a function table}Conditions: 1\neq 2
Rule: function_def · Uses: G4, function_def, mko_repr_notes
Leaf basis: function_def
A function assigns exactly one output to each input. In T3 the input 1 is paired with both 1 and 2, and 1≠2, so T3 is not a function table and cannot represent f or any function. It is also the case where L_two_point does not apply because the two points share an x-coordinate (a vertical arrangement): the slope through (1,1) and (1,2) would need division by 0.
S11 · implies
Before
g:\mathbb{Z}\to\mathbb{Z},\ f:D\to\mathbb{Z}After
g\neq f,\ \ g|_D=f
Conditions: D\neq\mathbb{Z}
Rule: function_def · Uses: G1, G5, function_def
Leaf basis: function_def + set_extensionality
g and f use the same formula but have different domains (ℤ and D), so by the definition of equality of functions they are not the same function; for example g(4)=7 is defined while 4∉D. Restricting g to D gives the same value as f at every point, so g|_D=f. This is why the MKO requires fixing the domain first.
S12 · implies
Before
x=4,\ x=\tfrac{1}{2}After
\text{no value supplied: }4,\tfrac{1}{2}\notin DConditions: none
Rule: mko_repr_notes · Uses: G1, G4, mko_repr_notes
Leaf basis: mko_repr_notes + function_def
T1 lists only the four points of D. f(4) is undefined because 4∉D, and 1/2 is not in D either. If the four points are plotted they look collinear, and the line passes through (1/2,0), but by MKO assumption a2 the appearance of a graph and unlisted points supply no values, so f(1/2)=0 cannot be claimed.
S13 · implies
Before
\text{decisions}After
W,\ 2x-1,\ T_1,\ \Gamma_f\ \text{represent }f;\ T_2,\ T_3,\ g\ \text{do not}Conditions: none
Rule: and_intro_elim · Uses: S02, S05, S06, S08, S09, S10, S11, S12
Leaf basis: and_intro_elim
Combine the decisions: with the object, domain and interpretation rule fixed, the words W, the formula 2x−1, the table T1 and the pair set Γ_f all represent f; the rows (1,1) and (3,5) recover the rule uniquely; T2 represents neither f nor any affine rule; T3 is not a function table; g differs from f in its domain; unlisted points have no values.