OIL seminar (1996)

January 10, 1996
Title:: A sequent calculus for compact closed categories
Speaker:: Masaru Shirahata (JAIST)
Abstract:: In this talk, we introduce a system of sequent calculus, which is equivalent to MLL with tensor and par identified, and study its interpretation in compact closed categories. We first review the elements of category theory and the correspondece between linear logic and symmetric monoidal closed categories. We then consider compact closed categories and introduce a system of sequent calculus for them with a very simple cut-elimination. Finally, we study the categorical interpretation of the cut-elimination procedure through the coherence result for compact closed categories by Kelly and Laplaza.

January 17, 1996
Title:: EMBEDDINGS OF INTUITIONISTIC AND CLASSICAL LOGIC INTO LINEAR LOGIC AND THEIR APPLICATION TO PROOF THEORY
Speaker:: Harold Schellinx (University of Utrecht)
Abstract:: We will discuss some mappings of intuitionistic and classical logic into linear logic: exponential (i.e. modal) translations that naturally present themselves when one inductively transforms LJ- or LK-proofs into proofs in linear sequent calculus with the same 'skeleton'. These 'decorative' (or 'plethoric') embeddings use a lot of exponentials and in fact it turns out that not all of these are necessary in order to obtain translations of intuitionistic and classical into linear logic which are sound- and faithful with respect to provability. These more economical (or 'stringent') embeddings however do not define inductive 'decorations' of LJ- and LK-proofs. They do however suggest restrictions on the form of rules in (intuitionistic and classical) sequent calculus, restrictions that are complete for provability. We will introduce these restrictions and show how ordinary proofs can be 'projected' onto the space of restricted proofs, thus giving rise to proof-systems for classical and intuitionistic logic from which a lot of 'redundant' proofs have been eliminated.

January 24, 1996
Title:: On logics with co-implication
Speaker:: Frank Wolter (JAIST)
Abstract:: As a rule logicians (as well as normal people) prefer the truth if compared with the false. This may be the reason for the fact that there are nearly no established non-classical systems with a co-implication while all of them have the implication connective. In my talk I will try to convince you that the false, and hence the co-implication, is not so bad.

January 31, 1996

Title:

A Propositional Logic with Explicit Fixed Points

Speaker:

Y.Suzu-Ki (JAIST)

Abstract:

This paper is written by Albert Visser in Studia Logica 40,pp155-174,1981. I will introduce the contents of this paper in OIL seminar.

Visser studied a logic,which is called Formal Propositional Logic(FPL) and where interpretating implication as formal Provability.He also gave Natural Deduction-style proof system and Kripke Semantics,and proved its soundness and completeness. A property of FPL is that FPL does not have Modus Ponens as a rule in proof system.

In this seminar, we will give the Basic Propositional Logic(BPL) and its semantics,next,show its soundness and completeness and last explain about FPL.FPL is given as extended BPL. I will explain the contents to section 3 in the paper.

Today, my research interest is related to BPL. I hope that I have a chance to explain about BPL in future.Anyway, this is my first talk about BPL in OIL-seminar.

February 7, 1996