Internal truth objects

Internal truth objects

[Sergey Goncharov]

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

FAU Erlangen-N?rnberg         Phone: +49-91-3185-64031
Chair for TCS                 Fax:   +49-91-3185-64055
Wetterkreuz 13                Email: Sergey.Goncharov@cs.fau.de
D-91058 Erlangen              Web:   http://www8.cs.fau.de/~sergey


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

Re: Internal truth objects

[Philip Scott]

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

Re: Internal truth objects

[Sergey Goncharov]

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

Re: Internal truth objects

[Patrik Eklund]

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