FOM: IHOL and topoi are not isomorphic, but related

[Till Mossakowski]

On Jan 31st, Stephen G. Simpson wrote:
>Since Awodey hasn't
>specified the category that he is talking about, it's hard to tell
>what he means by "isomorphic".  Note also that "theory" has an unusual
>meaning for topos people; see Makkai/Reyes.

So the question is what is the right category to use when claiming
that IHOL = topos theory.
May I make the following suggestion:
Since we are talking about logic, we should use a category
of logics. Now there is a paper by J. Meseguer, "General logics",
Logic Colloquium 1987, where such a category is defined. (Barwise's
abstract model theory is similar to that, but as far as I remember
he does not define translations between logics.)
Such a "logic" has to define notions
  of signature (for the non-logical symbols),
  of sentence,
  of (proof-theoretic) entailment, 
  of model, and 
  of satisfaction.
With this, there are derived notions of theory, soundness,
completeness etc.
An "entailment system" forgets about model theory, so
only the first three components are given.
There are also notion of map between logics and entailment
systems, leading to appropriate categories.

Now IHOL clearly is an entailment system. It also can be
extended to a logic, but then one has to specify
a model theory (there are at least two options
differing non-trivially: Kripke models and topoi).
So let's stay with entailment systems.

Topos theory, on the other hand, is not an entailment system,
but it is a *theory*, lets call it ToposTheory, formulated in essentialy 
algebraic logic (ESS_ALG).

The result cited by Awodey shows that 
* (something like) the category of IHOL-theories and 
* the model category of ToposTheory in ESS_ALG
are equivalent.
Thus IHOL-*theories* correspond to ToposTheory-*models*.
This switchting of levels between syntax and semantics
causes the problem that you get some 
"maximal extension by definition" when translating
an IHOL-theory to a topos and then go back.
This process of semantical abstraction cannot be called an
isomorphism in my eyes. I would compare it with the process 
of forming a monad or an algebraic theory from an equational
presentation, or with forming a Lindenbaum algebra from 
a propositional theory.
Nevertheless, such a semantical abstraction may be very
useful.

If we want to stay at the syntactical level, from the results
in the book by Lambek and Scott we get the following:
There is a convervative map of entailment systems 
from IHOL to essentialy algebraic logic. That is, 

     T |-^{IHOL} \phi

is equivalent to

     TOPOS_THEORY + Translate(T) |-^{ESS_ALG} Translate(\phi)

But there hardly will be an isomorphism of entailment systems,
nor one of logics (ESS_ALG probably can be easily embedded into
IHOL, but this does not help here).

Nevertheless, the above result is very interesting, since it faithfully
embeds IHOL into ESS_ALG, which is a rather simple logic
(just Universal Horn formulae for partial algebras).

So, lacking an isomorphism, we are back to Simpson's statement:
>Topos people seem to think that if there are translations of X into Y
>and Y into X, then X and Y are identical, i.e. the same subject.  This
>is completely incorrect.

Surely. But it may be very well the case that there is a translation
of X into Y which has so many interesting and pleasing properties
that some very tight connection between X and Y is revealed.

>To give a mathematical example, there are
>translations of group theory into ring theory (via "group rings") and
>vice versa, but this doesn't mean that group theory is identical to
>ring theory.  The motivation and the questions considered are very
>different.

I feel that the semantical abstraction from IHOL to topos theory,
and also the embedding of entailment, reveal a connection
between IHOL and topos theory that is much closer than that
between group theory and ring theory. I also think that
the connection between IHOL and topos theory is deeper,
just because it was revealed and could not be derived
from motivations being the same.
I don't know if the connection is strong enough to make
topos theory relevant for f.o.m. - I am an expert on 
neither IHOL nor topos theory ...
... but at least I can say that I was very impressed by the results
of the Lambek and Scott book.

Till Mossakowski