Questions about unification theory
As I started recently category theory and topos theory, I have some questions about unification theory and bridges, I precise that i'm an autodidact so i'm very far from being an expert.
Here is a pseudo-example, for T1 take the set theory, for T2 take the fuzzy set theory, if you see a set E as a constant function whose value is always 1 (fuzzy set) ,each sentence regarding that set in the set theory can match a sentence in the fuzzy set theory, and what you want is to have a mapping between definitions of set theory to definitions in the fuzzy set theory such as the theorems in the set theory still hold through the mapping in the fuzzy set theory.
You don't want to try to find by yourself all the theorems manually. You want a natural way to go from T1 to T2.
Thanks for bearing with me.
Hi there, correct me if I'm wrong but what it sounds like you're describing is a sort of interpretability of signatures. Fortunately for topos theory we can handle theories in a syntax-invariant manner. Specifically, two geometric theories, in potentially different signatures, are semantically equivalent (that is Morita equivalent) if and only if their classifying topoi are equivalent. Furthermore, a geometric morphism from one classifying topos to another represents, in some way, a syntax invariant "interpretation".
Let's look at some examples to clarify things. Let's start with some posets (these represent propositional logics). Take a Boolean algebra and its associated Stone locale . This clearly has an "interpretation" in that can be embedded into . Essentially all we're doing is allowing infinitary or-statements. This embedding corresponds to a geometric morphism at the level of topoi . In fact, this morphism is an equivalence of categories as every model of the logic described by is also a model of and vice versa - even in an arbitrary topos - and so the two are semantically equivalent.
For the example you raise, (now bear with as I don't know much about fuzzy set theory) we could brute force a topos for fuzzy set theory by taking the presheaf topos , where is considered as a preorder category. A topos for sets could be just . Then there are multiple interpretations induced by geometric morphisms between the two.
- There is the unique geometric morphism with sending . This is the interpretation you suggested (note that the terminal object is the functor that sends every to ).
- For each there is a geometric morphism in the opposite direction given by evaluating the fuzzy sets at - that is with acting by .
That is very interesting, as far as I'm learning topos theory i'm eventually going to come across those morita equivalences.
Actually I don't think there are some semantic equivalence between fuzzy set theory and the set theory, now if you can move from a classifying topos to another (I think that what you call an interpretation) this is exactly what i want.
Well for that i'll construct the fuzzy set category, I think this is a natural way to see it:
So you have as a fuzzy set, what would be closest to a singleton in the fuzzy set theory is those type of functions, where with iff 0 otherwise.
In that case we say if and .
So now the map are with
This way you have a category with all your small limits (even exponentials) however when trying to get the natural isomorphism
you'll have some issues. I don't even know that way if you get a topos.
That is why I asked if there are more general structure than topos, cause you might want to go from classical logics to more exotic one, and thats why I said that I have issues with the truth map being from the terminal to the subobject clasifyer because in more exotic logics you have also non terminal objects behaving like singleton object. In that case:
I'm going to have a look on the geometric morphisms.
That's very helpful.
There is also a similar behaviour, with a category, an "arithmetic" category
you take as the objects the natural number, you have iff and where p is a prime number, same thing here a map is with
Hi again, I never said fuzzy set theory and standard set theory are semantically equivalent. The two topoi and are definitely not equivalent categories. They are, however, related by many geometric morphisms.
That being said, I'm very happy to accept that my proposed model for fuzzy set theory is not perfect.
As for your other question about whether there are more general structures than a topos: there's always something more general, although I'm not knowledgeable enough to suggest any with confidence. However, it seems topoi still suffice for your purposes: it is not the case, in an arbitrary Grothendieck topos , that two objects are isomorphic if the Hom-sets are bijective, unlike in . This can clearly be seen even in presheaf topoi.
Let be the category . The terminal object is given by ; the initial object is given by . Now consider the functor given by . There's no arrow and so but also .
In general, in an arbitrary topos, it is not sufficient to consider global elements (i.e. arrows ) but generalised elements .
Yes, i'm trying to figure out how that structure work, I still have issues with that so I can sound a bit unclear; your example work.
I'm going to have a look about what you said on the geometric morphisms, because that's what I was looking for.
Hopefully a topoi will suffice.
Thanks a lot for the help
Hi; all has been said about the topos-theoretic account of your question, so I just wanted to expand a bit about the actual syntactic notion of interpretation that was named and that you really seemed to be talking about in your question: It's exactly what you want, a theory* T1 is interpretable by another one T2 when there exists a syntactic translation of the sentences between their respective languages (whether they are axioms [definitional or not], theorems, refutable, undecidable, etc.), which is correct in the sense of translated T1-theorems remaining T2-theorems. This translation is an interpretation of T1 by/into T2.
*where by this word I don't mean the vague concept of a branch of mathematics, but an actual formal system; so in your examples, some fixed set theory such as ZF, and some fixed fuzzy one.