Replied in thread
@jargoggles @spyro @juanan I'm trying to figure how to work in a #constructiveMathematics joke. Something about whether "this is taught at Harvard business school" is a decidable proposition.
#constructivemathematics
0 posts0 participants0 posts today
Replied in thread
@dpiponi I didn't really have a firm handle on this until I read https://us.metamath.org/mpeuni/df-if.html . If working in #constructiveMathematics add the additional proviso that the proposition needs to be decidable.
us.metamath.orgdf-if - Metamath Proof Explorer
A little thread on constructive mathematics and (tight) apartness relations in particular
Replied in thread
@kfogel Would you accept "real number" or "ordinal" in #constructiveMathematics ? Although I suppose that might be too technical of an example; your examples are quite good.
Replied in thread
@wrog @MartinEscardo @VinceVatter You can conclude A ⟹ B from ¬B ⟹ ¬A in #constructiveMathematics if you show that the proposition B is decidable, as seen at https://us.metamath.org/ileuni/condc.html . Examples of decidable propositions are "n is even" (where n is a natural number), "n = m" (where n and m are natural numbers), or "n is prime" (where n is a natural number). (The application of this to the original post here is a bit unclear to me for reasons discussed in other replies).
us.metamath.orgcondc - Intuitionistic Logic Explorer
Replied in thread
@johncarlosbaez @highergeometer The examples are familiar to much of the #constructiveMathematics crowd, see Theorem 1.2 of Bauer's Five Stages paper at http://dx.doi.org/10.1090/bull/1556 . But they are nicely presented here (I thought "really hard Gelfond–Schneider theorem" was a pleasant turn of phrase).
Replied in thread
@futurebird Those who know more mathematics than me assure me that continuity is indeed very rich. This has been especially true as I've learned about topology and #constructiveMathematics (both of which feature continuity in a central way).
Continued thread
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
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
Replied in thread
@openculture Uh oh. Either I am bad at explaining #constructiveMathematics or it isn't a science (by this test anyway).
Replied in thread
@DavidKButler Oooh nice. Also easily adapted to #constructiveMathematics as follows. The first and third work as you stated. The second one is the one which doesn't, but a modified variation of it does:
When you prove the statement “If A, then not B” by contradiction (what @andrejbauer calls "proof of negation"), your proof usually goes like this:
Suppose A.
Suppose B.
[insert arguments here]
C
But already, not C.
Contradiction!
Therefore not B.
#constructiveMathematics is math without excluded middle (also known as the principle of omniscience). What lies between excluded middle and no omniscience? In terms of real numbers:
* analytic LPO: ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)
* analytic WLPO: ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ ( 𝑥 = 𝑦 ∨ ¬ x = y )
* analytic MP: ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ ( ¬ x = y → (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))
* analytic LLPO: ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ ( ¬ x < y ∨ ¬ y < x )
(there are non-analytic versions too - see https://ncatlab.org/nlab/show/principle+of+omniscience for further details).
Replied in thread
@ColinTheMathmo Now you've done it. I've stated this in Metamath and am trying to prove it. Seems like it should still hold in #constructiveMathematics but it wasn't quite as easy as I thought.
Replied in thread
@MartinEscardo Thanks for a fun exercise in #constructiveMathematics ! At first we thought "oh the second one is easy we already have EXMID 
𝒫 1o ≈ 2o" but that's just one part, the other part basically asks if there can be a truth value other than true or false (there cannot). Our IZF solution is at https://us.metamath.org/ileuni/pwle2.html and https://us.metamath.org/ileuni/pwf1oexmid.html and discussion is at https://github.com/metamath/set.mm/issues/3456
us.metamath.orgpwle2 - Mathbox for Jim Kingdon
Replied in thread
@andrejbauer I try to tag most of my relevant posts with #constructiveMathematics but I seem to have forgotten for my post about proving a bijection between the rationals and the natural numbers: https://sfba.social/@soaproot/110914052615158608
SFBA.socialsoaproot (@soaproot@sfba.social)I am pleased to report the successful formalization of the equinumerosity of the rationals and the natural numbers in Metamath's (constructive) iset.mm.
We:
* proved ℕ × ℕ ≈ ℕ by decomposing into a power of two and an odd divisor
* defined omniscient sets
* defined disjoint unions
* proved two impossibility proofs about the Schroeder-Bernstein theorem: the full theorem (formalizing a 2019 paper) and a special case (we have an impossibility proof of the special case but just how strong it is appears to be an open problem),
* countable set theorems
Many thanks to my collaborators, especially Mario Carneiro, Thierry Arnoux, and Benoit Jubin. I never could have done something like this by myself.
Also a special acknowledgement to Peter Aczel who with a coauthor wrote the textbook containing the key lemma for this proof. He died on August 1, 2023 and will be missed according to all the tributes I read on Mastodon.
See a version of this post at https://github.com/metamath/set.mm/issues/2595#issuecomment-1684607410 with links and a few more words.
In #constructiveMathematics we cannot prove real number trichotomy, 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 . Does that mean there is a pair of real numbers where none of those hold (that is, where we can refute each of those three relationships)? Actually, no. We can prove ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴) from constructive theorems like 𝐴 ≤ 𝐵 ¬ 𝐵 < 𝐴 and 𝐴 = 𝐵 (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴) . This is another example of distinguishing between being unable to prove something, or being able to refute it.
Given excluded middle, AB = 0 → A = 0 or B = 0
Without excluded middle, what can we say?
1. A # 0 and B # 0 → AB # 0 (where # is apartness)
2. A # B and AB = 0 → A = 0 or B = 0
3. AB = 0 iff inf { |A| , |B| } = 0 (where inf is infimum)
These are formalized in metamath's iset.mm as https://us.metamath.org/ileuni/mulap0.html , https://us.metamath.org/ileuni/mul0eqap.html and https://us.metamath.org/ileuni/mul0inf.html . Also see https://mathoverflow.net/questions/403980/how-do-working-constructivists-get-by-with-out-the-zero-product-property/404116#404116 which lists these.
us.metamath.orgmulap0 - Intuitionistic Logic Explorer
Replied in thread
@CriticalCupcake Am I the only one who read this as "three is omniscient"? #constructiveMathematics
How do you establish a bijection between a set and the natural numbers? With excluded middle you might reach for the Schröder–Bernstein theorem but what about in #constructiveMathematics ? If you know some of the theorems about countability you'd think of a surjection from the natural numbers onto your set. And then you say that surjection needs to, for any initial segment, have an element (beyond that segment) not contained in the segment. Voila!
The Schroeder-Bernstein theorem says given injections A → B and B → A then there is a bijection between A and B. This is a theorem in Zermelo-Fraenkel set theory but fails in #constructiveMathematics . What about weakened forms? If A and B are finite we can prove it. What if A is the set of natural numbers and B is any set? This fails too. @andrejbauer has an argument from the effective topos at https://mathstodon.xyz/@andrejbauer/110711674689169554 and https://us.metamath.org/ileuni/sbthom.html relies on LPO being weaker than excluded middle.
MathstodonAndrej Bauer (@andrejbauer@mathstodon.xyz)@soaproot@sfba.social The effective topos shows that this fails. Let K ⊆ ℕ be the halting set and A = {2 n | n ∈ ℕ} ∪ {2 n + 1 | n ∉ K}. Clearly there are injections A → ℕ and ℕ → A. If there were a bijection ℕ → A then there would also have a surjection ℕ → (ℕ \ K), but this is impossible in the effective topos because ℕ \ K is not computably enumerable.