Infinitary cut-elimination via finite approximations (extended version)
| Autor: | Acclavio, Matteo, Curzi, Gianluca, Guerrieri, Giulio |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: Extended version of the paper "Infinitary cut-elimination via finite approximations" accepted at CSL2024 |
| Databáze: | arXiv |
| Externí odkaz: |
|