Re: Internal truth objects

[Philip Scott <phil@site.uottawa.ca>]

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/ ]