Infinitary Cut-Elimination for Non-Wellfounded Parsimonious Linear Logic

TL;DR

This paper develops an infinitary cut-elimination process for non-wellfounded proof systems in parsimonious linear logic, ensuring consistency and regularity preservation, with a relational model semantics.

Contribution

It introduces an infinitary cut-elimination method for non-wellfounded parsimonious linear logic, maintaining proof regularity and providing a denotational semantics.

Findings

Infinitary cut-elimination converges to well-defined proofs.

Cut-elimination preserves the progressing criterion and regularity conditions.

A relational model semantics is established for the proof system.

Abstract

We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressive criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.