## Stream: maths

### Topic: Intuitionistic maths

#### 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?

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

#### Kenny Lau (Aug 17 2020 at 15:53):

"all function is continuous" is a metatheorem right

#### Kenny Lau (Aug 17 2020 at 15:53):

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

#### Kenny Lau (Aug 17 2020 at 15:54):

or is that actually a theorem

#### 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

#### 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

#### Reid Barton (Aug 17 2020 at 15:56):

I think it has been formalized in Nuprl for example

#### Mario Carneiro (Aug 17 2020 at 15:57):

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

#### Mario Carneiro (Aug 17 2020 at 15:58):

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

#### 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


#### 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:

#### 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"

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

#### 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

#### 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

#### Mario Carneiro (Aug 17 2020 at 16:34):

the baseline is just too high for meaningful axiom study

#### 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

#### Mario Carneiro (Aug 17 2020 at 16:37):

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

#### 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