[Flirts] An institution of higher-order intuitionistic logic

[Till Mossakowski]

Dear Valeria,

here is an institution of higher-order intuitionistic logic.
But I think it is better to start with the propositional case,
also because the present logic does not deal with Curry-Howard.

Signatures are theories L of intuitionistic type theory, signature
morphisms are theory translations (see Lambek/Scott p.197).
L-Sentences are formulas in the symbols of Th. Sentence translation
is obvious (cf. again p.197).
Models of an intuitionistic type theory L consist of a topos T
and a strict logical functor T(L)-> T from the classifying topos T(L)
of L to T; equivalently, a theory translation t:L->L(T) from L to the
internal language L(T) of T. Model reduction is just composition (using
the latter representation of models).
An L-sentence e satisfies an L-model t:L->L(T), if T |= t(e),
or equivalently, L(T) |- t(e).
The satisfaction condition is trivial, because model reduction
is composition (Meseguer has called a similar thing "categorical logic
institutions", but note that he uses a T that is fixed for all models).
Model morphisms from t:L->L(T) to t':L->L(T') are pairs, consisting of
a functor f:T->T' and a natural transformation mu:L(f) o t -> t'.

Proof terms need to be extracted from the calculus on p.134f. of
Lambek/Scott. I do not spell out the details here, because
they do not do so either. Actually, they do not apply Curry-Howard at
all for this logic. Perhaps there is other work that does.

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