The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 11/01/2020 05:22, Hugo Herbelin wrote:
> On the constructive/classical debate, I tend to think that it is
> indeed a rather ideological issue. I would not be surprised that by
> about say 5 years from now on, we are able to design a type theory
> with fully-computational excluded-middle and fully-computational
> extensional axiom of choice. Presumably, this "classical" type theory
> will build on a cubical equality, which, I agree here with Thorsten,
> is the nicest way I know to provide computational quotients. Moreover,
> on the practical side, it would be easy in Coq to provide as soon as
> now a file axiomatizing quotients, as Arthur proposed, the same way as
> classical reasoning is already supported axiomatically.

It is fairly easy to build a syntactic model of CIC + SProp (without
UIP) + excluded middle on strict propositions, but without choice.
Similarly, there is a model of CIC extended with a classical modality
that enjoys both choice and excluded middle, at the cost of loss of
large dependent elimination on boxed inhabitants and a few additional
restrictions.

I am much less convinced of the possibility of a computational
interpretation of EM (strict or not) + AC + large elimation, even
restricted in the style of Baclofen Type Theory to prevent the paradox
that bears your name. Apart from the fact this is too similar to
something Krivine has been trying to achieve for 30 years, the recent
SProp + UIP + impredicativity utter debacle is making me lean on the
side of extreme suspicion. I hope future will prove me wrong though.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature