show/hide this revision's text 3 deleted 1 characters in body

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" ¬⊨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 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.

show/hide this revision's text 2 Took out the 'non-well-defined' appeal to 'higher' algebraic geometry. I suppose incessant hair-splitting must be the norm here...

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 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.

show/hide this revision's text 1

Au revoir, law of excluded middle?

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.