Zulip Chat Archive

Stream: maths

Topic: Intuitionistic maths


view this post on Zulip James Palmer (Aug 17 2020 at 15:44):

Hi everyone, does anyone know if much has been done to develop intuitionistic maths in Lean? I was specificialy wondering whether a proof of discontinuous functions not existing was available?

view this post on Zulip Floris van Doorn (Aug 17 2020 at 15:52):

In mathlib we have only developed mathematics that is compatible with classical mathematics (and mostly classical mathematics itself). There is nothing to prevent you from adding your intuistionistic axioms to Lean, and not using the classical ones. You can check that you have not used classical axioms by writing #print axioms my_theorem.

view this post on Zulip Kenny Lau (Aug 17 2020 at 15:53):

"all function is continuous" is a metatheorem right

view this post on Zulip Kenny Lau (Aug 17 2020 at 15:53):

also your phrasing "discontinuous functions not existing" is a bit... ironic lol

view this post on Zulip Kenny Lau (Aug 17 2020 at 15:54):

or is that actually a theorem

view this post on Zulip Reid Barton (Aug 17 2020 at 15:56):

It's a theorem in Brouwer-style intuitionistic mathematics, which is constructive mathematics plus some anti-classical axioms

view this post on Zulip Mario Carneiro (Aug 17 2020 at 15:56):

The approach Floris mentioned, using lean's actual axioms, is not really useful for investigations of the meta-properties of intuitionistic proofs

view this post on Zulip Reid Barton (Aug 17 2020 at 15:56):

I think it has been formalized in Nuprl for example

view this post on Zulip Mario Carneiro (Aug 17 2020 at 15:57):

To do that properly you should formalize the model theory of intuitionistic logic

view this post on Zulip Mario Carneiro (Aug 17 2020 at 15:58):

which, incidentally, does not require the metatheory (that is, lean) to be anticlassical

view this post on Zulip Anne Baanen (Aug 17 2020 at 15:59):

Kenny Lau said:

also your phrasing "discontinuous functions not existing" is a bit... ironic lol

@[simp] theorem not_exists : (¬  x, p x)   x, ¬ p x :=
exists_imp_distrib

#print axioms not_exists -- no axioms

view this post on Zulip Anne Baanen (Aug 17 2020 at 16:01):

Classical mathematicians generally know what they're doing. It's when they turn "I can't prove it doesn't exist" into "I know it exists" that everything starts to go wrong :upside_down:

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:02):

Isn't it more like "I can prove it's not possible for it not to exist"

view this post on Zulip Patrick Massot (Aug 17 2020 at 16:31):

I obviously think we shouldn't have different corners of mathlib using incompatible axioms. You should start a new library with anti-classical axioms, maybe call it non-math_lib.

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:32):

If you are explicitly studying logic, axiom removal in lean isn't nearly good enough, but you can do deep embeddings just fine

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:34):

The only people who are satisfied with no-axioms lean are those who study CIC and maybe HoTT, and even these people are unhappy with some of the things that lean gives them that they don't want, like definitional proof irrelevance

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:34):

the baseline is just too high for meaningful axiom study

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:36):

So far, mathlib has developed with zero new axioms beyond what core lean gives us, and I think we should keep it that way. #print axioms hasn't got a lot of love, and people aren't used to checking it, so adding an anticlassical axiom into mathlib would be a disaster

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:37):

It would be nice if the docs page listed print axioms results though

view this post on Zulip James Palmer (Aug 17 2020 at 16:39):

thanks everyone for the help! And sorry for my dodgy wording...


Last updated: May 10 2021 at 07:15 UTC