Coordinate plane: deciding axis or quadrant membership and comparing ordered pairs

Goal and scope

In a fixed Cartesian coordinate system, let A=(−3,2), B=(2,−3), B′=(6/3,−3), C=(0,−4), O=(0,0) and E=(−1/2,−5). First prove that the axes meet only at the origin and that every point either lies on an axis or lies in exactly one quadrant; then decide for each point its axis or quadrant, and decide whether A and B, and B and B′, are the same point.

Uses only the MKO's definitions: a fixed origin, perpendicular oriented axes and a unit on each, coordinates as ordered pairs of reals, the x-axis given by y=0 and the y-axis by x=0, and the quadrants off the axes given by the signs of the two coordinates. It infers no distance, angle or figure size (MKO assumption a2) and reads no coordinates from a sketch; the canonical MKO and its English edition are not changed.

Givens and symbols

• cartesian_product_def
• order_basics
• set_extensionality
• set_operations_def
• numeric_evaluation

• G1 — An origin, perpendicular oriented x- and y-axes and a unit on each axis are fixed in the plane; in this coordinate system each point corresponds to an ordered pair of reals (x,y)∈ℝ², and all points are compared in the same system (MKO assumptions a1, a2).
• G2 — The x-axis is 𝒳={(x,y)∈ℝ² ∣ y=0} and the y-axis is 𝒴={(x,y)∈ℝ² ∣ x=0}; Q_I={(x,y) ∣ x>0 and y>0}, Q_II={(x,y) ∣ x<0 and y>0}, Q_III={(x,y) ∣ x<0 and y<0}, Q_IV={(x,y) ∣ x>0 and y<0}.
• G3 — A=(−3,2), B=(2,−3), B′=(6/3,−3), C=(0,−4), O=(0,0) and E=(−1/2,−5), all given in the coordinate system of G1.

• (x,y) — the ordered coordinates of a point, the first read along the x-axis and the second along the y-axis
• \mathcal{X},\ \mathcal{Y} — the x-axis {y=0} and the y-axis {x=0}
• Q_{\mathrm{I}},\ Q_{\mathrm{II}},\ Q_{\mathrm{III}},\ Q_{\mathrm{IV}} — the first, second, third and fourth quadrants
• O — the origin (0,0)

Rules and sources

• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• 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.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• 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.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_coord_plane · cited — In a specified Cartesian coordinate system, a point has the ordered coordinates (x,y). The x-axis satisfies y=0 and the y-axis satisfies x=0, and they meet at (0,0). Away from the axes, the four quadrants are determined by the signs of x and y. · mko-coordinate-plane
• mko_quadrant_signs · cited — When x and y are both nonzero, the sign patterns (+,+), (−,+), (−,−) and (+,−) give the first, second, third and fourth quadrants; points on an axis belong to no quadrant. The origin lies on both axes. · mko-coordinate-plane
• L_classify · lemma — For every (x,y)∈ℝ²: if x=0 or y=0, it lies in no quadrant; if x≠0 and y≠0, it lies in exactly one quadrant.

Main derivation

\text{a point in the fixed coordinate system}

\text{point}\leftrightarrow(x,y)\in\mathbb{R}^2,\quad (x,y)=(x',y')\iff x=x'\land y=y'

\text{axes and quadrants}

\mathcal{X}=\{y=0\},\ \mathcal{Y}=\{x=0\},\ Q_{\mathrm{I}}=\{x>0,y>0\},\ Q_{\mathrm{II}}=\{x<0,y>0\},\ Q_{\mathrm{III}}=\{x<0,y<0\},\ Q_{\mathrm{IV}}=\{x>0,y<0\}

(x,y)\in\mathbb{R}^2

(x=0\lor y=0\Rightarrow\text{no quadrant})\ \land\ (x\neq 0\land y\neq 0\Rightarrow\text{exactly one quadrant})

\mathcal{X}\cap\mathcal{Y}

\{(0,0)\}

A=(-3,2)

A\in Q_{\mathrm{II}},\ A\notin\mathcal{X}\cup\mathcal{Y}

B=(2,-3)

B\in Q_{\mathrm{IV}},\ B\notin\mathcal{X}\cup\mathcal{Y}

(-3,2)\ \text{and}\ (2,-3)

A\neq B,\quad\text{while}\quad\{-3,2\}=\{2,-3\}

B'=\left(\tfrac{6}{3},-3\right)

B'=(2,-3)=B

C=(0,-4)

C\in\mathcal{Y},\ C\notin\mathcal{X},\ C\ \text{in no quadrant}

O=(0,0)

O\in\mathcal{X}\cap\mathcal{Y},\ O\ \text{in no quadrant}

E=\left(-\tfrac{1}{2},-5\right)

E\in Q_{\mathrm{III}},\ E\notin\mathcal{X}\cup\mathcal{Y}

A,B,B',C,O,E

A\in Q_{\mathrm{II}},\ B=B'\in Q_{\mathrm{IV}},\ E\in Q_{\mathrm{III}},\ C\in\mathcal{Y}\setminus\mathcal{X},\ O\in\mathcal{X}\cap\mathcal{Y},\ A\neq B

Substeps and lemmas

x=0\ \lor\ y=0

(x,y)\notin Q_{\mathrm{I}}\cup Q_{\mathrm{II}}\cup Q_{\mathrm{III}}\cup Q_{\mathrm{IV}}

x\neq 0\ \land\ y\neq 0

(x,y)\in Q_{\mathrm{I}}\cup Q_{\mathrm{II}}\cup Q_{\mathrm{III}}\cup Q_{\mathrm{IV}}

(x,y)\in Q_i\cap Q_j,\ i\neq j

\bot

(x,y)\in\mathcal{X}\cap\mathcal{Y}

(x,y)=(0,0)

(0,0)

(0,0)\in\mathcal{X}\cap\mathcal{Y}

Reverse audits

• S12 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S10, S11, and_intro_elim — Goal G: the classification of every point and the two comparisons. Sufficient condition H: the separate conclusions of S05 to S11; H⇒G is just conjunction. H is proved forwards from the coordinates and the definitions; G is never used as a premise.
• S11 · premise_audit · G3, S02, S03, mko_quadrant_signs — Uses only the signs of the coordinates (N8, N9).
• S10 · premise_audit · S03, S04, L_classify — Directly cites S04 and the lemma; no further computation is needed.
• S09 · premise_audit · S02, S03, L_classify — It needs the strict inequalities in the quadrant definitions; C may not be placed in the third or fourth quadrant (N7).
• S08 · inverse_equivalence · cartesian_product_def, numeric_evaluation — 6/3 and 2 are the same rational number (N6), so the two forms may replace each other in either direction.
• S07 · premise_audit · S01, cartesian_product_def, set_extensionality — One differing coordinate is enough for the points to differ (N5); the converse, that distinct points differ in a particular coordinate, is not claimed.
• S06 · premise_audit · G3, S02, S03, mko_quadrant_signs — As in S05, only the signs of the coordinates are used (N3, N4).
• S05 · premise_audit · G3, S02, S03, mko_quadrant_signs — Only the signs of the two coordinates are needed (N1, N2); the decision does not depend on any drawing.
• S04.2 · premise_audit · S04.1, set_extensionality, set_builder — Both directions are now proved, so the sets are equal.
• S04.1 · premise_audit · set_operations_def, cartesian_product_def — Uses only the definitions of intersection and of ordered pairs; the reverse inclusion is S04.2.
• S04 · premise_audit · S02, set_extensionality — Set equality needs both directions, proved separately in the sub-steps.
• S03.3 · premise_audit · S02, order_basics, contradiction — All six pairs of quadrants are checked; each pair has one coordinate with opposite signs, and the contradiction comes from trichotomy.
• S03.2 · premise_audit · S02, order_basics, case_analysis — The cases must cover every possibility: two signs for x and two for y give four cases, and none may be left out.
• S03.1 · premise_audit · S02, order_basics, set_operations_def — It relies on the strict inequalities in the quadrant definitions; with ≥ instead, the origin would fall into all four 'quadrants'.
• S03 · premise_audit · L_classify, order_basics, S02 — Relies only on the definitions of S02 and trichotomy of the reals; no particular point is involved.
• S02 · premise_audit · G2, def_intro, mko_quadrant_signs, set_builder — This step only names the sets; the strict inequalities are part of the definition and may not be relaxed to ≥ or ≤.
• S01 · premise_audit · G1, mko_coord_plane, cartesian_product_def — This step only fixes the representation and derives no new fact; in a different coordinate system the same point could have other coordinates, so every later decision is confined to the system of G1.

Error controls and negative controls

Points on an axis are in no quadrant

The first error named in the MKO is to put points on an axis, or the origin, into a quadrant. The quadrants are defined with strict inequalities (S02), so C=(0,−4), although its second coordinate is negative, is in neither the third nor the fourth quadrant, and the origin is not a point of the first quadrant (S03.1, S09, S10).

Ordered pairs do not commute

The second error named in the MKO is to treat an ordered pair as an unordered set. {−3,2}={2,−3}, but (−3,2)≠(2,−3): the first is in the second quadrant and the second in the fourth (S07). Whether two points coincide is decided by comparing corresponding coordinates one by one.

Coordinates are data, not read from a sketch

B′=(6/3,−3) is written differently from B but is the same point (S08), and E with first coordinate −1/2 might look close to the y-axis in a rough sketch. Decisions rest only on the stated coordinate values and the definitions; this guide also infers no distance between points and no figure size (MKO assumption a2).

• The origin (0,0) is in the first quadrant because both its coordinates are ≥0 → reject — Q_I requires x>0 and y>0; 0>0 is false, so the origin is in no quadrant.
• (−3,2)=(2,−3) because both use the same two numbers → reject — Equal ordered pairs need equal first coordinates, and −3≠2; the two points are even in different quadrants.
• C=(0,−4) has a negative second coordinate, so C is in the third or fourth quadrant → reject — The third and fourth quadrants both require x≠0 (x<0 or x>0), while C has x=0, so C is on the y-axis.
• B′=(6/3,−3) and B=(2,−3) are written differently, so they are different points → reject — 6/3=2, so both corresponding coordinates agree and B′=B.

Result and limitations

The axes meet only at the origin, and every point either lies on an axis (and then in no quadrant) or lies in exactly one quadrant. A=(−3,2)∈Q_II, B=(2,−3)=B′∈Q_IV, E=(−1/2,−5)∈Q_III, C=(0,−4) is on the y-axis and in no quadrant, and O is on both axes and in no quadrant; A≠B although {−3,2}={2,−3}.

• The correspondence between points and ordered pairs of reals (G1) is a premise of the coordinate system; this guide does not derive it from geometric axioms.
• This guide does not deal with distance, angle or figure size; those need a separate semantic bridge (MKO formal next).

Verification and source binding

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

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

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