Core type theory I: implication and negation

David Ripley (Monash University)

Dave Ripley (Monash) will present "Core type theory I: implication and negation" at 11 on 19 October in Old Quad G10.

Abstract: In a series of papers and books spanning four decades, Neil Tennant has developed a logical system first called "intuitionist relevant logic" and more recently "core logic". Core logic is a relative of intuitionistic logic, but is weaker in distinctive ways having to do with its handling of contradictory sets of formulas, and its requirement that all proofs be normal.

Tennant has offered a variety of motivations for core logic, among them claims to its benefits for *computational* approach to logic. In this vein, Tennant has emphasized features of *proof search* in core logic. However, there is another natural way to connect logics to computation, based on the *Curry-Howard correspondence* between proofs and programs, and between proof normalisation and program execution. This presentation develops a typed term calculus that relates to core logic in this way. (I restrict my attention here to the implication-negation fragment of core logic.)

If core logic is known for a single feature, it's that it's not closed under the rule of *cut*. Indeed, it is often dismissed on exactly these grounds, since closure under cut is often seen as a necessary condition for a logic to be sensible at all. For example, Girard has said that "a sequent calculus without cut-elimination is like a car without [an] engine". The analogy here turns again on the Curry-Howard correspondence, in particular the correspondence between cut-elimination procedures for a logic and computation (reduction) in its corresponding term system. By examining the term system to be presented here, however, I will argue that core logic already contains a perfectly working engine; the connection Girard is pointing to might be important, but it does not actually require cut. 

In addition, the term calculus to be presented here violates several of the usual theorems typically proved for such systems. (These are again connected to core logic's failures of cut.) And yet calculation in this calculus proceeds largely unimpeded. There are thus potential lessons here for type theories as well; new ways to arrive at workable systems.