The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

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