Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I just read that Synthetic Differential Geometry rejects the principle of the excluded middle. Surly that was said a lot before here, but I wasn’t aware of that. I like to know that and personal I think for a long time that truth should be four valued:
TRUE
FALSE
UNDEF
UNDEC
However that was nothing more than a private believe system, because I thought that there is not much for the UNDEC value. But since “Determining whether two finite simplicial complexes are homeomorphic” is UNDEC it is maybe of not so little practical importance.
rejects the principle of the excluded middle
really it means working internal to a topos which approximates very closely the category of smooth manifolds. If one thinks of ’propositions’ as being open submanifolds and negation as being the interior of the complement, then it is clear that can’t be (the whole space) in general. In that sense, I don’t think it is true that there are four truth values, because I doubt that the subobject classifier looks like that.
There are small Heyting algebras which look like something you describe, I recall seeing such a thing in a lecture by Chris Mortensen, a logician at Adelaide, on inconsistent mathematics.
a topos which approximates very closely the category of smooth manifolds
Well, plus infinitesimal objects (that being sort of the whole point of SDG). And infinite-dimensional ones.
a topos which approximates very closely the category of smooth manifolds
Well, plus infinitesimal objects (that being sort of the whole point of SDG). And infinite-dimensional ones.
On the other hand excluded middle already fails in the topos which is something like the context for “SDG without infinitesimals”. Also, already here it is true that “all functions are smooth”, something that is often said as if characteristic of SDG.
Not that this contradics anything, but Mirco might find it useful to be aware of this.
Well, plus infinitesimal objects (that being sort of the whole point of SDG). And infinite-dimensional ones
yes, but in a way that ordinary manifolds do what they should.
To me, rejecting the principle of the excluded middle just means that for example contraposition proofs are not allowed. So when I hear that a formalism rejects it I would naively think, that the hole story is constructed without that kind of proof principle.
Mirco, let me re-iterate what David already said:
the statement that “SDG rejects excluded middle” is only true if you make yourself work strictly internally to a topos that models SDG.
Most applications of SDG happily work externally and just look at some such topos from the outside as one does for any old category. Then there is nothing funny about the logic.
It can be a pretty powerful thing to strictly work internally in a given category, but unless and until you have good reason to do so and know what you are doing, you can happily ignore all statements about non-classical logic.
The thing is that most any category that you will come across has even weirder internal logic than a topos that models SDG. For instance you could take something as mundane as the category of vector spaces or the like. If you tried to work strictly internal to it you’d find the most bizarre kind of internal logic. But this does not mean that we cannot perfectly reason about vector spaces with ordinary logic by looking at them from the outside. As everybody usually does.
7: I wanted to write the same :)
1 to 8 of 8