Forum

Notifications
Clear all

Questions about unification theory


mdjoknaan
(@mdjoknaan)
Active Member
Joined: 7 months ago
Posts: 5
Topic starter  
Hi,

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.

 
My first question is, let's say that I have theory T1 , and somehow I manage to extend it to  a more general one T2, by more general i mean that each sentences of T1 can be completely translated into the language of the T2 (ie. definitions, theorems, etc.), we can also imagine that the T2 contains more general quantifiers such as the sentences in the subtheory are just a particular case of the  more general one.
Obviously in the super-theory you will have more theorems, more definitions, etc. What you don't want to do is to start over in your super-theory, you want some kind of "map" whereby you can 'canonically' convert definitions into super-definitions such as if you have a theorem in your sub-theory this theorem still holds in the extended one in a "general" way.
You also want to be able to see if you can translate those definitions to exotic definitions so as to have new theorems, once you have eliminated all those cases you can really focus on what is really specific to your super-theory.
So my question is, is there an easy way to do that, an object or a concept of the bridge or unification theory?

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.

 
 
My second question is, is there a more general structure than the topos one, in the sense that one can have some category structure, without a topos structure but still having some logic associated to it;  i'm not really at ease with the terminal objects used to describe the truth map (correct me if i'm wrong), in general i'm not  a ease with the way the terminal object is used, i'm more at ease with the notion of initial object.

Thanks for bearing with me.

 
This topic was modified 7 months ago by mdjoknaan

ReplyQuote
Joshua Wrigley
(@jwrigley)
Eminent Member
Joined: 12 months ago
Posts: 22
 

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  \mathbb{B} and its associated Stone locale  L_{\mathbb{B}} .  This clearly has an "interpretation" in that  \mathbb{B} can be embedded into  L_{\mathbb{B}} .  Essentially all we're doing is allowing infinitary or-statements.  This embedding corresponds to a geometric morphism at the level of topoi Sh(L_{\mathbb{B}}) \to Sh(\mathbb{B}).  In fact, this morphism is an equivalence of categories as every model of the logic described by \mathbb{B} is also a model of L_{\mathbb{B}} 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 {\bf Sets}^{[0,1]}, where [0,1] is considered as a preorder category.  A topos for sets could be just {\bf Sets}.  Then there are multiple interpretations induced by geometric morphisms between the two.

  • There is the unique geometric morphism \gamma \colon {\bf Sets}^{[0,1]} \to {\bf Sets} with \gamma^\ast sending  X \mapsto \coprod_{x \in X} 1_{{\bf Sets}^{[0,1]}} .  This is the interpretation you suggested (note that the terminal object 1_{{\bf Sets}^{[0,1]}} is the functor that sends every x \in [0,1] to 1_{\bf Sets}).
  • For each  x \in [0,1] there is a geometric morphism in the opposite direction given by evaluating the fuzzy sets at  x - that is  ev_x \colon {\bf Sets} \to {\bf Sets}^{[0,1]} with ev_x^\ast acting by  [0,1] \xrightarrow{P} {\bf Sets} \mapsto P(x) .

ReplyQuote
mdjoknaan
(@mdjoknaan)
Active Member
Joined: 7 months ago
Posts: 5
Topic starter  

@jwrigley

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 f \colon E \to [0,1] as a fuzzy set, what would be closest to a singleton in the fuzzy set theory is those type of functions,x_\alpha \colon E \to [0,1] where  x \in E, \alpha \in ]0,1] with  x_\alpha(y) = \alpha iff  y =x 0 otherwise.

In that case we say x_\alpha \in f if f(x) \neq 0 and \alpha = f(x).

So now the map are \delta \colon f \to g with \delta \colon \{x_\alpha \in f\} \to \{y_\beta \in g\}
This way you have a category with all your small limits (even exponentials) however when trying to get the natural isomorphism
\theta_f \colon [f, P(g)] -> Sub(f \times g)  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: f = g \iff (\forall x_\alpha, x_\alpha \in f \iff x_\alpha \in g)

 

I'm going to have a look on the geometric morphisms.
That's very helpful.

This post was modified 7 months ago by mdjoknaan

ReplyQuote
mdjoknaan
(@mdjoknaan)
Active Member
Joined: 7 months ago
Posts: 5
Topic starter  

There is also a similar behaviour, with a category, an "arithmetic" category

you take as the objects the natural number, you have a \in n iff a = p^\beta, \beta \geq 1 and a | n where p is a prime number, same thing here a map is \delta \colon n \to k with \delta \colon \{a \in n\} \to \{b \in k\}


ReplyQuote
Joshua Wrigley
(@jwrigley)
Eminent Member
Joined: 12 months ago
Posts: 22
 

Hi again, I never said fuzzy set theory and standard set theory are semantically equivalent.  The two topoi {\bf Sets}^{[0,1]} and {\bf Sets} 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 \mathcal{E}, that two objects E,\, F are isomorphic if the Hom-sets  {\rm Hom}_{\mathcal{E}}(1_{\mathcal{E}}, E) \cong {\rm Hom}_{\mathcal{E}}(1_{\mathcal{E}},F) are bijective, unlike in {\bf Sets}.  This can clearly be seen even in presheaf topoi.

Let {\bf 2} be the category  \bullet_0 \to \bullet_1 .  The terminal object 1_{\bf Sets^2}\in {\bf Sets}^{\bf 2} is given by 1_{\bf Sets^2}(\bullet_0) = 1_{\bf Sets^2}(\bullet_1) = \{\ast\}; the initial object 0_{\bf Sets^2}\in {\bf Sets}^{\bf 2} is given by 0_{\bf Sets^2}(\bullet_0) = 0_{\bf Sets^2}(\bullet_1) = \emptyset.  Now consider the functor P \colon {\bf 2} \to {\bf Sets} given by P(\bullet_0) = \emptyset, \, P(\bullet_1) = \{\ast\}.  There's no arrow \{\ast\} = 1_{\bf Sets^2}(\bullet_0) \to P(\bullet_0) = \emptyset and so \emptyset = {\rm Hom}_{\bf Sets^2}(1_{\bf Sets^2},P) \cong {\rm Hom}_{\bf Sets^2}(1_{\bf Sets^2},0_{\bf Sets^2}) but also  P \not \cong 0_{\bf Sets^2}.

In general, in an arbitrary topos, it is not sufficient to consider global elements (i.e. arrows 1_{\mathcal{E}} \to F) but generalised elements E \to F.

 

 


ReplyQuote
mdjoknaan
(@mdjoknaan)
Active Member
Joined: 7 months ago
Posts: 5
Topic starter  

@jwrigley

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

This post was modified 7 months ago by mdjoknaan

ReplyQuote
GrothenDitQue
(@grothenditque)
New Member
Joined: 11 months ago
Posts: 3
 

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

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


ReplyQuote
Share: