Return to Question

In what way and with what utility is the law of excluded middle usually disposed of in intuitionistic type theory and its descendants? I am thinking here of topos theory and its ilk, namely synthetic differential geometry and the use of topoi in algebraic geometry (this is a more palatable restructuring, perhaps), where free use of these "⊨P∨¬P" theories is necessarily everywhere--freely utilized at every turn, one might say. But why and how are such theories first formulated, and what do they look like in the purely logical sense?

You will have to forgive me; I began as a student in philosophy (not even that of mathematics), and the law of non-contradiction is something that was imbibed with my mother's milk, as it were. This is more of a philosophical issue than a mathematical one, but being the renaissance guys/gals that you all are, I thought that perhaps this could generate some fruitful discussion.

In what way and with what utility is the law of excluded middle usually disposed of in intuitionistic type theory and its descendants? I am thinking here of topos theory and its ilk, namely synthetic differential geometry and the use of topoi in algebraic geometry (this is a more palatable restructuring, perhaps), where free use of these "¬⊨P∨¬P" theories is necessarily everywhere--freely utilized at every turn, one might say. But why and how are such theories first formulated, and what do they look like in the purely logical sense?

You will have to forgive me; I began as a student in philosophy (not even that of mathematics), and the law of excluded middle is something that was imbibed with my mother's milk, as it were. This is more of a philosophical issue than a mathematical one, but being the renaissance guys/gals that you all are, I thought that perhaps this could generate some fruitful discussion.

In what way and with what utility is the law of excluded middle usually disposed of in intuitionistic type theory and its descendants? I am thinking here of topos theory and its ilk, namely synthetic differential geometry and more modern higher algebraic geometry, where free use of these "⊨P∨¬P" theories is necessarily everywhere--freely utilized at every turn, one might say. But why and how are such theories first formulated, and what do they look like in the purely logical sense?

You will have to forgive me; I began as a student in philosophy (not even that of mathematics), and the law of non-contradiction is something that was imbibed with my mother's milk, as it were. This is more of a philosophical issue than a mathematical one, but being the renaissance guys/gals that you all are, I thought that perhaps this could generate some fruitful discussion.

In what way and with what utility is the law of excluded middle usually disposed of in intuitionistic type theory and its descendants? I am thinking here of topos theory and its ilk, namely synthetic differential geometry and the use of topoi in algebraic geometry (this is a more palatable restructuring, perhaps), where free use of these "⊨P∨¬P" theories is necessarily everywhere--freely utilized at every turn, one might say. But why and how are such theories first formulated, and what do they look like in the purely logical sense?

You will have to forgive me; I began as a student in philosophy (not even that of mathematics), and the law of non-contradiction is something that was imbibed with my mother's milk, as it were. This is more of a philosophical issue than a mathematical one, but being the renaissance guys/gals that you all are, I thought that perhaps this could generate some fruitful discussion.