The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-08-05 0:59 GMT+02:00 Daniel Schepler <dschepler AT gmail.com>:

This is interesting - I've thought myself of explaining the
Curry-Howard correspondence to mathematicians as a way of converting
any proposition to a type (or ZFC set if they want) such that the
original proposition is equivalent to the type being "nonempty" (or
more accurately in the intuitionistic universe, inhabited).  And then
from that starting point, you can explain why an element of the type
corresponds very naturally to a formal proof of the proposition.  So
for example, for the recursive steps,

A≠∅ /\ B≠∅ <-> A×B≠∅
A≠∅ \/ B≠∅ <-> A⊔B≠∅
(A≠∅ -> B≠∅) <-> Fn(A,B)≠∅
(∃ i, A_i ≠ ∅) <-> (⊔_i A_i) ≠ ∅
(∀ i, A_i ≠ ∅) <-> (∏_i A_i) ≠ ∅

The problem here is that the last one is exactly the axiom of choice.
And similarly, the first proof I usually think of for the third one
requires excluded middle for B≠∅ and it's probably not provable with
axiom-free Coq.

I easily got tricked with that, but isn’t it rather A≠Ø?

For your third point, you can cheat either by using axiom of choice (which you needed in your 5th case), or by defining "A≠Ø" as "(A→⊥)→⊥", that is: there is no function from A to the empty set (and thus avoid the intuitionistic problems), unless I am wrong.
 

--
Daniel Schepler

On Mon, Aug 4, 2014 at 3:12 PM, Matthieu Sozeau
<matthieu.sozeau AT inria.fr> wrote:
> Maybe another view could help, consider Prop as a universe built from 0, 1, x of Props and [A], where [A] “squashes”
> the information in an arbitrary A : Type. 0, 1 and x have unrestricted eliminations to Type, whereas [A] is restricted
> to Prop contexts, and equality in all those type is irrelevant. Disjunction and existentials now become squashed, i.e,
> A \/ B := [A+B] and exists x : A. B := [{x : A & B}]. Now you can prove that 1 and [1 + 1] are isomorphic using
> these rules, and hence eliminate hence on [1 + 1] in Type, but wouldn’t get to know which side is proven, the eliminator
> would be, again:
>
> [1+1]-elim : (P : [1+1] -> Type) (p : forall x : 1, P (to-1+1 x)) (x : [1+1]) : P x.
>
> Where (to-1+1 x : [1+1]) is irrelevant, whether you implement it using [left x] or [right x], [left 1] or [right 1],
> these can’t be distinguished anymore. I think this reasoning is consistent with what Coq does,
> see the Rooster and the Syntactic Bracket by A. Spiwack and H. Herbelin that describes this “decomposition”
> of Prop in more details.
>
> Hope this helps,
> — Matthieu

--
.../Sedrikov\...