The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

There might be working mathematicians who would explain that ZFC is not the only foundation : the specialists of ZFC. In Patrick Dehornoy's book "la théorie des ensembles", he says that the main purpose of ZFC is the study of big infinities, big cardinals. Thus modern set theorists must add extra axioms such as the existence of inaccessible cardinals. Naturally they also add excluded middle, because their objects of study are by definition non computable.

Dehornoy also says that the foundation of mathematics by ZFC is an accident. It was not meant by Cantor at the beginning of set theory, and it is probably not meant by modern practitioners of ZFC. Incidentally, Dehornoy cites HoTT as another and promising foundation.

This conversation mentionned examples in differential geometry, algebraic geometry, algebra and number theory, but none in ZFC. It seems a sign that modern mathematics do not need ZFC, except for the specific study of big infinities.

On Thu, Jan 9, 2020 at 8:25 AM Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:

Le 08/01/2020 à 20:00, BEGAY Pierre-leo a écrit :

Talia Ringer <tringer AT cs.washington.edu> a écrit :

> Last I checked, the plan was to allow for simple, verified extensions to
> Coq in order to handle computational interpretations of different axioms.
> Nicolas Tabareau gave a talk about this at ITP.
>
> It remains to be seen whether this is possible in a way that does not have
> serious drawbacks, as I gather the customizability of Isabelle is one of
> the biggest pain points, and most users only ever use Isabelle/HOL anyways.
> Perhaps having different proof assistants for different needs is a
> perfectly acceptable status quo. That is, after all, true for other
> programming languages.
>
> Maybe the right focus in that case is interfacing between proof assistants,
> so that we can have projects that use bits and pieces of both as
> applicable. Or automatic reuse of programs, specifications, and proofs
> across different proof assistants when possible, with some kind of verified
> guarantee about the layer interfacing the tools.

You might want to take a look at logipedia and Dedukti. I am no expert on this (I only saw a talk about it given by Gilles Dowek, who I assume is the leader on both projets), but as far as I understand, the former is an encyclopedia of proofs across different languages built upon the latter. The point of this seems to be the analysis of the need for theory-specific axioms in different proofs, to see if they could be translated to assistants built around weaker theories. I'm not sure how operational this whole thing is though.

Pierre-Léo

Thanks Pierre-Léo for the ad! ;-) Note that until some time ago Dedukti was not an interactive proof assistant but just a type-checker. We are currently working in turning it into a full proof assistant with tactics and some LSP-based interface (emacs and vscode). See https://github.com/Deducteam/lambdapi for more details. The interesting point of Dedukti and its new version is that functions and predicates can be defined by giving arbitrary rewriting rules. Rehan Malak and Bruno Barras use this feature to develop models of cubical type theory. Best regards, Frédéric Blanqui, coordinator of the development of the new version of Dedukti.

>
> On Wed, Jan 8, 2020, 12:44 AM Sylvain Boulmé <
> Sylvain.Boulme AT univ-grenoble-alpes.fr> wrote:
>
>> Hello,
>>
>> Le 08/01/2020 à 02:50, jonikelee AT gmail.com a écrit :
>> > [decloaking from lurker mode to add my $0.02]
>> >
>> > Does having LEM built into Lean interfere with the user's ability to
>> exploit the Curry-Howard isomorphism?
>> >
>> > If so, that seems like a bad trade off: a small convenience for a
>> > small group of people (Fields Medal wanabees) that imposes a large
>> > inconvenience for a large group of people (software engineers).
>>
>> Actually, I guess that a classical interpretation of "Prop" is
>> compatible with *many* certified software development in Coq. For
>> example, consider the CompCert compiler: currently, it is intented to be
>> used through Coq extraction, and since the current Coq extraction
>> removes Prop contents, it is consistent with proof-irrelevance and
>> classical propositions.
>>
>> Thus, as I understand it, supporting non-classical propositions is
>> motivated by higher-order mathematics or by programming on propositions
>> in the proof assistant... Hence, the picture is quite the opposite:
>> currently, most people using maths (including software engineers) do not
>> care of constructive propositions, and simply use classical logic,
>> because it is convenient.
>>
>> But, this does not mean that proof assistants should only care about the
>> majority. For example, it would be great to have an enhanced Coq
>> extraction, able to deal with an univalent version of equality (this
>> would provide a powerful mechanism of "coercion"). Is there any progress
>> in this direction ?
>>
>> Sylvain.
>>