#constructiveMathematics

0 posts0 participants0 posts today

soaproot<a href="https://kolektiva.social/@jargoggles" class="u-url mention">@jargoggles</a> <a href="https://fosstodon.org/@spyro" class="u-url mention">@spyro</a> <a href="https://infosec.exchange/@juanan" class="u-url mention">@juanan</a> I'm trying to figure how to work in a <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> joke. Something about whether "this is taught at Harvard business school" is a decidable proposition.

soaproot<a href="https://mathstodon.xyz/@dpiponi" class="u-url mention">@dpiponi</a> I didn't really have a firm handle on this until I read <a href="https://us.metamath.org/mpeuni/df-if.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://us.metamath.org/mpeuni/df-if.html</a> . If working in <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> add the additional proviso that the proposition needs to be decidable.

soaproot<a href="https://kfogel.org/users/kfogel" class="u-url mention">@kfogel</a> Would you accept "real number" or "ordinal" in <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> ? Although I suppose that might be too technical of an example; your examples are quite good.

soaproot<a href="https://mastodon.murkworks.net/@wrog" class="u-url mention">@wrog</a> <a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention">@MartinEscardo</a> <a href="https://mathstodon.xyz/@VinceVatter" class="u-url mention">@VinceVatter</a> You can conclude A ⟹ B from ¬B ⟹ ¬A in <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> if you show that the proposition B is decidable, as seen at <a href="https://us.metamath.org/ileuni/condc.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://us.metamath.org/ileuni/condc.html</a> . 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).

soaproot<a href="https://mathstodon.xyz/@johncarlosbaez" class="u-url mention">@johncarlosbaez</a> <a href="https://mathstodon.xyz/@highergeometer" class="u-url mention">@highergeometer</a> The examples are familiar to much of the <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> crowd, see Theorem 1.2 of Bauer's Five Stages paper at <a href="http://dx.doi.org/10.1090/bull/1556" target="_blank" rel="nofollow noopener noreferrer" translate="no">http://dx.doi.org/10.1090/bull/1556</a> . But they are nicely presented here (I thought "really hard Gelfond–Schneider theorem" was a pleasant turn of phrase).

soaproot<a href="https://sauropods.win/@futurebird" class="u-url mention">@futurebird</a> 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 <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> (both of which feature continuity in a central way).

soaprootI 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 <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> , has still required me to adjust some of the proofs where we had been taking supremums.4/4

soaprootGiven excluded middle (or something similar), every inhabited, bounded-above set of real numbers has a supremum. We don't get that in <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> but what additional conditions can ensure we have a supremum?1/4

soaproot<a href="https://toot.community/@openculture" class="u-url mention">@openculture</a> Uh oh. Either I am bad at explaining <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> or it isn't a science (by this test anyway).

soaproot<a href="https://mathstodon.xyz/@DavidKButler" class="u-url mention">@DavidKButler</a> Oooh nice. Also easily adapted to <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> 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 <a href="https://mathstodon.xyz/@andrejbauer" class="u-url mention">@andrejbauer</a> 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.

soaproot<a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> 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 <a href="https://ncatlab.org/nlab/show/principle+of+omniscience" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://ncatlab.org/nlab/show/principle+of+omniscience</a> for further details).

soaproot<a href="https://mathstodon.xyz/@ColinTheMathmo" class="u-url mention">@ColinTheMathmo</a> Now you've done it. I've stated this in Metamath and am trying to prove it. Seems like it should still hold in <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> but it wasn't quite as easy as I thought.

soaproot<a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention">@MartinEscardo</a> Thanks for a fun exercise in <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> ! 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 <a href="https://us.metamath.org/ileuni/pwle2.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://us.metamath.org/ileuni/pwle2.html</a> and <a href="https://us.metamath.org/ileuni/pwf1oexmid.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://us.metamath.org/ileuni/pwf1oexmid.html</a> and discussion is at <a href="https://github.com/metamath/set.mm/issues/3456" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://github.com/metamath/set.mm/issues/3456</a>

soaproot<a href="https://mathstodon.xyz/@andrejbauer" class="u-url mention">@andrejbauer</a> I try to tag most of my relevant posts with <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> but I seem to have forgotten for my post about proving a bijection between the rationals and the natural numbers: <a href="https://sfba.social/@soaproot/110914052615158608" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://sfba.social/@soaproot/110914052615158608</a>

soaprootIn <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> 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.

soaprootGiven excluded middle, AB = 0 → A = 0 or B = 0Without 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 <a href="https://us.metamath.org/ileuni/mulap0.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://us.metamath.org/ileuni/mulap0.html</a> , <a href="https://us.metamath.org/ileuni/mul0eqap.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://us.metamath.org/ileuni/mul0eqap.html</a> and <a href="https://us.metamath.org/ileuni/mul0inf.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://us.metamath.org/ileuni/mul0inf.html</a> . Also see <a href="https://mathoverflow.net/questions/403980/how-do-working-constructivists-get-by-with-out-the-zero-product-property/404116#404116" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://mathoverflow.net/questions/403980/how-do-working-constructivists-get-by-with-out-the-zero-product-property/404116#404116</a> which lists these.<a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a>

soaproot<a href="https://tech.lgbt/@CriticalCupcake" class="u-url mention">@CriticalCupcake</a> Am I the only one who read this as "three is omniscient"? <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a>

soaprootHow 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 <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> ? 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!

soaprootThe 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 <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a> . 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. <a href="https://mathstodon.xyz/@andrejbauer" class="u-url mention">@andrejbauer</a> has an argument from the effective topos at <a href="https://mathstodon.xyz/@andrejbauer/110711674689169554" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://mathstodon.xyz/@andrejbauer/110711674689169554</a> and <a href="https://us.metamath.org/ileuni/sbthom.html" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://us.metamath.org/ileuni/sbthom.html</a> relies on LPO being weaker than excluded middle.

soaproot<a href="https://mathstodon.xyz/@highergeometer" class="u-url mention">@highergeometer</a> <a href="https://mathstodon.xyz/@11011110" class="u-url mention">@11011110</a> Sure, but I guess I'm willing to be a bit less strict about who is a set theorist. I thought about that diagram a lot when I was trying to figure out, of the set difference theorems which hold in ZFC, which ones hold in IZF too. (Spoiler alert) a whole bunch do not. <a href="https://sfba.social/tags/constructiveMathematics" class="mention hashtag" rel="tag">#constructiveMathematics</a>

Recent searches

Search options

Administered by:

Server stats:

#constructivemathematics