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.

#constructiveMathematics

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

@highergeometer @11011110 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. #constructiveMathematics

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

@benleis Do you want to hear more about me formalizing #constructiveMathematics in metamath? Latest has been trying to get topology going. And yes, I've heard about locales and compactness of [0,1] and other things but I'm starting with more elementary questions like open set theorems. The discrete topology just worked but the indiscrete topology will need a new definition as described at https://github.com/metamath/set.mm/issues/3089

@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

I realize that natural language and mathematics are two different things but I enjoyed this sign from the point of view of Excluded Middle #constructiveMathematics

It is time for my regularly scheduled praise for @andrejbauer 's "Five stages of accepting constructive mathematics"[1]

Why? Because a collaborator of mine just asked the age-old question of how you prove that there exist irrational numbers 𝑎 and 𝑏 such that (𝑎↑𝑏) is rational, without excluded middle..

Bauer explains this wonderfully in the paper so at https://github.com/metamath/set.mm/issues/2958 I could just cite it.

#constructiveMathematics

[1] free download at https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/

@MartinEscardo thank you for your pinned thread about #ConstructiveMathematics ! this reminded me of papers I perused while researching Hilbert's philosophical progression and the impact of his work post-Gödel (which... makes sense) - while my math isn't up to snuff to follow all of your examples, it kindled a spark to revisit a few papers I'd set aside for when I'd studied a bit more

Oh and please boost the post at the top of this thread if you think people would be interested. I'm not sure how many math-interested people follow the #metamath or #constructiveMathematics tags.

I proved the ratio test for IZF in #metamath ! I knew this would be different in #constructiveMathematics because of the need to show how fast the series converges, but on the whole once I proved a basic convergence theorem based on a fixed rate of convergence, I have found that a lot of our convergence results work just like they did with excluded middle. (will put links in a reply to this message).

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/