set theory/ type theory/ Lean introductory essay

Stream: general

[James Palmer]

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

[Patrick Massot]

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

[Chris Wong]

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.

[Chris Wong]

(deleted)

[Chris Wong]

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

[Logan Murphy]

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.

[Anne Baanen]

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.

[Anne Baanen]

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.

[Anne Baanen]

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

[Anne Baanen]

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 α → α.

[Anne Baanen]

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

[James Palmer]

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

[Sebastien Gouezel]

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.

[Kevin Buzzard]

Hilbert was ;-)

[Kevin Buzzard]

I guess we know things he didn't know though

[Johan Commelin]

Sure, but a century has passed

[Sebastien Gouezel]

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

[Anne Baanen]

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.