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 On 2013-05-03, at 11:46 AM, Sergey Goncharov wrote:
Dear categorists,
A standard method for doing logic in category theory is, as far I as know, by imposing more and more conditions on the subobject posets Sub(X), which are equivalence classes of monomorphisms with X as the codomain.
By adding more and more assumptions of this kind one gets more and more powerful internal logics. The connection between predicates and functions does not arise in all these stages as long as one does not request existence of the subobject classifier (therefore almost certainly turning the whole thing into a topos).
What I am wondering about is whether an alternative approach have ever been developed, namely by postulating an internal truth-value object Omega, by introducing predicates as exponentials Omega^X, and so forth.
I would expect, if such an idea have ever been developed it would yield one of the many ways to provide foundations to the topos theory. The fact that is not well-known sort of indicates that it is probably not such a robust idea, in which case I would be grateful if someone would explain me why.
The only approach to topos theory I know, which might be relevant here is the one by allegories. Starting from a category C with a distinguished object Omega (say, internal Heyting algebra) we can introduce an allegory having the same object as C and as morphisms A->B those of C having form A x B -> Omega. Antiinvolution would then follow by swapping the arguments, and the intersection can be made deducible from the axiomatic structure of Omega. The question is, of course, the modular law, and the conditions under which it would follow. Has anyone studied that?
I would be very grateful for any hints and/or references on the subject.
Best regards,
-- Sergey Goncharov, Assistant Professor
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]