[FOM] Improving Set Theory

[Emilio Jesús Gallego Arias]

Hi all,

>> Lean does not have this problem. For me, Lean is the only one worth
>> learning if you actually want to do mathematics.

As already pointed out by other people this seems like a pretty bold
claim given that people has been successfully doing pretty advanced
maths in Coq, Isabelle, HOL, Mizar, etc... for a quite a bit of time.

There is a long discussion about "Lean vs Coq" going on the coq-club
mailing list for those interested, but I'd like to provide a different
point of view to a couple of foundational-related remarks about Coq
below:

>> Two problems with Coq: (1) it really wants you to do constructive
>> mathematics

I guess we would have to specify what "really" means here, but so far
Coq has been extensively used to build classical proofs; maybe it
suffices to point that the real numbres in the Coq standard library are
classical, not constructive.

Several forms of the axiom of excluded middle are indeed present in
Coq's standard library, and other than the loss of computational
interpretation, using them poses no more difficulty.

People in Coq tend to use quite advanced "home-grown" tactics so indeed
for some users their tactics will work better with the EM axiom.

IIUC Lean handles the EM axiom in a bit of a special way; so indeed
there is a slight advantage as Coq users must use tactics aware of the
EM instead; on the other hand Lean pays a price which is loss of some
theoretical properties about the core logic IIANM.

>> (2) it doesn't have quotients. If you have an equivalence relation on
>> a type (i.e. a set) and you want to construct the set of equivalence
>> classes plus the universal property, you're out of luck. You have to
>> work with the big object and consider functions on it which are
>> constant on equivalence classes. They even have a word for it --
>> "setoid hell".

Regarding quotients the situation is similar to EM, they can be
axiomatized in a pretty convenient way [1] , all you need is to make
tactics aware.

People have been using different formulation of quotients [for example
the FT proof relies on a different notion] with success for quite a long
time.

It is true that the nature of Coq tends to be quite "open" in terms of
what solutions are possible. In some cases such as quotients, a lot of
choice is given to the end-user and indeed, implementing an effective
tactic set to reason about quotients is a very difficult endeavor so
users face pain often.

Kind regards,
E.

[1] http://poleiro.info/posts/2019-12-25-quotients-in-coq.html