@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.
A little thread on constructive mathematics and (tight) apartness relations in particular
@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).
@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).
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
@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.
@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.
@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
@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
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.
@andrejbauer Although the style of the post I'm replying to befits its publication date, it has inspired me to prove the following https://github.com/metamath/set.mm/pull/3114 which complements existing similar proofs for ordinal trichotomy, regularity, the axiom of choice, the subset of a finite set being finite, and others. #constructiveMathematics #metamath
@johncarlosbaez This is true on the learner side too: I really want to learn #constructiveMathematics and there are plenty of things I have grasped and even formalized in metamath, but when people talk about toposes and sheaves I still just hear "tweet, tweet, tweet". Hopefully will not be true forever, but I guess I can do some combination of (1) enjoying the things I have figured out (largely set theory and analysis; even number theory is more different without excluded middle than I expected), and (2) figuring I will never run out of things to explore.
@andrejbauer @MartinEscardo @kameryn Worse yet, "Dear editor, here is a paper about countable reals and I am not crazy and neither is the rest of the #constructiveMathematics community"
Why would you prove theorems in a computer-checkable format? Without one, if you publish a proof it takes highly skilled experts a year to figure out whether your proof is correct (if you are credible enough that they'll bother). With one, the computer is checking each step of the proof and the humans only need to compare what you prove with what you claim to have proved. I prove #constructiveMathematics at https://us.metamath.org/ileuni
Thread about #UnivalentCombinatorics, in the sense of @egbertrijke.
Usually people think of #ConstructiveMathematics as being more restrictive than #ClassicalMathematics.
In this thread, I want to give a concrete example illustrating that constructive mathematics is more general than classical mathematics.
1/
The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y.
Ohad Kammar gave a better proof.
Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable.
1/
#hott #univalentFoundations #constructiveMathematics
#neutralMathematics
