From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7707 Path: news.gmane.org!not-for-mail From: Philip Scott Newsgroups: gmane.science.mathematics.categories Subject: Re: Internal truth objects Date: Sat, 4 May 2013 15:46:14 -0400 Message-ID: References: Reply-To: Philip Scott NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 (Apple Message framework v1085) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1367712796 30878 80.91.229.3 (5 May 2013 00:13:16 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 5 May 2013 00:13:16 +0000 (UTC) Cc: Categories To: Sergey Goncharov Original-X-From: majordomo@mlist.mta.ca Sun May 05 02:13:16 2013 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1UYmZm-00084n-IW for gsmc-categories@m.gmane.org; Sun, 05 May 2013 02:13:14 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:45668) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1UYmYF-0002EI-2R; Sat, 04 May 2013 21:11:39 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1UYmYG-00042j-Cn for categories-list@mlist.mta.ca; Sat, 04 May 2013 21:11:40 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7707 Archived-At: 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/ ]