soaproot
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
@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
@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).
Cantor-Bernstein implies Excluded Middle
We prove in constructive logic that the statement of the Cantor-Bernstein theorem implies excluded middle. This establishes that the Cantor-Bernstein theorem can only be proven assuming the full power of classical logic. The key ingredient is a theorem of Martín Escardó stating that quantification over a particular subset of the Cantor space $2^{\mathbb{N}}$, the so-called one-point compactification of $\mathbb{N}$, preserves decidable predicates.
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
soaproot (@[email protected])
@[email protected] What I have produced is largely at https://us.metamath.org/ileuni/mmil.html especially the sections "Different flavors of constructive mathematics", "A note on existence", and "How to intuitionize classical proofs". Haven't really pursued writing up any of it as a paper (for a variety of reasons).
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