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.
What do you think about changing
This can be formulated in any doctrine
to:
This notion often exists in many-sorted doctrines
(or similar)?
For instance, Lawvere theories/one-sorted algebraic theories are perhaps the quintessential example of a doctrine, but for which there is no notion of empty theory.
There is a notion of “empty theory” for Lawvere theories: it’s the one where there are no operations except for projections.
If the initial Lawvere theory is intended to be “empty”, then the necessary tweak would be minor. As a counterpoint, though: Lawvere refers to the initial theory as “the theory of equality”, which I think is more apt; the definition of “empty theory” on the nLab page seems appropriate, as you truly can do no equational reasoning with no sorts, whereas you can do something with variable projections, albeit trivial.
I just assumed that was the intention, but now that I look at the entry (“no sorts”), I guess I misspoke. By definition, Lawvere theories in the original sense are uni-typed. But I think the intended doctrine must here be categories with finite products, and the initial such is just the terminal category. I’m not even sure Lawvere theories (in the OG sense) would or should be considered a “doctrine”.
The question becomes: how are we defining “doctrine”?
Yes, exactly. There is no “empty Lawvere theory” in this sense, but when I wrote the page I didn’t consider that a “doctrine” could involve restrictions on the number of sorts. A doctrine to me is rather about the categorical/logical structure. If “one-sorted logic” is a doctrine, is “two-sorted logic” a doctrine? “Logic with seven sorts, three function symbols, eleven relation symbols, and eighteen axioms”?
If “one-sorted logic” is a doctrine, is “two-sorted logic” a doctrine? “Logic with seven sorts, three function symbols, eleven relation symbols, and eighteen axioms”?
I would say yes :) Though there is a distinction in that no-one is ever likely to care about the latter, but people do care about S-sorted logics for fixed S. From a categorical point of view, I don’t think one cares. But from a logical point of view, being able to fix a set of sorts is important, and if these don’t count as “doctrines”, they deserve some other name. (Maybe just “theories”? Though this sounds even more underspecified than doctrine!) I could understand wanting to reserve “doctrine” for constructions of categorical interest, though, in which case it probably doesn’t make sense to fix the sorts.
I think the traditional meaning of “doctrine” has referred only to constructions of categorical interest. I don’t know whether logicians have a name for restrictions placed on the number of sorts.
1 to 8 of 8