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.
1 to 6 of 6
On the page essentially algebraic theory, a syntactic description of essentially algebraic theories is given, in terms of a set of sorts, a set of operations (each labelled as from finitely many input sorts to one output sort, and furthermore as either “total” or “partial”), for each partial operation a set of equations between total operations on the appropriate sorts defining its domain, and a set of equations holding universally.
Suppose we further demand each of the sets above be finite, as we would expect of any “human-writable” theory (for example, as in the theory of categories). Is there a name for this particular kind of essentially algebraic theory? (I would imagine it corresponds to the finitely presented objects in the category of finite-limit categories).
Also, given such a theory T and a W-pretopos V, is it necessarily the case that there is, internal to V, an initial model of T? My intuition suggests this is true and straightforward (surely the syntactic construction of the free model of T can be given via the inductive types found in a W-pretopos), but it’s hard to find references on such things.
I would just call this a ‘finitary’ essentially algebraic theory.
I worry that may be interpreted only as re-emphasizing that the operations are finitary (i.e., that we are using finite limits rather than arbitrary limits); indeed, in a quick Google for “finitary essentially algebraic theory”, I can only find it being used in this way. I don’t think I could use that phrase to clearly indicate an exclusion of theories such as “There is a single sort S, and a sequence of binary operations c_0, c_1, c_2, …, on it”.
But, of course, it may well be that there is no commonly used phrase describing the notion I have in mind.
Yes, you're right. Perhaps ‘finite’ (instead of ‘finitary’) works.
I think the Elephant uses “finitely presented theory” in a similar context.
Your second question in #1 is interesting. One does sometimes run into issues with free algebras for theories that have axioms, of course, but I’m not sure whether that can happen when everything is finite.
If you think of an algebraic theory as itself an algebraic sort of thing, presented by sorts, operations, and axioms, then ‘finitely presented’ makes a lot of sense.
1 to 6 of 6