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.
Added a description of several different approaches to geometric theory.
First of all, every cartesian theory, regular theory, or even coherent theory is a geometric theory. Of course, we don't have those articles yet, but perhaps Mike is planning to write them. In any case, they certainly include all finitary algebraic theories, but also a lot more.
A good example of a coherent theory that is not algebraic (in any of the usual senses, although it comes from algebra) is the theory of a local ring; a similar example is the theory of a discrete field.
But to really answer your question, I need an example of a geometric theory that is not coherent. I actually don't know of a good example; it would involve some sort of infintary disjunction (indexed by an external set, like some sort of ground field or the set of all natural numbers, not by an internal object, since coherent theories can have that). Perhaps Mike does, or perhaps there is one in the Elephant.
Looks like we do have a stub at coherent logic already.
I didn't have immediate plans to write those other articles; geometric theories are in some sense the most important. One nice example of a (propositional) non-coherent geometric theory is the theory of a real number, whose classifying topos is the topos of sheaves on R. There are some other good ones in the Elephant, I'll look them up and add some examples to the page.
I added some examples to geometric theory.
I thought of another example and added it: the theory of a finite set. (Mike should probably check to make sure that there isn't a stupid mistake there, but it looks right to me.)
I don't think you can take the disjunction of a set of sequents. The disjunctions have to happen inside the positive formulae on either side of the sequents.
Dang, you're right! (And without loss of generality, the disjunctions take place on the right-hand side.) So there's my stupid mistake.
But it would have been a nice example, wouldn't it?
Thanks for the large number of examples!
I haven't really absorbed this, though. Maybe I don't really fully know what a "theory" is and what it even means for it to be preserved under geometric morphisms.
I also don't know what "extensional essence" of a Grothendieck topos means.
I know what a Lawvere theory is, some kind of category. Is the idea that I define a Lawvere theory in a topos T1 as a cateory internal to T1 and then ask if its image under a geometric morphisms takes it to an internal categeory that is still a Lawvere theory?
If the answer is: "yes, sure, what did you think?" I'll add a remark making this explicit...
Sorry, I mis-wrote. It's the topos that's the extensional essence of the theory, not vice versa. And it's not the theory that's preserved by geometric morphisms, only its models. The theory itself is defined independently of any topos (or, if you like, internal to the base topos, which is usually Set). Does that help?
@Toby: On p815 of the Elephant is described a different sort of "theory of a finite set" which has one n-ary relation symbol for each n, where is to be interpreted as "the elements through exhaust the set." Its models in Grothendieck topoi are the K-finite objects.
So a theory is some category, a model is a (co)presheaf on it with special properties, and the question is whether these properties are preserved under functors on the (co)presheaf topos?
I still think of a theory (not yet existing, but one of us should write something there) as usually understood in logic, that is as something specified syntactically. If a theory of some kind (of some ‘doctrine’, roughly speaking) can be characterised by a category, then so much the better, but I don’t think of that as what the theory is.
In fact, I doubt that every useful kind of theory can be described as a category (consider the theory of a category, for example), although I have hopes that they might all be describable as $\infty$-categories. So ideally, the choice to view a theory as a syntactic concept or as a higher category should simply be a matter of taste and perpsective.
Anyway, yes, if you specify a theory by a category, then (at least in the simplest situation) a model of the theory is a functor from that category to $Set$, possibly equipped with extra stuff/structure/property. However, you can also consider models in some other category; for example, a model in $Top$ of the theory of groups is a topological group.
@Toby: The theory of categories can be described as a category, namely the syntactic category of the theory of a category. It's not a Lawvere theory, since the theory of categories is not a finite-product theory, but rather is a lex category, since the theory of categories is "essentially algebraic." Internal categories in a lex category C are equivalent to lex functors into C from the syntactic category.
I do also prefer to think about "theories" as being syntactically described, with the resulting syntactic category encapsulating the "extensional essence" of the theory (relative to a given doctrine). In particular, two theories with equivalent syntactic categories are "Morita equivalent" in the sense that they have the same models in all categories (in the relevant doctrine), but I would still not call them the same theory. The other point of view is valid too, though, and from that perspective you can say that a theory is a (small) category T in some doctrine, and a T-model in a category C (in the same doctrine) is a functor (in that doctrine). In particular, Lawvere theories are the same as theories in the doctrine of finite products (the extra condition separating Lawvere theories, as usually defined, from arbitrary small categories with finite products, is just a "cofibrancy" condition that can safely be ignored if you allow your functors to preserve finite products non-strictly).
I'm not sure if that's exactly what you meant by "(co)presheaf," Urs. I think of "presheaf" as usually meaning a functor with values in Set, whereas here the whole point is that the functors can take values in arbitrary categories (in the doctrine).
okay, so preservation of models under geometric morphisms is about whether a functor composed with some functor yields a functor that still satisfies some conditions?
@ Mike:
But is that really the theory of categories? I would say that it is the theory of strict categories; in particular, it includes a notion of equality of objects. It is perhaps the closest approximation to the theory of categories that is itself a category, but it contains extraneous features in the resulting language and does not automatically recover the desired notion of when two categories are equivalent. One can only notice this if one has a previous, more logically oriented notion of what the theory of categories is, derived from practice.
Technical note: An arbitrary (small) category with finite products corresponds to a typed finite-products theory (with smally many types), while a Lawvere theory as usually defined corresponds to an untyped finite-products theory. But that disctinction is also not terrible essential; the generalisation to simply typed theories is quite natural and easy to handle.
@Urs: yes, that's one way to say it. In a sense, though that trivializes the idea, or incorporates it into the definition; the real meat being then in the correspondence between the syntactic presentation of theories and their syntactic categories.
@Toby: To be completely precise, I would call it the theory of internal categories in the doctrine of lex categories. Some people might call it the theory of small categories; strict categories is reasonable too. I agree that this is not the same as the speak-no-evil approach that the two of us, at least, would prefer to regard as "the theory of categories," but I think saying without explanation that "the theory of categories is not a category" gives the wrong impression.
Regarding typing, I presume that by "untyped" you mean what I would call "single-typed." And yes, I generally tend to gloss over the natural-and-easy generalization to multiple types, but maybe that is a bad habit.
okay. I created theory with the little that I understand about it now. Puny as it is, this bit of information is what I was lacking when reading geometric theory
By the way, it seems that elsewhere on the Lab Lawvere theories at least are not distinguished from their syntactic categories. The entry on Lawvere theory says that a Lawvere theory is a certain catgeory. In view of your comments above, maybe the wording should be made more precise?
also, typically on the lab it says that a model is a functor to . In order to understand the entry geometric theory one should probably say that in general a model is something in an arbitrary topos?
A model is, by default, a functor to Set, much as a presheaf is, by default, a functor to Set. But in both cases, one can considers other targets if one wishes (topological models, ring-valued sheaves, etc). And some fields may even have a different default (although I don't know that any do for models).
The term Lawvere theory generally does mean a category; it was Lawvere who first said that we can think of theories as categories rather than as linguistic constructs (with finite-products theories as the first example), and we honour him for his insight with this name.
A model is, by default, a functor to Set, much as a presheaf is, by default, a functor to Set.
Fine, but so the reader of the entry on geometric theories should be alerted that here we consider explicitly models in arbitrary toposes and how they behave as we move geometrically between these.
The term Lawvere theory generally does mean a category
Okay with me, I just made that remark in the light of Mike's comment that
... that trivializes the idea, or incorporates it into the definition; the real meat being then in the correspondence between the syntactic presentation of theories and their syntactic categories.
I am not the expert on this stuff. I am just giving you feedback on how I perceive the entry on geometric theory. When I first read it, it wasn't clear to me if the toposes in question were those where the models take values, or were the toposes of Set-valued presheaves in which the Set-valued models live. So that should be said explicitly in the entry.
I made that comment because we were talking about theories in general, not specifically about Lawvere theories, and to me the default meaning of "theory" is syntactic, not a category. In other words, "Lawvere" is a red herring adjective. (-:
I think it depends on your background whether a model is by default in Set. That's certainly true in model theory, but not so much in categorical logic. But clarification in any particular context is always a good idea.
I renamed at geometric theory the section that used to be titled “from logic to geometry” to In terms of sheaf topoi. Then I put a standout box around the statement that geometric theories are effectively identified with sheaf topoi.
Mike wrote:
In a sense, though that trivializes the idea, or incorporates it into the definition; the real meat being then in the correspondence between the syntactic presentation of theories and their syntactic categories.
I got the impression from Jim Dolan that going from the “syntactic presentation” of a theory to the corresponding category was mainly a bunch of bureaucratic red tape, and that the really fun starts when we get past that stage and think of theories as being those categories. Sort of like how groups are more fun than group presentations, though of course those presentations are very useful. So, I’m a bit surprised that you seem to be taking more of the viewpoint of the traditional fuddy-duddy logician who likes nothing more than manipulating well-formed formulas according to purely syntactic rules - or at least contemplating such manipulations.
I think that deserves a longer answer and a wider audience.
added a pointer to Barr’s theorem to geometric logic (in a new Properties-section)
The axioms for the existence of arrows/objects $X$ with a particular universal property (think: requirement that a category has a subobject classifier) always appear to go like “the category has an object, such that for every arrow from…”.
I.e. $\exists X.\,\forall .\,\dots$
So are those theories then typically or always not geometrical theories?
1 to 32 of 32