Ancestors

Toot

Written by soaproot on 2024-10-13 at 04:11

Given excluded middle (or something similar), every inhabited, bounded-above set of real numbers has a supremum. We don't get that in #constructiveMathematics but what additional conditions can ensure we have a supremum?

1/4

=> More informations about this toot | More toots from soaproot@sfba.social

Descendants

Written by soaproot on 2024-10-13 at 04:12

One condition which suffices is that set is located. That is, given real numbers x and y with x < y , either there is an element of the set greater than x, y is an upper bound for the set. (formalized as https://us.metamath.org/ileuni/axsuploc.html in metamath)

2/4

=> More informations about this toot | More toots from soaproot@sfba.social

Written by soaproot on 2024-10-13 at 04:26

Another condition which suffices is that it is a set of integers which is decidable. We can state decidable a few ways, but the one I've been using lately is that a set of integers 𝐴 is decidable iff ∀𝑥 ∈ ℤ ( 𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐴 ) . Sets of integers (many of which are quite easy to show are decidable) come up in number theory, I think items 10 and 23 at https://us.metamath.org/mm_100.html may be examples (although I have at least one example, probably better, which hasn't made it to the website quite yet).

3/4

=> More informations about this toot | More toots from soaproot@sfba.social

Written by soaproot on 2024-10-13 at 04:32

I realize that depending on your mathematical background this is either obvious and elementary, or impenetrable and unfamiliar. It's OK! But I did want to try to explain what I have been proving lately in Metamath. Hope this gives some idea of how number theory, which doesn't generally change a huge amount in #constructiveMathematics , has still required me to adjust some of the proofs where we had been taking supremums.

4/4

=> More informations about this toot | More toots from soaproot@sfba.social

Written by Andrej Bauer on 2024-10-13 at 08:46

@soaproot Bishop's definition of a supremum of a set of reals is not just the usual order-theoretic "least upper bound", but it's got some sort of locatedness built in, if I remember correctly. Perhaps like this: 𝑥 is the supremum of 𝑆 ⊆ ℝ if it is an upper bound, and for every 𝑦 < 𝑥 there is 𝑧 ∈ 𝑆 such that 𝑦 ≤ 𝑧.

Another point worth mentioning is that we can complete ℚ to a set of reals by suprema of all bounded inhabited sets. This is knowns as the McNeille completion, and it's larger than the completion by Dedekind cuts. Then we do get the usual strong completeness "every bounded inhabited set has a supremum", but we lack other desirable properties (in particular that 0 < 𝑥 ∨ 𝑥 < 1, and that the resulting structure is a field).

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Written by soaproot on 2024-10-13 at 13:32

@andrejbauer Ah yes, good point on definitions. I've been working with the definition that the supremum x of a set S ⊆ ℝ, if it exists, is an upper bound (for every y ∈ S y ≤ x) such that ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ S 𝑦 < 𝑧)). To be honest I don't know why Metamath chose this definition but it was well before any of us were doing anything constructively, so I imagine it was taken from a non-constructive analysis text (in this case, the source isn't cited).

=> More informations about this toot | More toots from soaproot@sfba.social

Written by Andrej Bauer on 2024-10-13 at 15:22

@soaproot Well, that's Bishop's definition of supremum. It allows you to show that the set gets arbitrarily close to its supremum, which of course can be quite useful. With the standard definition (least upper bound), you can only show that the set isn't bounded away from its supremum, so weirdness ensues.

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Written by soaproot on 2024-10-13 at 14:03

@andrejbauer Everything I have been posting/proving is for the reals defined via constructive Dedekind cuts (as defined in the HoTT book and various similar sources). The McNeille reals are worth a mention in the context of supremum properties, but I haven't formalized anything with McNeille reals, I guess because of the noted tradeoffs.

=> More informations about this toot | More toots from soaproot@sfba.social