The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, but given that it is a choice principle, maybe we can conclude (in response to Jonathan’s original question) that it is not really constructive…?

Well, it is fairly subtle… There are plenty of variant of choice which are (trivial) theorems in type theory. That being said, it is known that choice principles involving Prop, while they can be admitted, cannot be given their natural type theoretic proofs without creating inconsistency. Which seems to mean they probably don't have a total realizer. In this sense, we're probably facing a non-constructive principle. But I'd like to see some better proof of that.

But, I guess that brings out a different kind of theoretical question.  Coq's Props already have a different logic (impredicative) from the logic of Types.  And, of course, one doesn't have to worry about what Props would extract to, as they don't.  Why then keep Prop so constructive?

Coq is about as big as it can while preserving erasability, canonicity (i.e. every normal form of an inductive type starts with a constructor, and other such properties) and consistency. There is no known way to extend it without compromising one of these properties.

On 2 October 2014 23:22, Jonathan <jonikelee AT gmail.com> wrote:

On 10/02/2014 01:02 PM, Eddy Westbrook wrote:

Well, but given that it is a choice principle, maybe we can conclude (in response to Jonathan’s original question) that it is not really constructive…?

-Eddy

Mostly, I was just trying to think of what Coq's logic would allow if its Prop elimination rules were extended to allow Prop elimination anywhere in a Prop-rooted proof subtree instead of just in Prop subgoals themselves.

It is interesting that such an extension would be equivalent to a kind of weak choice axiom.  Because I was just thinking in very practical terms - sometimes one finds oneself in a non-Prop subgoal in a Prop-rooted proof subtree and needs to analyze a Prop - and currently the only way to do that is to undo back to some earlier Prop subgoal (perhaps the root of that subtree) and do the analysis there - and such undoing could require restructuring the proof.  So, I thought that such an extension wouldn't add anything at all to the logic - but it does.  And, it's a weak choice axiom, hence not constructive.

But, I guess that brings out a different kind of theoretical question.  Coq's Props already have a different logic (impredicative) from the logic of Types.  And, of course, one doesn't have to worry about what Props would extract to, as they don't.  Why then keep Prop so constructive?

Certainly, one can always add their favorite choice axiom(s).  But, the above Prop-subtree elimination extension, even though it seems to be equivalent to a weak choice axiom, can't be added through use of any such axiom (that would be consistent with the rest of Coq's logic) - at least I can't see how.

-- Jonathan

On Oct 2, 2014, at 9:41 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Well, this principle of choice is equivalent to the dependent version of Pierre-Marie's above: [forall A B, (forall x:A, inhabited B) -> inhabited (forall x:A, B)]. I don't think it implies excluded-middle by itself. But it does if you add in quotient types. The non-dependent version, however, seems pretty weak.

On 2 October 2014 18:01, Eddy Westbrook <westbrook AT kestrel.edu> wrote:
Yes, you are right, thanks!

I got the name TTDA from Werner's paper "Sets in Types, Types in Sets", where he has a different axiom that he calls a choice principle.

It also looks like AC_fun in Coq.Logic.ChoiceFacts.

So, then, does this version of choice imply excluded middle? I can't find a proof in the standard library...

Eddy

Sent from my iPhone

On Oct 1, 2014, at 6:12 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 10/01/2014 09:01 PM, Eddy Westbrook wrote:
The nondep_AC axiom below is, I think, equivalent to the Type-Theoretic Description Axiom (TTDA), which is this:

Definition TTDA : Type :=
   forall (A B : Type) (P : A -> B -> Prop),
     (forall (a : A), exists b, P a b) ->
     (exists f, forall (a : A), P a (f a)).

That looks like Coq.Logic.ClassicalChoice.choice.

TTDA has some sort of non-constructive content, in that it, with propositional Excluded Middle, allows you to prove informative Excluded Middle. I am not what TTDA just by itself allows, however.

-Eddy

On Oct 1, 2014, at 5:29 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 30/09/2014 22:47, Jonathan wrote:
Anyone seen it before?

It seems instead equivalent to a weak form of a non-dependent axiom of
choice, rather than to excluded middle :

Definition nondep_AC := forall A B, (A -> inhabited B) -> inhabited (A
-> B).
Definition escape := forall A, inhabited (inhabited A -> A).

Lemma dir : nondep_AC -> escape.
Proof.
intros ac A; apply ac; trivial.
Qed.

Lemma rev : escape -> nondep_AC.
Proof.
intros esc A B f.
destruct (esc B) as [g].
constructor; auto.
Qed.

PMP