Edward Haeusler

Indexed and Fibred category theory have a long tradition in computer science as a language to formalize different presentations of the notion of a logic, as for instance, in the theory of institutions and general logics, and as unifying models of logic and type theory as well. Here we introduce the notions of indexed and fibred frames and construct a rich mathematical workspace where many relevant and useful concepts of logics can be elegantly modelled. To demonstrate the applicability of these tools, essential ideas around the theory of institutions are recasted and described

We present a categorical/denotational semantics for the Lambek Syntactic Calculus, indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product corresponds to a noncommutative bi-endofunctor into a category, which encloses all categories of such hierarchical structure. A soundness theorem for LSC is shown with respect to this semantical framework.

Sambin [6] proved the normalization theorem for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45