[Flirts] RE: Curry-Howard isomorphism for Institutions

[Till Mossakowski]

Dear Valeria,

 >>they idea of using sets of sentences as objects is new and useful,
 >>or did we miss something there also?
 > Well, I don't think it is useful, as *when* you can do your
 > categorical modelling properly, sets of sentences are modelled for
 > free, either in the case where there's a connective that internalizes
 > the comma (like a categorical tensor) or using the fibration
 > mechanism. So no, I don't see the usefulness at the moment, it doesn't
 > buy me anything new. Maybe you'd like to expand on that?

For properties like compactness, you need possibly infinite set of
sentences. And many logics do not have infinitary conjunction,
hence you cannot internalize. If then the logic happens to have
infinitary proof rules, I cannot see how to model this by fibrations.
But may be I am missing something again :-).

 >>it does allow defining many basic proof theoretic concepts in a nice 
abstract way,
 > But I don't see these many concepts. Would you like to discuss them 
one by one?

One concept is having not not-elimination, which separates classical
from intuitionistic logic.

> A logic, for me, does not exist without its derivations and proofs.
That's interesting. Strassburger in is paper "What is a logic
and what is a proof" starts with "a logic is a pre-order",
i.e. he omits proofs. Only later proofs come in. And I agree:
there should be a notion of logic with proofs, but a notion
of logic without proofs is useful as well.

>>It seems that there are three levels:
> 
>>1. entailment systems (= kind of pre-orders) 
>>2. categories of sentences and proofs 
>>3. 2-categories of sentences, proofs and proof reductions.
> Not quite. One can and normally does talk about proof reductions using simply categories and morphisms.
> You do not need to introduce 2-cells for that.
I do not understand.
I thought formulas = objects, proofs = 1-cells. So what are
proof reductions other than 2-cells? OK, they might just be
a pre-order on 1-cells. But this just amounts to having
thin Hom-categories.

>>This seems to be related to polycategories, which, however, only use finite sequences of sentences.
> Yes, indeed in the kind of proof theory I like, rules mostly have a finite number of hypotheses/assumptions. Girard says somewhere that the infinite is always a potential one, which I think is quite nice.
I definitely want to include infinite sets of sentences as well.
The whole notion of compactness as studied in traditional logic
only makes sense with infinite sets of sentences.
And ZFC, which is widely used in mathematics, is not finitely
axiomatizable. Neither is first-order Peano arithmetic.
Infinitary rules are less important, but it would be nice not
to exclude them, because they are used occasionally.
Moreover, the framework of institutions with proofs should be
philosophically neutral, and should admit the study of logics
that might be rejected by some people, but not by all.

>  The modularity there is another one of the success criteria, right?
Yes, certainly.

Greetings,
Till

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