Dear All, The question about "logic 'in' category" sounds very "internal" and indeed toposes (or topoi, whichever you prefer) come to mind. Subobject classifiers and truth values dominate, and it first looks very propositional and then quantifiers are rediscovered. So its rediscovering first-order 'in' some category, where cartesian closedness as a criteria already "rings a bell". On the other hand, if we replace 'in' more with 'with' or 'over', logic with/over categories, work using category theory as an overall metaalanguage for logic is e.g. seen in Goguen's (and Burstall's etc.) institutions and Meseguer's entailment systems (general logic). This approach then creates the category of logics, and morphisms between logics is interesting. Concerning types, type constructors are tricky as they are usually left out of some signature, so type constructors is a "meta business", and modern type theory looks they way it does because of this. There are e.g. informal notions like "soft typing", and many many other similar notions for 'extended' types, whatever that means. Having type constructors then outside the machinery, leaves room for ad hoc stuff, and we run the danger of mixing meta and object languages. The signataure is interesting and we do have the category of signatures. Arities and sorts can be handled categorically, e.g. the way Benabou did on schemes. In a recent paper we extended that to term monads over monoidal biclosed categories, so the sort object must be distinguished from the actual set of sorts. A term functors can be inductively constructed, that is really 'constructed' and not just inductively and verbously imagined, We have a recent paper http://www.sciencedirect.com/science/article/pii/S0165011413000997 where we also and maybe mainly deal with the type constructors in levels of signatrures. We e.g. show how the informally described 'set of lambda terms' can be more formally constructed. Some or actually many say that the definition of lambda terms is elegant, but it is nevertheless not strictly mathematical, certainly not categorical. We tried to do that, and we think it looks fine. We are building some more stuff upon those observations. Apart from having those few remarks on lambda calculus we also briefly look at Sch?nfinkel, Curry and Church (1920-40) in these notations. For instance Church's iota and o are interesting. One of them we know what it is, the other one is still unclear, and modern type theory never bothered to look at it. "Propositions as types" looks very interesting and appealing when you intuitively understand it, but when you develop the math for it, it easily becomes mostly mathematics fiction. If we are dealing with foundational issues, things must be very precies. If we only go for constructions in functional languages, the underlying mathematics is more fictive. The reason why we published that paper 'fuzzy' is that we go 'over' certain categories e.g. to decide where actually to represent uncertainties. So we kind of "internalize" the representation of uncertainty, but not the logic a la topoi. Needless to say, the difference between one-sorted and many-sorted is non-trivial, even if some say it is trivial, but they mostly look at a signature as an end-point with respect to formal treatments of types, not a beginning point. Opetopes things seem go in nice directions, and we need to look more into it. For instance, the category of signatures over a monoidal biclosed category appears to be a monoidal biclosed category in some case at least. We didn't check it, but we have looked at "Kleisli over Kleisli" in a similar fashion (so has Manes), and "composing algebras" is suddenly a possible notion on the Eilenberg-Moore side. Composing with the term functor is one way to provide uncertainty modelling, and having term functors over categories carrying uncertainty building blocks is another way. We prefer to say intuitively that there is a distinction to be made between "fuzzy computing" and "computing with fuzzy". All this distinguishes our approach from Goguen and Meseguer in that we do not have an abstract Sign category, nor an abstract Sen functor (yet to be defined), but they are more specific given underlying specific signatures. So substitution, in a more general sense remains in focus. In the paper we so far deal only with signatures and terms, so we are now indeed looking into sentences. Obviously, axioms, inference rules and theories must follow also for all this to make more sense. If we look at first-order, quantifiers are indeed very tricky, and there are many fundamental questions related to the fons et origo birth of first-order logic. Every logician and almost every categorist has created their own view on this. For propositional logic, a proposition is more clearly a term, whereas moving to predicate logic, a predicate becomes a sentence, and in Horn clauses, atomic formulas are distinct from non-atomic ones. And so on and so forth. If anyone wants to know more, just let us know. Cheers, Patrik On Mon, 6 May 2013, Sergey Goncharov wrote:
Dear Philip,
thank you for your answer and for the useful references. A Dogma is indeed the right thing, precisely what I had in mind. At least, now I know the name for this thing.
The question is only that if a category at hand already has a candidate for Omega (e.g. externally complete Heyting algebra), what would be easy-to-check conditions that it is a dogma w.r.t. that Omega. Or, alternatively, what would be constructions for creation dogmas from other dogmas. I bet, no one has bothered to investigate this issue.
Best, Sergey
On 04/05/13 21:46, Philip Scott wrote:
Dear Sergey: this was explored a bit in the early days of categorical logic. The key topos isomorphism Sub(A) \iso Hom(A,\Omega) combines two possible viewpoints (of course, Bill Lawvere was a key figure in both developments): the LHS (as you point out) considers categories with distinguished "logical" structure imposed on the subobject posets (and quantifiers arising as adjoints): e.g. the work of Makkai-Reyes-Joyal, et.al (see, for example, Makkai-Reyes' book "First-Order Categorical Logic, SLNM 611, where one sees a discussion focussed on Regular Categories, Heyting Categories, etc.). On the other hand, the right hand side is based on looking at appropriate categories with an object \Omega and distinguished logical structure, giving a "theory of types". These categories model (intuitionistic as well as classical versions of) Russell's type theory. This viewpoint was developed for example in early work of Hugo Volger (on "semantical categories" of various kinds) and in Lambek's "Dogmas" (for the latter, see Lambek's article "From Types to sets" in Advances in Math [1980]. )
For Lawvere's discussions on these matters, see his two introductions (to SLNM 445 "Model Theory and Topoi", ed. by Lawvere, Maurer, and Wraith [1975], where Volger's works appeared, along with other early workers ) and Lawvere's introduction to SLNM 274). See also Lawvere's introduction [2006] to the reprinted version of "Adjointness in Foundations" on the TAC webpage). More early history (from the 1970's) is discussed in the historical comments at the end of Part II of my 1986 book with Lambek (Introduction to Higher Order Categorical Logic) as well as several books in topos theory (e.g. Johnstone's books).
Of course Lawvere's early categorical logic papers ("Adjointness in Foundations", "Equality in Hyperdoctrines", etc.) inspired numerous other directions in categorical logic leading to other kinds of structures beyond "Dogma-like" categories, which you asked about. [For this, I'll just mention the keywords and let you look up the individuals involved: indexed categories and fibrational approaches to categorical logic, categorical models of polymorphism, and (most recently) dependent (Martin-Lof) type theory and homotopy lambda calculus].
Cheers, Philip Scott
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]