# 座標平面：判定點在哪條軸或哪個象限，並比較有序對

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-coordinate-plane/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-coordinate-plane-01 · production-20261019-adopted-96



## 目標與範圍

在固定的平面直角座標系中，給定 A=(−3,2)、B=(2,−3)、B′=(6/3,−3)、C=(0,−4)、O=(0,0)、E=(−1/2,−5)。先證明兩軸只交於原點、每個點要嘛在軸上、要嘛恰在一個象限中；再逐點判定它所在的軸或象限，並判定 A 與 B、B 與 B′ 是否為同一點。

只用 MKO 的定義：固定原點、互相垂直的有向軸與各軸單位，座標是實數有序對，x 軸由 y=0、y 軸由 x=0 定義，軸外的象限由兩坐標的正負號決定。不推論距離、角度或圖形尺寸（MKO 假設 a2），也不從示意圖讀坐標；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- cartesian_product_def
- order_basics
- set_extensionality
- set_operations_def
- numeric_evaluation


- G1 — 平面上已固定原點、互相垂直的有向 x 軸與 y 軸及各軸單位；在這個座標系中，每個點對應一個實數有序對 (x,y)∈ℝ²，所有點都在同一座標系中比較（MKO 假設 a1、a2）。
- G2 — x 軸 𝒳={(x,y)∈ℝ² ∣ y=0}，y 軸 𝒴={(x,y)∈ℝ² ∣ x=0}；Q_I={(x,y) ∣ x>0 且 y>0}，Q_II={(x,y) ∣ x<0 且 y>0}，Q_III={(x,y) ∣ x<0 且 y<0}，Q_IV={(x,y) ∣ x>0 且 y<0}。
- G3 — A=(−3,2)、B=(2,−3)、B′=(6/3,−3)、C=(0,−4)、O=(0,0)、E=(−1/2,−5)，皆在 G1 的座標系中給出。


- (x,y) — 點的有序座標，第一坐標沿 x 軸、第二坐標沿 y 軸讀取
- \mathcal{X},\ \mathcal{Y} — x 軸 {y=0} 與 y 軸 {x=0}
- Q_{\mathrm{I}},\ Q_{\mathrm{II}},\ Q_{\mathrm{III}},\ Q_{\mathrm{IV}} — 第一、二、三、四象限
- O — 原點 (0,0)





## 規則與來源


- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- 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。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_coord_plane · cited — 在指定平面直角座標系中，點的座標是有序對 (x,y)。x 軸滿足 y=0，y 軸滿足 x=0；兩者交於 (0,0)。軸外四象限由 x、y 的符號決定。 · mko-coordinate-plane
- mko_quadrant_signs · cited — x、y 都非零時，(+,+)、(−,+)、(−,−)、(+,−) 分別為第一、二、三、四象限；軸上的點不屬於任何象限。原點同時在兩軸。 · mko-coordinate-plane
- L_classify · lemma — 對每個 (x,y)∈ℝ²：若 x=0 或 y=0，它不在任何象限；若 x≠0 且 y≠0，它恰在一個象限中。





## 逐步主鏈

S01 · definition操作前

\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'

條件：無

規則：mko_coord_plane · 依賴：G1

葉節點依據：mko_coord_plane + cartesian_product_def

先固定座標系（G1），之後「點」就以實數有序對表示：第一坐標沿 x 軸讀取，第二坐標沿 y 軸讀取。依笛卡兒積的相等條件，兩點相同當且僅當兩個對應坐標分別相等；這是 MKO para2 所說的比較方式，而且只在同一座標系中有意義。



S02 · definition操作前

\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\}

條件：無

規則：def_intro · 依賴：G2, S01

葉節點依據：def_intro + mko_quadrant_signs + set_builder

依 MKO 寫出兩軸與四個象限的集合定義。注意象限用的是嚴格不等號：Q_I 要求 x>0 且 y>0，而不是 x≥0 且 y≥0；這正是軸上的點被排除在象限之外的原因。



S03 · implies操作前

(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})

條件：無

規則：L_classify · 依賴：S02, order_basics

葉節點依據：L_classify + order_basics + case_analysis

依引理 L_classify，平面上的每個點都被「兩軸的聯集」與四個象限恰好分類一次：軸上的點不在象限中，軸外的點恰在一個象限中。證明在 S03.1（軸上）、S03.2（軸外至少一個）、S03.3（至多一個）。



S04 · implies操作前

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

操作後

\{(0,0)\}

條件：無

規則：set_extensionality · 依賴：S02

葉節點依據：set_extensionality + set_operations_def

證明 MKO 的「兩軸交於 (0,0)」，而且只交於這一點。兩個方向的包含分別在 S04.1 與 S04.2。



S05 · implies操作前

A=(-3,2)

操作後

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

條件：-3<0; 2>0

規則：mko_quadrant_signs · 依賴：G3, S02, S03

葉節點依據：mko_quadrant_signs + order_basics + numeric_evaluation

A 的第一坐標 −3<0、第二坐標 2>0，符號為 (−,+)，符合 Q_II 的定義。因 −3≠0，A 不在 y 軸；因 2≠0，A 不在 x 軸。依 L_classify，A 不在其他象限。



S06 · implies操作前

B=(2,-3)

操作後

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

條件：2>0; -3<0

規則：mko_quadrant_signs · 依賴：G3, S02, S03

葉節點依據：mko_quadrant_signs + order_basics + numeric_evaluation

B 的第一坐標 2>0、第二坐標 −3<0，符號為 (+,−)，所以 B∈Q_IV。兩坐標都非零，所以 B 不在任何一軸上。



S07 · implies操作前

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

操作後

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

條件：無

規則：cartesian_product_def · 依賴：S01, S05, S06

葉節點依據：cartesian_product_def + set_extensionality + numeric_evaluation

有序對相等需要第一坐標相等，而 −3≠2，所以 A≠B。相反地，無序集合 {−3,2} 與 {2,−3} 有相同元素，依 set_extensionality 相等。交換坐標改變了點，甚至改變了象限（Q_II 變 Q_IV），所以點不能當成無序集合。



S08 · equivalent操作前

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

操作後

B'=(2,-3)=B

條件：無

規則：cartesian_product_def · 依賴：G3, S01, S06

葉節點依據：cartesian_product_def + numeric_evaluation + eq_replace

6/3=2 且 −3=−3，兩個對應坐標都相等，依有序對相等條件 B′=B，所以 B′ 也在 Q_IV。點是否相同由坐標值決定，不由寫法決定。



S09 · implies操作前

C=(0,-4)

操作後

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

條件：0=0; -4\neq 0

規則：L_classify · 依賴：G3, S02, S03

葉節點依據：L_classify + set_builder + numeric_evaluation

C 的第一坐標是 0，所以 C∈𝒴；第二坐標 −4≠0，所以 C∉𝒳。依 L_classify（x=0 的情形），C 不在任何象限，雖然它的第二坐標是負的。



S10 · implies操作前

O=(0,0)

操作後

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

條件：無

規則：L_classify · 依賴：G3, S03, S04

葉節點依據：L_classify + set_operations_def

由 S04，O 同時在兩軸上；由 L_classify（x=0），O 不在任何象限。原點是兩軸的唯一公共點，不是第一象限的「角」。



S11 · implies操作前

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

操作後

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

條件：-\tfrac12<0; -5<0

規則：mko_quadrant_signs · 依賴：G3, S02, S03

葉節點依據：mko_quadrant_signs + order_basics + numeric_evaluation

E 的兩坐標 −1/2<0、−5<0，符號為 (−,−)，所以 E∈Q_III。坐標不必是整數；只看符號。兩坐標都非零，E 不在軸上。



S12 · implies操作前

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

條件：無

規則：and_intro_elim · 依賴：S05, S06, S07, S08, S09, S10, S11

葉節點依據：and_intro_elim

把各點的判定合在一起：A 在第二象限，B 與 B′ 是同一點、在第四象限，E 在第三象限，C 在 y 軸上而不在 x 軸上，O 在兩軸上；C 與 O 都不在任何象限；A≠B。所有結論都只由坐標值與 S02 的定義推出。







## 局部子步與引理

S03.1 · implies操作前

x=0\ \lor\ y=0

操作後

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

條件：無

規則：order_basics · 依賴：S02, order_basics

葉節點依據：order_basics + set_operations_def

每個象限都要求 x>0 或 x<0，也都要求 y>0 或 y<0。依三一律，x=0 時 x>0 與 x<0 都不成立；y=0 時 y>0 與 y<0 都不成立。所以只要 x=0 或 y=0，四個象限的條件都不滿足，該點不在任何象限。



S03.2 · case_split操作前

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\neq 0; y\neq 0

規則：case_analysis · 依賴：S02, order_basics

葉節點依據：case_analysis + order_basics

依三一律，x≠0 時 x>0 或 x<0；y≠0 時 y>0 或 y<0。四種組合 (+,+)、(−,+)、(−,−)、(+,−) 涵蓋全部可能，分別恰是 Q_I、Q_II、Q_III、Q_IV 的定義條件，所以該點至少在一個象限中。



S03.3 · implies操作前

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

操作後

\bot

條件：無

規則：contradiction · 依賴：S02, order_basics

葉節點依據：contradiction + order_basics

任兩個不同象限對 x 或對 y 要求相反的符號：Q_I 與 Q_II、Q_III 與 Q_IV 在 x 上相反；Q_I 與 Q_IV、Q_II 與 Q_III 在 y 上相反；Q_I 與 Q_III、Q_II 與 Q_IV 兩者都相反。若一點同在兩個不同象限，就要同時有例如 x>0 與 x<0，違反三一律。所以至多在一個象限；配合 S03.2 得恰在一個。S03.1 至 S03.3 合起來證得引理 L_classify。



S04.1 · implies操作前

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

操作後

(x,y)=(0,0)

條件：無

規則：set_operations_def · 依賴：S02, set_operations_def

葉節點依據：set_operations_def + cartesian_product_def

(x,y)∈𝒳∩𝒴 表示 (x,y)∈𝒳 且 (x,y)∈𝒴，也就是 y=0 且 x=0；依有序對相等條件，(x,y)=(0,0)。



S04.2 · implies操作前

(0,0)

操作後

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

條件：無

規則：set_operations_def · 依賴：S02, S04.1

葉節點依據：set_builder + set_operations_def + set_extensionality

(0,0) 的第二坐標是 0，所以在 𝒳；第一坐標是 0，所以在 𝒴；因此在交集中。S04.1 與 S04.2 合起來，依 set_extensionality 得 𝒳∩𝒴={(0,0)}。







## 逐步反向審查


- S12 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S10, S11, and_intro_elim — 目標 G：各點的分類與兩個比較。足夠條件 H：S05 至 S11 的各別結論；H⇒G 只是合取。H 由坐標與定義正向證成，沒有把 G 當作前提。
- S11 · premise_audit · G3, S02, S03, mko_quadrant_signs — 只用坐標符號（N8、N9）。
- S10 · premise_audit · S03, S04, L_classify — 直接引用 S04 與引理，不需另外計算。
- S09 · premise_audit · S02, S03, L_classify — 需要象限定義中的嚴格不等號；C 不可被歸入第三或第四象限（N7）。
- S08 · inverse_equivalence · cartesian_product_def, numeric_evaluation — 6/3 與 2 是同一個有理數（N6），兩種寫法可雙向代換。
- S07 · premise_audit · S01, cartesian_product_def, set_extensionality — 一個坐標不同就足以推出兩點不同（N5）；反向（兩點不同推出某個指定坐標不同）不宣稱。
- S06 · premise_audit · G3, S02, S03, mko_quadrant_signs — 與 S05 相同，只用坐標符號（N3、N4）。
- S05 · premise_audit · G3, S02, S03, mko_quadrant_signs — 只需兩個坐標的符號（N1、N2）；判定不依賴任何圖。
- S04.2 · premise_audit · S04.1, set_extensionality, set_builder — 兩個方向都已證，集合相等成立。
- S04.1 · premise_audit · set_operations_def, cartesian_product_def — 只用交集與有序對的定義；反向包含在 S04.2。
- S04 · premise_audit · S02, set_extensionality — 集合相等需要兩個方向，在子步中分別證明。
- S03.3 · premise_audit · S02, order_basics, contradiction — 六對象限逐一檢查；每對都有一個坐標的符號相反，矛盾來自三一律。
- S03.2 · premise_audit · S02, order_basics, case_analysis — 分情況必須涵蓋全部可能：x、y 各兩種符號共四種，缺一不可。
- S03.1 · premise_audit · S02, order_basics, set_operations_def — 依賴象限定義中的嚴格不等號；若誤用 ≥，原點會同時落在四個「象限」中。
- S03 · premise_audit · L_classify, order_basics, S02 — 只依 S02 的定義與實數三一律；不涉及任何具體點。
- S02 · premise_audit · G2, def_intro, mko_quadrant_signs, set_builder — 此步只命名集合；嚴格不等號是定義的一部分，不能改成 ≥ 或 ≤。
- S01 · premise_audit · G1, mko_coord_plane, cartesian_product_def — 此步只固定表示方式，不推出新事實；若換了座標系，同一個點的坐標可能不同，所以後面的判定都限於 G1 的座標系。





## 錯誤控制與反例

軸上的點不在任何象限MKO 指出的第一個誤解是把軸上的點或原點列入象限。象限定義用嚴格不等號（S02），所以 C=(0,−4) 雖然第二坐標為負，仍不在第三或第四象限；原點也不是第一象限的點（S03.1、S09、S10）。

有序對不可交換MKO 指出的第二個誤解是把有序對當成無序集合。{−3,2}={2,−3}，但 (−3,2)≠(2,−3)：前者在第二象限，後者在第四象限（S07）。判定兩點是否相同要逐一比較對應坐標。

坐標是資料，不從圖上讀B′=(6/3,−3) 與 B 寫法不同卻是同一點（S08），而 E 的坐標 −1/2 在粗略的圖上可能看起來接近 y 軸。判定只依明示的坐標值與定義；本稿也不推論兩點距離或圖形大小（MKO 假設 a2）。


- 原點 (0,0) 在第一象限，因為它的兩個坐標都 ≥0 → reject — Q_I 要求 x>0 且 y>0；0>0 不成立，原點不在任何象限。
- (−3,2)=(2,−3)，因為兩者用的是同樣兩個數 → reject — 有序對相等需要第一坐標相等，−3≠2；兩點甚至在不同象限。
- C=(0,−4) 的第二坐標為負，所以 C 在第三或第四象限 → reject — 第三、第四象限都要求 x≠0（x<0 或 x>0），而 C 的 x=0，C 在 y 軸上。
- B′=(6/3,−3) 與 B=(2,−3) 寫法不同，所以是不同的點 → reject — 6/3=2，兩個對應坐標都相等，所以 B′=B。





## 結論與限制

兩軸只交於原點；每個點要嘛在軸上（不在任何象限），要嘛恰在一個象限。A=(−3,2)∈Q_II，B=(2,−3)=B′∈Q_IV，E=(−1/2,−5)∈Q_III，C=(0,−4) 在 y 軸上、不在任何象限，O 在兩軸上、不在任何象限；A≠B，雖然 {−3,2}={2,−3}。


- 點與實數有序對的對應（G1）是座標系的前提，本稿不由幾何公理推導它。
- 本稿不涉及距離、角度或圖形大小；這些需要另外的語義橋（MKO formal next）。





## 驗證及來源綁定

9 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-coordinate-plane-01.json)