Stream: maths

Topic: Wiedijk's "Benchmark"

Kevin Buzzard (Apr 03 2020 at 23:05):

In his 2007 paper "The QED Manifesto revisited" @Freek Wiedijk complains about how no prover at that time was suitable for formalising all of mathematics. I've said to Freek several times that I think Lean is a better candidate but he still moans about it for reasons I don't really understand. However one can look at the issues he raises which he says have not been solved, and then ask whether Lean solves them. For example he complains on p4 of the manuscript that none of the projects that existed at that time "have solved the difficult problem of how to integrate work by multiple people into a nice coherent whole". I think mathlib and github have solved that problem better than any of the systems he is talking about. He also highlights four mathematical statements and complains on the same page that none of the systems can "express all four statements in a good way". Statements are attached:

How are we doing with that one? (2) and (3) I am completely happy that we can express naturally. How about (1) and (4)?

Bhavik Mehta (Apr 04 2020 at 01:40):

I want to say that (4) might be nicely expressible using the framework in the flypitch project: we could write the first-order logic sentence (in the language of set theory) expressing "2^{\aleph_0} = \aleph_2", and then just write essentially {ZFC + PFA} ⊢' that sentence

Reid Barton (Apr 04 2020 at 01:56):

I think the challenge in 4 is just to state the axiom PFA at all. I couldn't find a description of it that I could understand.

Reid Barton (Apr 04 2020 at 01:59):

We definitely can already formulate the conclusion $2^{\aleph_0} = \aleph_2$--it seems this is what the author was mainly concerned about.

Reid Barton (Apr 04 2020 at 02:03):

It's

import set_theory.ordinal

open cardinal

#check ((2 : cardinal.{0}) ^ omega.{0} = aleph 2)


Reid Barton (Apr 04 2020 at 02:04):

I was hoping PFA was some obscure statement about infinite combinatorics but it seems to really be an obscure statement about set-theoretic forcing

Reid Barton (Apr 04 2020 at 02:06):

or more precisely, it involves quantifying over all the formulas of the language of set theory

Bhavik Mehta (Apr 04 2020 at 03:02):

I don't see the difficulty there - once we have the basic definitions of forcing at least. Defining a stationary subset (see eg Def 8.1 of Jech Set Theory) of a regular uncountable cardinal is easy (and defining a regular uncountable cardinal should be easy if it's not already done), then given a forcing P we can define the generic model - from here we can easily define what a proper forcing is (I'm using Def 31.1 of Jech), and then PFA is easy (density and such are one liners). In particular I don't think we ever need to quantify over all formulas in the language of set theory, this is the sort of thing the forcing theorem and generic model theorem should fix nicely

Bhavik Mehta (Apr 04 2020 at 03:02):

I might be missing some subtlety though

Reid Barton (Apr 04 2020 at 03:04):

The difficulty is I don't know what forcing is.

Reid Barton (Apr 04 2020 at 03:05):

Wait, maybe not. Maybe you found a different formulation of the axiom than the ones I found.

Bhavik Mehta (Apr 04 2020 at 03:25):

I'm using the one on wikipedia and the one in Jech Set Theory

Patrick Stevens (Apr 04 2020 at 09:04):

Reid Barton said:

The difficulty is I don't know what forcing is.

I should warn you that forcing is an unsolved problem in exposition - although the best I've read so far is https://arxiv.org/abs/0712.1320

Bhavik Mehta (Apr 04 2020 at 13:30):

In any case, hasn't the flypitch project shown that lean can definitely define cohen forcing

Kevin Buzzard (Apr 04 2020 at 13:53):

Maybe but I doubt it can be used to say anything about the cardinals in data.cardinal

Kevin Buzzard (Apr 04 2020 at 13:54):

(or wherever they are, sorry)

Bhavik Mehta (Apr 04 2020 at 13:55):

Yeah I agree with that, I think the sensible way to formulate (4) would be defining cardinals in the language of set theory using the definitions from flypitch rather than set_theory.ordinal cardinals

Gabriel Ebner (Apr 04 2020 at 13:55):

Note that flypitch only defines a very limited class of forcing models. Essentially just Setᵤ and Setᵤ[G] (where Setᵤ is the collection of sets with cardinality less than Type u as defined in Lean).
But even with that you can still define properᵤ (i.e., proper in Setᵤ) and PFUᵤ. From there you should be able to prove that PFU₀ → Setᵤ ⊧ 2^ℵ₀ = ℵ₂  and I believe this should be equivalent to 2^ℵ₀ = ℵ₂

Gabriel Ebner (Apr 04 2020 at 13:56):

I believe the ordinals and cardinals in Setᵤ and Type (u+1) are isomorphic.

Last updated: May 19 2021 at 00:40 UTC