>Synthetic differential geometry proves the negation of the law of excluded middle
>The internal logic of a topos is intuitionistic (no LEM)
>Cartesian closed categories and most type theories (so the foundation of CS) are in correspondence with intuitionistic logic by the Curry-Howard-Lambek correspondence
>The axiom of choice implies LEM by Diaconescu's theorem i.e. the negation of LEM implies the negation of the axiom of choice
>Now a lot of math relies on the axiom of choice or its equivalents e.g. every vector space has a basis
Is math fucked?
>The internal logic of a topos is intuitionistic (no LEM)
>Cartesian closed categories and most type theories (so the foundation of CS) are in correspondence with intuitionistic logic by the Curry-Howard-Lambek correspondence
>The axiom of choice implies LEM by Diaconescu's theorem i.e. the negation of LEM implies the negation of the axiom of choice
>Now a lot of math relies on the axiom of choice or its equivalents e.g. every vector space has a basis
Is math fucked?
