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.

翻译：我们研究了基于简约逻辑的非良基证明系统，该逻辑是线性逻辑的一种较弱变体，其中指数模态!被解释为有限数据上流的构造子。通过采用标准的进展性准则，在全局层面保持了逻辑一致性。我们提出了一种基于有限逼近的无穷切割消除方法，并证明在进展性准则存在的情况下，该方法在其极限处会返回定义明确的非良基证明。此外，我们证明了切割消除过程保持了进展性准则以及内化证明理论均匀性程度的各种正则性条件。最后，我们基于关系模型为我们的系统提供了指称语义。