Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

I have been looking around, unsuccessfully, for generalizations of universal algebra based on higher-order logic (rather than first order) and where the relations are not purely equational. Motivation: I need a "theory of syntax" for presentations of higher-order, non-equational theories. Furthermore, I want to be able to specify 'combinators' over these presentations, rigorously.

I am aware of Lawvere theories, but these are still equational (and neither particularly higher-order, though the multi-sorted generalization seems straightforward enough). There is a beginning of model theory done in a logical independent way, i.e. model theory over an institution; but that seems to concentrate on the model-theoretic aspects, rather than the universal algebra aspects. Perhaps what I am looking for are sketches?

[Edit:] From the various answer below, it seems I should be asking the question "how can I view type theory as a theory of syntax"? Somehow, that seems like an 'implementation' (as it requires a fair bit of 'encoding'); for example, to express the 'theory of categories' [i.e. (Obj, Mor, id, src, trg, $\circ$) and 5-6 axioms, I need a dependent record. Plus what is a sort (and sort constructor for Mor), what is an operation, and what is in Prop? Universal algebra cleanly separates these.

A good question was asked: what theorems do I want? Well, whatever operations I make on theories, well-formedness of the results will require discharging some obligations -- these obligations should all be finitely expressible (and automatically well-formed). Furthermore, the resulting syntactic objects and their morphisms should form a finitely co-complete category. Note that I expect that deciding if a given (presentation of a ) theory has a model to be undecidable.

share|improve this question
Is "universal algebra based on higher order logic" any different from type theory? In addition to what you mentioned, you might want to check out classifying topoi (see Sheaves in Geometry and Logic by MacLane and Moerdijk). Otherwise, you might find what you need in Introduction to Higher Order Categorical Logic by Lambek and Scott. –  François G. Dorais Mar 11 '10 at 4:52
I have many suggestions which address one or more parts of your question, but I don't see a generalization which does not seem more model-theoretic than universal-algebraic. Could you tell us what theorems such a beast might have? Perhaps a Birkhoff theorem analogue or at least a high-order homomorphism theorem? Also, if combinators are a large part of the goal, perhaps you should look at some form of combinatory or algebraic logic? Gerhard "Ask Me About System Design" Paseman, 2010.03.10 –  Gerhard Paseman Mar 11 '10 at 4:53
[Some people][1] say that all type theories can be expressed as quasi-equational theories (also called "essentially equational"). Perhaps these are enough for you? [1]: wms2.andrew.cmu.edu:81/nmvideo/SCS_lecture2b-4-10-hint.mov –  Andrej Bauer Mar 11 '10 at 9:09
Thank you all - I have edited my question with respect to these comments. And I am watching that video now. –  Jacques Carette Mar 11 '10 at 14:40
add comment

1 Answer

up vote 3 down vote accepted

Lawvere theories generalize to higher-order logic in a straightforward way. A first-order hyperdoctrine is a functor $\mathcal{P} : C^{\mathrm{op}} \to \mathrm{Poset}$ where $C$ has products and is used to interpret terms in context, plus a small herd of conditions to make substitution and quantifiers work out right.

If you want a hyperdoctrine that can interpret higher-order predicate logic, what you additionally want is to (a) require $C$ to be cartesian closed, and (b) $C$ should have an internal heyting algebra $H$ with the property that for each $X$ in $C$, $\mathit{Obj}(\mathcal{P}(X)) \simeq C(X, H)$. Basically, $H$ models the sort of propositions, and the cartesian closure lets you freely interpret lambda-terms denoting predicates and relations. The bijection $\mathit{Obj}(\mathcal{P}(X)) \simeq C(X, H)$ tells you that the morphisms into $H$ actually do correspond to truth values in context $X$, so you can interpret a higher-order term by interpreting a proposition in $\mathrm{Poset}$ via the functor $\mathcal{P}$, and then transporting it back into $C$.

(I would have made this a comment, but it was too long.)

share|improve this answer
This feels like an answer to me - as do some of the comments above. At least they are pointing me in a number of (hopefully fruitful) directions to look in. –  Jacques Carette Mar 11 '10 at 15:25
Of course, this notion of "higher-order hyperdoctrine" is almost the same as "elementary topos"; that is, a topos is just one of these higher-order hyperdoctrines in which furthermore \mathcal{P}(X) must be the poset of subobjects of X (thus, it has "comprehension"). Moreover, any higher-order hyperdoctrine can be augmented to one with this comprehension property by simply adding objects for each existing predicate and morphisms for provably functional relations, without changing the action of P on those objects and morphisms which already exist. (Uh-oh, comment limit. Well, that's enough.) –  Sridhar Ramesh Mar 16 '10 at 21:16
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.