Least and Greatest Fixed Points in Linear Logic

TL;DR

This paper introduces muMALL, an extension of linear logic with fixed point operators, establishing its proof-theoretic properties and potential applications to automated proof search.

Contribution

It adds least and greatest fixed point operators to linear logic, proving weak normalization and designing a complete focused proof system.

Findings

muMALL satisfies weak normalization

A complete focused proof system for muMALL is developed

Foundations are applied to intuitionistic logic

Abstract

The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call muMALL, satisfies two fundamental proof theoretic properties: we establish weak normalization for it, and we design a focused proof system that we prove complete. That second result provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We show how these foundations can be applied to intuitionistic logic.