Zulip Chat Archive

Stream: general

Topic: set theory/ type theory/ Lean introductory essay


view this post on Zulip James Palmer (Aug 27 2020 at 12:52):

Hey guys,

for the Xena project I've been writing an essay targeted at enthusiastic high schoolers/ 1st year undergrads explaining the various foundational issues in mathematics, as well as introducing the power of Lean to people. Lean features in it quite briefly in places, but there is much discussion on what the future of Lean could be and how that will affect how mathematicians in general decide to practise maths.

I am posting it below in this message (upon Kevin's suggestion) and I would really appreciate (constructive - pun intended) feedback about how to potentially improve things :)

thank you very much!

Summer_Project_2020-3.pdf

view this post on Zulip Patrick Massot (Aug 27 2020 at 12:56):

Is "stop caring about constructive math" considered a constructive feedback?

view this post on Zulip Chris Wong (Aug 27 2020 at 13:49):

I think the introduction accurately describes what intuitionistic logic is, but not why it's useful—constructive proofs can be read as algorithms that compute their results. I see that point is hinted at later but I think it's worth making more prominent.

view this post on Zulip Chris Wong (Aug 27 2020 at 13:59):

(deleted)

view this post on Zulip Chris Wong (Aug 27 2020 at 14:07):

Also, I can imagine a beginner reading this

it is arrogant for us to assume that a mathematical statement can
only ever be true or false

and coming away thinking it's a ternary logic. Though my brain is fried at the moment so this might not be an issue at all

view this post on Zulip Logan Murphy (Aug 27 2020 at 19:01):

I've only read the first few sections but looks like a nice essay! I'll piggyback onto Chris's point, although I'm by no means an expert in the philosophy of foundations. I think that rather than using the statement

it is arrogant for us to assume that a mathematical statement can only ever be true or false

it might be more informative and interesting to mention the differences between intuitionistic and classical approaches to the ontology of mathematics. Classical mathematicians are generally Platonists, in that there is a mathematical reality outside of human cognition (if humans weren't around, mathematics would still exist). Intuitionists (if I understand them) think that mathematics only really exist as a construction of human cognition. The existence of a mathematical object can only be asserted by providing a method for its construction, so the LEM must be rejected since it would allow for an object to exist without a way to construct it. This also provides a nice way to introduce how intuitionistic logic is important computationally, since ``method of construction'' is just a synonym for algorithm.

Again, I'm not an expert, and this may not be the kind of discussion you want to include. This is just what I think of when I consider why e.g. LEM is excluded in intuitionism.

view this post on Zulip Anne Baanen (Aug 27 2020 at 21:18):

A bit more specifically, according to the Brouwer-style school of intuitionism I was taught (and which I believe in on even-numbered days), mathematics only really exists as a construction of my cognition. So a proof is an object in my mind, and perhaps I can put shapes on paper which cause a proof to appear in the mind of the reader (what formalists would call a proof), but that is nothing that the intuitionist needs to be concerned about to do mathematics. Conversely, any object in my mind can serve a role in mathematics. This leads to the concept of a free choice sequence: a sequence of values such that I pick each value as it's needed (and making use of everything I can think of at that point, not at the point I name the sequence). Requiring constructions is more a consequence of this philosophical postulate: something like ∀ i, s_i = 0 ∨ ∃ i, s_i ≠ 0 cannot hold for free choice sequences.

view this post on Zulip Anne Baanen (Aug 27 2020 at 21:39):

As an intuitionist, when I assert a statement P ∧ Q, I am correct only when I know a proof of P and a proof of Q, and to correctly assert P ∨ Q, I need to know which one of the two is true and know a proof for that alternative, etc.

view this post on Zulip Anne Baanen (Aug 27 2020 at 21:39):

With that in mind, I'd also like to suggest a change to the slogan "it is arrogant for us to assume that a mathematical statement can only ever be true or false": "it is arrogant for us to assume that for each mathematical statement, we know a proof or disproof" or "..., we can find a proof or a disproof eventually".

view this post on Zulip Anne Baanen (Aug 27 2020 at 22:12):

I skimmed across the rest of the essay and this caught my eye:

It is worth noting, however, that in Per Martin-Löf’s intuitionistic type theory, the axiom of choice is not an axiom for the fact that it is provable from the other axioms. [... I]n L.E.J Brouwer’s intuitionistic logic the axiom of choice is inconsistent with the rest of the axioms

I would say that the words "the axiom of choice" refer to two different statements in the two sentences. If we have an indexed family of inhabited sets, a choice function for this family is the same thing as a proof that each set is inhabited, in Martin-Löf type theory and in Brouwer's intuitionism (at least in the BHK interpretation). There is another axiom of choice that is equivalent for the classical mathematician but nonprovable in MLTT and false according to Brouwer: "If for each set X in a set of sets there is no function X → ∅, then there is a function from the set of sets sending X to an element x ∈ X.". This is the axiom added to Lean to get classical logic, as axiom classical.choice : Π {α : Sort u}, nonempty α → α.

view this post on Zulip Anne Baanen (Aug 27 2020 at 22:19):

Anyway, I'm very happy to see people being waken from their dogmatic slumber of vaguely Platonic classical maths, so I definitely like the essay :)

view this post on Zulip James Palmer (Aug 27 2020 at 23:00):

Thank you very much everyone who responded, I will make sure to tighten things up having looked through all these statements :)

view this post on Zulip Sebastien Gouezel (Aug 28 2020 at 07:47):

Anne Baanen said:

With that in mind, I'd also like to suggest a change to the slogan "it is arrogant for us to assume that a mathematical statement can only ever be true or false": "it is arrogant for us to assume that for each mathematical statement, we know a proof or disproof" or "..., we can find a proof or a disproof eventually".

I don't think the reformulation captures intuitionism, because it definitely makes sense in classical mathematics too: there are statements which are not decidable, so no one is arrogant enough to think there will be a proof or disproof of every statement, because this is just false.

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 07:49):

Hilbert was ;-)

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 07:49):

I guess we know things he didn't know though

view this post on Zulip Johan Commelin (Aug 28 2020 at 07:49):

Sure, but a century has passed

view this post on Zulip Sebastien Gouezel (Aug 28 2020 at 07:52):

I almost put (only Hilbert was ever that arrogant) in my message, but I decided to leave it for the first arrogant reader :-)

view this post on Zulip Anne Baanen (Aug 28 2020 at 10:09):

Sebastien Gouezel said:

I don't think the reformulation captures intuitionism, because it definitely makes sense in classical mathematics too: there are statements which are not decidable, so no one is arrogant enough to think there will be a proof or disproof of every statement, because this is just false.

Right, without mentioning the more restrictive notion of truth, the slogan makes sense in classical mathematics but doesn't tell a classical mathematician anything about the nature of true or false statements.


Last updated: May 11 2021 at 21:10 UTC