Peano Arithmetic and $μ$MALL
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916928507871232 |
|---|---|
| author | Manighetti, Matteo Miller, Dale |
| author_facet | Manighetti, Matteo Miller, Dale |
| contents | Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose to use $μ$MALL as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative-additive linear logic (MALL) with the addition of the logical connectives universal and existential quantifiers (first-order quantifiers), term equality and non-equality, and the least and greatest fixed point operators. We first demonstrate how functions defined using $μ$MALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into $μ$MALL, we obtain $μ$LK+, a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for $μ$LK+ (including cut-elimination and the completeness of focusing), we prove that $μ$LK+ is consistent and that it contains Peano arithmetic. We also prove some conservativity results regarding $μ$LK+ over $μ$MALL. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2312_13634 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Peano Arithmetic and $μ$MALL Manighetti, Matteo Miller, Dale Logic in Computer Science Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose to use $μ$MALL as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative-additive linear logic (MALL) with the addition of the logical connectives universal and existential quantifiers (first-order quantifiers), term equality and non-equality, and the least and greatest fixed point operators. We first demonstrate how functions defined using $μ$MALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into $μ$MALL, we obtain $μ$LK+, a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for $μ$LK+ (including cut-elimination and the completeness of focusing), we prove that $μ$LK+ is consistent and that it contains Peano arithmetic. We also prove some conservativity results regarding $μ$LK+ over $μ$MALL. |
| title | Peano Arithmetic and $μ$MALL |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2312.13634 |