coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Unusual drinker-like paradox, Robert Dockins, 10/01/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] Unusual drinker-like paradox, Pierre-Marie Pédrot, 10/01/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Arnaud Spiwack, 10/01/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Eddy Westbrook, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Jonathan, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Eddy Westbrook, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Arnaud Spiwack, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Eddy Westbrook, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Jonathan, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Arnaud Spiwack, 10/07/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Eddy Westbrook, 10/07/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Eddy Westbrook, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Arnaud Spiwack, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Eddy Westbrook, 10/02/2014
- Re: [Coq-Club] Unusual drinker-like paradox, Jonathan, 10/02/2014
Archive powered by MHonArc 2.6.18.