I replaced “all the same models in all Grothendieck topoi” by “categories of models in all Grothendieck topoi up to equivalence”, because that’s only what is true by the definition of classifying topoi!

Vincent R.B. Blazy

]]>I replaced “all the same models in all Grothendieck topoi” by “categories of models in all Grothendieck topoi up to equivalence”, because that’s only what is true by the definition of classifying topoi!

Vincent R.B. Blazy

]]>I have added pointer to this review:

- Steven Vickers,
*Continuity and geometric logic*, Journal of Applied Logic Volume 12, Issue 1, March 2014, Pages 14-27 (doi:10.1016/j.jal.2013.07.004)

I came across this while looking for references that would make explicit the origin/motivation of the terminology “geometric logic” as indeed pertaining to geometry. On this point, Vickers’ text starts out with

The historical roots of this idea must surely go back to Grothendieck’s dictum that “A topos is a generalized topological space”

and then helpfully expands on the justification of the terminology. But do we know where the term actually originates and what the original source offered as motivation/explanation?

]]>Concerning your first point, the model theory of geometric logic in general is only sporadically covered on the nLab. If I find the time I'll add something in the near future, I guess definitions of quotient theory and expansion are also missing. ]]>

Tweaked the wording a bit. I think it would be helpful to give a link explaining the relevant notion of “complete theory”. Also, exactly what theory in FOL are we comparing it to? PA?

]]>Since it is a good illustration of the expressiveness of infinitary disjunctions I’ve expanded the example of the natural numbers.

]]>Added the empty and inconsistent theories as examples, as well as a link to an online version of the Reyes-Makkai monograph.

]]>While providing some interconnections for theory of flat functors I saw that the nLab already had some material on this even in a nicer notation than the one I used in the other entry. Well, I set some pointers.

]]>Added example of flat diagrams, the most general theory of presheaf type.

Steve Vickers

]]>Tidying up presentation of theory of real numbers, to clarify difference between side conditions and sequents.

Steve Vickers

]]>= included in definition of geometric theory.

Steve Vickers

]]>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?

]]>added a pointer to Barr’s theorem to geometric logic (in a new Properties-section)

]]>I think that deserves a longer answer and a wider audience.

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

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

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

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

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?

]]>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?

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

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

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