Higher-order, multi-sorted, non purely equational version of universal algebra ?

2010-03-11T04:27:12Z

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.

Answer by Neel Krishnaswami for Higher-order, multi-sorted, non purely equational version of universal algebra ?

2010-03-11T15:19:31Z

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

Higher-order, multi-sorted, non purely equational version of universal algebra ? - MathOverflow

Higher-order, multi-sorted, non purely equational version of universal algebra ?

Answer by Neel Krishnaswami for Higher-order, multi-sorted, non purely equational version of universal algebra ?