Mistake in definition of order on rationals

[pglutz]

https://github.com/OpenLogicProject/OpenLogic/blob/abc1f3d213dcc47aaf2bc3add61c454b2ef368fc/content/sets-functions-relations/arithmetization/rationals.tex#L53

I believe the definition of the ordering on the rationals in the text is incorrect. The text uses pairs of integers (the second of which is required to be nonzero) to represent rationals and formally defines the rationals as a quotient of the set of such pairs of integers. The ordering is then defined by declaring [a, b]~ \leq [c, d]~ whenever ad \leq bc. However, since b and d are allowed to be negative, this does not work---it is not invariant under the equivalence relation ~ and it does not define a total order. As an example of what goes wrong, suppose a = 1, b = -1, c = -2, d = 1. Then ad = 1 and bc = 2 so ad < bc but we should not have [a, b]~ \leq [c, d]~. The definition should be amended to require that b and d be positive. This probably requires adding at least a bit of explanatory text since "positive" has not been defined (though it could be defined easily) and perhaps to explain why every equivalence class contains a pair whose second element is positive.

[rzach]

This seems right to me; @timbutton ?

[timbutton]

@rzach yes, this needs fixing, and I appreciate @pglutz's suggestion as to how. I am frantic with admin tasks for the next two weeks, so won't be able to fix it for a little while. @rzach, feel free to fix it if you like; otherwise, I'll get to it in mid-February.

[rzach]

Is the proposal to change the definition of ℚ to be equivalence classes of pairs [a,b] where a, b ∈ ℤ but b is positive? I wonder if an easier (ie, more local) fix would be to leave the definition of ℚ the same and just redefine ≤ on ℚ as

[a,b] ≤ [c,d] iff [c,d] - [a,b] ~ [e_ℤ,f_ℤ] for some e ∈ ℕ, 0 ≠ f ∈ ℕ

(that is, p ≤ q iff q-p is not negative). I think nothing else has to be changed since the verification that ℚ is an ordered field is left as an exercise. I don't know if that exercise would be harder with this definition of ≤ (where only the verification of the order properties would change) or @pglutz 's (where all the field properties would change).

[pglutz]

@rzach I think you misunderstood the fix I suggested but your fix is probably better than what I had in mind anyway.

In case you're curious, the fix I had in mind was to leave the definition of Q the same but change the definition of the order to:

[a, b] \leq [c, d] iff for some [a', b'] ~ [a, b] and some [c', d'] ~ [c, d] we have b' > 0, d' > 0 and a'd' \leq c'b'.

This does not require changing the definition of Q but it is more of a mouthful and to show it defines an order requires justifying why every ~ equivalence class [a, b]_~ contains an element [a', b'] such that b' > 0.

Your fix is nice because it seems a bit cleaner and less ad-hoc.

[timbutton]

This seems great to me. Does the 0 need a "naturals" subscript? Can't recall and only have my phone!

On Thu, 27 Jan 2022, 02:10 Richard Zach, @.***> wrote:

Is the proposal to change the definition of ℚ to be equivalence classes of pairs [a,b] where a, b ∈ ℤ but b is positive? I wonder if an easier (ie, more local) fix would be to leave the definition of ℚ the same and just redefine ≤ on ℚ as

[a,b] ≤ [c,d] iff [c,d] - [a,b] ~ [e_ℤ,f_ℤ] for some e ∈ ℕ, 0 ≠ f ∈ ℕ

(that is, p ≤ q iff q-p is not negative). I think nothing else has to be changed since the verification that ℚ is an ordered field is left as an exercise. I don't know if that exercise would be harder with this definition of ≤ (where only the verification of the order properties would change) or @pglutz https://github.com/pglutz 's (where all the field properties would change).

— Reply to this email directly, view it on GitHub https://github.com/OpenLogicProject/OpenLogic/issues/296#issuecomment-1022778210, or unsubscribe https://github.com/notifications/unsubscribe-auth/AM5CQB7TYXA7ZK6WH4ANRS3UYCSRPANCNFSM5MZQ4ZVA . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you were mentioned.Message ID: @.***>