Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Unusual drinker-like paradox

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unusual drinker-like paradox


Chronological Thread 
  • From: Robert Dockins <robdockins AT fastmail.fm>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Unusual drinker-like paradox
  • Date: Tue, 30 Sep 2014 15:15:39 -0700


On Sep 30, 2014, at 1:47 PM, Jonathan
<jonikelee AT gmail.com>
wrote:

> Consider the goal: forall (A:Type), inhabited (inhabited A -> A).
>
> It seems to be a bit like the Drinker's Paradox, but not quite. However, I
> can't seem to prove it from the Drinker's Paradox, or vice versa. It is
> provable from excluded middle. I think it's also weaker than excluded
> middle.
>
> If added to a constructive logic, it would suggest that the resulting logic
> isn't really constructive ("For any type, there exists a way to get an
> instance non-constructively."). But, if it is weaker than excluded middle,
> then paradoxically the logic still is constructive.

I don’t really have an answer to the substance of your question, but I’ll
just remark that merely lacking the law of the excluded middle is not enough
for most constructivists to accept a logic as constructive. There is a zoo
of nonconstructive omniscience principles that are weaker than LEM, but are
nonetheless rejected by constructivists. The “limited principle of
omniscience” and the “lesser limited principle of omniscience” are among the
more well-known.

http://ncatlab.org/nlab/show/principle+of+omniscience

> Anyone seen it before?
>
> It's the most trivial general example I could come up with that can't be
> proved in Coq because Coq doesn't allow "informative" Prop case analysis in
> a non-Prop goal even if that goal is a subgoal of a parent (or ancestral)
> Prop goal - and thus isn't really informative to the overall proof, and
> would be erased during extraction.


Cheers,
Rob


Archive powered by MHonArc 2.6.18.

Top of Page