Higher-order, multi-sorted, non purely equational version of universal algebra ? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-21T20:20:18Z http://mathoverflow.net/feeds/question/17822 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/17822/higher-order-multi-sorted-non-purely-equational-version-of-universal-algebra Higher-order, multi-sorted, non purely equational version of universal algebra ? Jacques Carette 2010-03-11T04:27:12Z 2010-03-11T15:19:31Z <p>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.</p> <p>I am aware of <a href="http://en.wikipedia.org/wiki/Lawvere_theory" rel="nofollow">Lawvere theories</a>, 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. <a href="http://en.wikipedia.org/wiki/Institutional_model_theory" rel="nofollow">model theory over an institution</a>; but that seems to concentrate on the model-theoretic aspects, rather than the universal algebra aspects. Perhaps what I am looking for are <a href="http://en.wikipedia.org/wiki/Sketch_%28mathematics%29" rel="nofollow">sketches</a>?</p> <p>[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.</p> <p>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.</p> http://mathoverflow.net/questions/17822/higher-order-multi-sorted-non-purely-equational-version-of-universal-algebra/17873#17873 Answer by Neel Krishnaswami for Higher-order, multi-sorted, non purely equational version of universal algebra ? Neel Krishnaswami 2010-03-11T15:19:31Z 2010-03-11T15:19:31Z <p>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. </p> <p>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$. </p> <p>(I would have made this a comment, but it was too long.) </p>