#constructivemathematics — Public Fediverse posts

@mc I have no idea whether it will blow your mind or not, and it is in the area of learning/explanation rather than research, but in the process of formalizing several theorems [1] I got enough insight into set size in #constructiveMathematics to write the table on set size at https://us.metamath.org/ileuni/mmil.html#set-size and the thread on finite sets at https://sfba.social/@soaproot/116993765790369897

[1] especially https://us.metamath.org/ileuni/qnnen.html , https://us.metamath.org/ileuni/konigsberg.html , and https://us.metamath.org/ileuni/ballotfi.html

@jonmsterling @dpiponi @rg9119 My own experience is trying to make topology work in #constructiveMathematics. Using fairly conventional (same as classical) definitions for point set topology, I find open sets generally work but almost anything with closed sets wants to use excluded middle. I'm told I need to learn point free topology (locales) but I haven't yet gotten around to it or done enough with topology to make it unavoidable.

I'm going to write a mini-thread on finite sets in #constructiveMathematics (mostly to pass along some intuition that a friend who is new to this material shared with me). Classical intuition works poorly on constructive finite sets, but once you adapt your intuition, constructive finite sets lose their paradoxical quality.

I'll go from definitions and theorems to intuition, so if you just want the intuition, skip to the end.

1/7

@constantine I thought James Hanson and Andrej Bauer won it (with their countable reals paper), but perhaps that is a #constructiveMathematics pilled way to look at it.

@MartinEscardo Does that mean if I have developed (at least to a certain extent) an intuition about #constructiveMathematics that I can use that to better learn topology?

@ibrahimtencer Heh, as I was learning #constructiveMathematics I tried to prove a lot of things which can be proved with excluded middle but where I didn't know whether I could or not without it. Some turned out to be provable, some I could show implied a taboo.

Whether this was a good learning technique I'm not too sure.

@sliminality When people told me this holds for real numbers in #constructiveMathematics (in fact is often the definition of ≤), I didn't believe them at first. But not only did my collaborators tell me this was a good definition and I read it in the HoTT Book, but I also found it allowed me to prove the expected theorems about ≤

@iblech Oooh very nice way to state the concept; the proof is also pleasantly direct. As @MartinEscardo is always reminding us, #constructiveMathematics tends to work best when we state a result positively and in this case doing so enables us to not have to worry about not-equal versus apart in stating the result.

In Metamath notation: 𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))) . Proof at https://github.com/metamath/set.mm/pull/5275

cc @antoinechambertloir @ColinTheMathmo

The smallest positive real whose cosine is one is two times the smallest positive real whose sine is zero. Proved from axioms of IZF set theory via constructing reals, convergence and notation for infinite series, the exponential function, continuity, and the monotone intermediate value theorem. https://us.metamath.org/ileuni/taupi.html #PiDay #HalfTauDay #HalfTau #constructiveMathematics

@MartinEscardo @ncf Sure #constructiveMathematics has been saying inhabited for (our equivalent of) nonempty. But as for the original post, is there an alternative to "is not free in"? It isn't "bound" because I'm wanting to include the case where the variable does not appear at all. (Context is https://us.metamath.org/ileuni/df-nf.html and other parts of Metamath which use this notation)

@paysmaths @Theoremoftheday Very nice. One additional thing to say about this theorem: in #constructiveMathematics the Cantor–Bernstein–Schröder Theorem is equivalent to the law of the excluded middle (see https://arxiv.org/abs/1904.09193 or formalizations in, at least, TypeTopology or Metamath).

I said I'd also talk about one sided versus two sided Dedekind cuts. My own work has been with two sided Dedekind cuts and indeed orthodoxy in #constructiveMathematics is that these are the ones which are well defined. But I did find there is a one sided definition, due to James E Hanson, which apparently works. I'll just refer to https://mathoverflow.net/a/495508/489586 for further details (which are not as simple as the classical one sided cut).

7/8

This is a 🧵 about the Dedekind cut construction of real numbers in #constructiveMathematics , particularly two technical details. The first has to do with defining additive inverse and multiplication, when we can't use excluded middle for things like "is a real number positive or not?". The second is about one sided versus two sided cuts.

1/8

@ddrake @inthehands Also, in the case of #constructiveMathematics , section 11.6 of the HoTT book is about the surreal numbers including what is different if you develop them without excluded middle. (I realize it sounds like I'm surrealsplaining but think of my posts as being aimed at me as much as you - if I decide to do more with the surreals some day that is).

@RefurioAnachro Ooh nice. I mostly haven't written my #constructiveMathematics in blog post form but I have written some pages described at https://sfba.social/@soaproot/115374218852029139

I've posted about this a few times but let me try to do so more clearly. How do we, in #constructiveMathematics , show that a set is countably infinite (that is, there is a bijection between our set and the set of natural numbers)? There's a theorem for this which is elegant and also handles some of the trickier cases such as showing that the set of rational numbers is countably infinite. 1/n

I'm writing about nonincreasing sequences of zeroes and ones. So you could have all zeroes, all ones, a one followed by zeroes, two ones followed by zeroes, etc. (Here a sequence is a function from ω, the set of natural numbers, to { 0 , 1 }). How many such sequences are there? #constructiveMathematics
1/n

@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.

@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

#logic #math #constructiveMathematics

@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.

@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).

@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

@openculture Uh oh. Either I am bad at explaining #constructiveMathematics or it isn't a science (by this test anyway).

@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).

@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.