FOM: P.S. Boolean rings and Boolean algebras

[Till Mossakowski]

There may be an objection to the isomorphisms between
Boolean algebras and Boolean rings, either taken as
isomorphism of model theories, or as isomorphism
of induces clones, monads or whatsoever: namely
these are not isomorphisms in a "syntactic" or
proof-theoretic sense.

Vaughan Pratt compares closure of theories under logical consequence
with closure of signatures under derived operations.
Now these closure are infinite objects. Thus, they are beyond the
borderline of proof theory (to be precise, beyond the realm 
recursive formal languages and partial recursive functions and 
recursively enumerable sets over them).

But you can define a notion of theory interpretation between
theories. With a suitable notion of theory interpretation
(say, f:T1-->T2 if both T1,T2 have the same signature and 
the axioms of T1 can be proved from the axioms of T2),
two theories have the same closure under logical consequence
iff they are isomorphic in the category ThInt of theory interpretations.
Thus, "having the same logical consequences" can be captured
by isomorphism in a "proof theoretic" category.

Now the question is:
Can the notion of "having the same derived operation
symbols" (i.e. inducing isomorphic clones, monads, or algebraic
theories) also be captured by isomorphism in some
"proof theoretic" category?

Note that the obvious category one can thank of, the category
ThDerived of theories with "derived theory morphisms", which may
map n-ary operation symbols of T1 to terms in n variables over T2, 
is not appropriate here.
One has to take a quotient of this category, identifying
all morphisms between two objects. Then isomorphism
in this category means "having the same derived operation
symbols".

One can argue that taking this quotient is no longer
proof theoretic. But the situation is quite the same
for ThInt above: it is a quotient of a category of theories
and *proofs* of interpretations.
Both quotients amounts to some existential quantification
(over proofs or derived theory morphisms),
which is not recursive in general, but is still recursively
enumerable.

So if theories with the same logical consequences are taken
to be isomorphic (say, different axiomatizations of ZFC), 
why not also theories with the same derived operations?

Till Mossakowski