The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Aug 5, 2014 at 2:03 AM, Cedric Auger 
<sedrikov AT gmail.com>
 wrote:
>
>
>
> 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≠Ø?

Well, the classical argument for the forward direction would go
something like: "If B is nonempty, choose an element b; then the
constant function with value b shows Fn(A,B) is nonempty.  Otherwise,
if B is empty, then A is also empty, so the 'empty' function shows
Fn(A,B) is nonempty."  Of course, I guess using excluded middle on A
nonempty you could give a very similar proof.

> 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.

Oh, right, I suppose it's provable that (~ notT A -> ~ notT B) -> ~
notT (A -> B).  It's (inhabited A -> inhabited B) -> inhabited (A ->
B) that's probably not provable.
-- 
Daniel Schepler