[FOM] the amazing language of set theory
louis.garde at free.fr
Sat Mar 26 02:26:27 EDT 2016
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
More information about the FOM