Re: Internal truth objects

[Sergey Goncharov <Sergey.Goncharov@cs.fau.de>]

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
>
>
>
> 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,
>>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]