[Flirts] Lawvere/cat institutions (was Re: Your paper Proof)

[Till Mossakowski]

Hi Razvan,

I have just discussed with Florian Rabe the problem he
discovered in your freely generated proof systems.
I think that the restriction to injective sentence translations
is not very beautiful. I suggest to take another solution:

Revise the notion of institution with proofs.
 From the discussions with Joseph when he visited us in Bremen
I learned that we should consider institutions to be
a rather general notion. That is, extending the terminology
of our universal logic paper, we have X/Y-institutions,
where X and Y are categories (with forgetful functors
to Set).
So far, we have considered Y=Cat and X a category of certain
categories having a power set as its set of objects.
Now to solve the problem Florian discovered, it suffices
to use the power-multiset instead. But this still is
not very algebraic. Now my colleague Lutz Schröder has the idea
to use any category that is generated by (arbitrary set-indexed)
products from a given set of objects (called "sentences").
This has the drawback that products are not necessarily
uniquely decomposable into their component sentences.
Eventually, in discussion with Lutz, we arrived at the
following, in a sense offering a new variant of
the Curry-Howard isomorphism:

        proof categories are many-sorted Lawvere theories

Now a single-sorted finitary Lawvere theory is a product-preserving
object-bijective functor from N^{op} to P, where N is the
category of finite ordinals  (considered as a subcategory of Set)
and P is any category.(of "term tuples").
A many.sorted Lawvere theory (without rank) is a product-preserving
object-bijective functor from Fam(S)^op to P, where Fam(S) is the free
category with coproducts over a set S of generating objects, which can
be shown to be isomorphic to the comma category (Set,S) of families
phi:X->S of elements of S (where X is an arbitrary index set).
(Coproducts are constructed by taking coproducts of index sets.)
Such a family is nothing but an S-sorted system of variables,
a proof judgement hence is a variable context!
This nicely corresponds to the intuition (guided by many examples,
and also by the standard interpretation of algebraic theories
as Lawvere theories) that P (the category of proofs) has as morphisms
tuples of terms with variables, where the variable context is given by
the source proof judgement.

Note that if we have a sentence psi, the projections
pi1,pi2: psi x psi -> psi
are retractions with one-sided inverse <id,id>, but this in
general is not an isomorphism. This exactly yields the
difference between psi and psi x psi needed for the
non-injective sentences translations.

I am much more convinced by this new definition than by the
old one, also independently of the problem that Florian has
raised. I therefore propose to adopt this new definition
in subsequent work.

By the way: all the best for the winter days and a happy new year!

Greetings,
Till


Razvan Diaconescu wrote:
> Hi Florian,
> 
> Thank you for your message. Excuse me for replying not so soon. It
> took me a while to reflect upon this issue and I am also not very
> quick anyway. 
> 
>  |But I ran into problems when I considered non-injective sentence
>  | translations. After some tries I settled with an unsatisfactory
>  | construction that appeared to be the best possible choice. I wanted
>  | to see how you solved the problem, but my impression is that you
>  | have not solved it either. 
> 
> You're right, this is a gap. Thank you for discovering this. It is a
> very interesting fact.
> 
>  |Am I missing something? If so, can you tell me what it is? If not, I
>  |  would like to know your opinion on how to adapt the construction. 
> 
> After some serious reflection these are my conclusions. The issue of
> free proof systems requires to allow only injective signature
> morphisms (then injectivity of sentence translations follows).
> Notice that this is very consistent to traditional logic practice. 
> Although I was quite disturbed by this conclusion at the beginning
> because of my strong background in algebraic specification (where
> non-injective signature morphisms play an important role), I think
> this is an important insight in the nature of proof theory. We have to
> accept it as a fundamental truth.
> 
> To resume there are basically 3 choices.
> 
> 1. Restriction of signature morphism to injective ones.
> 2. Relax the concept of proof system by not considering proof
>    translations anymore.
> 3. Abandon the idea of free proof systems.
> 
> Now my mind is very clear about all these, only 1. is acceptable.
> 2. is not acceptable for many reasons, one of them is that it does
> make sense structurally. As mathematician I would discard it
> immediately.
> 3. does not make sense either, because this is what the actual proof
> systems are. If you look at FOL from a true logical perspective (in
> the tradition of Godel, Tarski, Birkhoff which maintains a good
> balance between semantics and proof theory), then we can easily
> understand this point. As I am teaching logic to my students, I cannot
> find any other reasonable way to present them the proof systems of
> FOL, EQL, etc.
> 
> Finally, it seems to me that 1. applies directly only to Thm 3.12, the
> other results of the paper do not require it. Do you agree?
> 
> All the best,
> Razvan


-- 
Till Mossakowski               Phone +49-421-218-4683
Dept. of Computer Science      Fax +49-421-218-3054
University of Bremen           till at tzi.de
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till