The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

Dear Gaëtan,

please allow me to get back to this.

Am Mittwoch, den 06.12.2017, 21:56 +0100 schrieb Gaëtan Gilbert:
> It's equivalent to epsilon.
> 
> Let A : Type. Consider the function
> 
>    λ x : A + bool => match x with inl a => inl a | inr b => inr (not b)
> 
> It has a fixed point if and only if A is inhabited, but A + bool is 
> always inhabited (eg by inl true).
> 
> In the attached file I use this to prove epsilon from your axioms.

in your file you define

    Lemma epsilon A (H : inhabited A) : A.

but that is not (as I first thought) the epsilon from
Coq.Logic.ClassicalEpsilon or Coq.Logic.Epsilon, which is

     Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A


I see that your [epsilon] allows me to get a value out of an
[inhabited A], which is usually not allowed, but what are the
consequences of that? How does it related to the full Hilbert’s axiom?


Thanks,
Joachim

-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part