Intuitionistic maths

Stream: maths

[James Palmer]

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]

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]

"all function is continuous" is a metatheorem right

[Kenny Lau]

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

[Kenny Lau]

or is that actually a theorem

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

I think it has been formalized in Nuprl for example

[Mario Carneiro]

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

[Mario Carneiro]

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

[Anne Baanen]

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]

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]

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

[Patrick Massot]

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]

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]

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]

the baseline is just too high for meaningful axiom study

[Mario Carneiro]

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]

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

[James Palmer]

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