[FOM] the amazing language of set theory

[Louis Garde]

Le 26/03/2016 00:39, Martin Davis a écrit :
> The somewhat analogous twentieth century discovery that all of 
> mathematics can be reinterpreted into statements in the language of 
> set theory (just one binary relation, usually written as the Greek 
> letter "epsilon") has revolutionized not mathematical practice, but 
> rather foundational studies.

 From my point of view, the discovery that the concept of 'logical 
consequence' can be identified with the set-theoretic concept of 
'function' is the next big step in the same direction.
This is the "proposition-as-type"paradigm ( see 
https://ncatlab.org/nlab/show/propositions+as+types ), at the heart of 
Martin-Löf type theory and HoTT.

Unfortunately, because of historical reasons, it seems that many people 
still believe that this identification leads to a restrictive logic.
The Law of Excluded Middle, or the Axiom of Choice, are not incompatible 
with this identification, but without them you can do constructive logic.

Making the law of excluded middle optional is an enrichment for logic 
and mathematics, not a restriction ( see 
http://math.fau.edu/richman/Docs/philmath.pdf ).

Louis.