[FOM] The unbearable ghastliness of EFQ, and Tim Chow's focusing question

[Louis Garde]

Le 05/09/2015 22:50, Harvey Friedman a écrit :
>   But let me ask
> the readership what they have seen of interest about negation free
> formalizations for mathematics?
I would not say that HoTT is a negation free formalization for 
mathematics, but still negation comes with a different flavour in it:

In HoTT, each proposition is defined as a type; the construction of an 
element a:A of a type A is a (constructive) proof of the proposition A.

Negation is then /defined /as a function from a type A to the empty type 
0: the type "~A" is /defined/ as "A->0", the type of the functions from 
type A to the empty type 0.
The empty type 0 is /defined /itself by the EFQ property, that can be 
written as: efq_X :0->X, that is to say for any type X we have a 
function efq_X that builds an element of type X from an element of type 0.

You have a contradiction when you have both a:A and a':~A; as a':~A is 
by definition a function from A to 0, you can apply a' to element a and 
you get a'(a):0, an element of 0.
You can then apply efq_X to a'(a), and you get efq_X (a'(a)):X, that is 
to say efq_X (a'(a)) is a proof of the proposition X. So with a 
contradiction in A you can prove any proposition X.

The type 0 is not used in the axiomatization of the other HoTT types, so 
it is perfectly possible to do mathematics in HoTT without using it. But 
then you have no way to express that some structure "does not have the 
property P", so you miss a lot of information on your structures.

Louis.



-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150906/46e58a28/attachment-0001.html>