Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | https://arxiv.org/abs/2503.19930 |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912904873246720 |
|---|---|
| author | d'Aragona, Antonio Piccolomini |
| author_facet | d'Aragona, Antonio Piccolomini |
| contents | Proof-theoretic semantics (PTS) is normally understood today as Base-Extension Semantics (B-eS), i.e., as a theory of proof-theoretic consequence over atomic proof systems. Intuitionistic logic (IL) has been proved to be incomplete over a number of variants of B-eS, including a monotonic one where introduction rules play a prior role (miB-eS). In its original formulation by Prawitz, however, PTS consequence is not a primitive, but a derived notion. The main concept is that of argument structure valid relative to atomic systems and assignments of reductions for eliminating generalised detours of inferences in non-introduction form. This is called Proof-Theoretic Validity (P-tV), and it can be given in a monotonic and introduction-based form too (miP-tV). It is unclear whether, and under what conditions, the incompleteness results proved for IL over miB-eS can be transferred to miP-tV. As has been remarked, the main problem seems to be that the notion of argumental validity underlying the miB-eS notion of consequence is one where reductions are either forced to be non-uniform, or non-constructive. Building on some Prawitz-fashion incompleteness proofs for IL based on the notion of (intuitionistic) construction, I provide in what follows a set of reductions which are surely uniform (however uniformity is defined) and constructive, and which make the atomic Split rule logically valid over miP-tV, thus implying the incompleteness of IL over a Prawitzian (monotonic, introduction-based) framework strictly understood. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_19930 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Uniform validity of atomic Split rule in monotonic proof-theoretic semantics d'Aragona, Antonio Piccolomini Logic Proof-theoretic semantics (PTS) is normally understood today as Base-Extension Semantics (B-eS), i.e., as a theory of proof-theoretic consequence over atomic proof systems. Intuitionistic logic (IL) has been proved to be incomplete over a number of variants of B-eS, including a monotonic one where introduction rules play a prior role (miB-eS). In its original formulation by Prawitz, however, PTS consequence is not a primitive, but a derived notion. The main concept is that of argument structure valid relative to atomic systems and assignments of reductions for eliminating generalised detours of inferences in non-introduction form. This is called Proof-Theoretic Validity (P-tV), and it can be given in a monotonic and introduction-based form too (miP-tV). It is unclear whether, and under what conditions, the incompleteness results proved for IL over miB-eS can be transferred to miP-tV. As has been remarked, the main problem seems to be that the notion of argumental validity underlying the miB-eS notion of consequence is one where reductions are either forced to be non-uniform, or non-constructive. Building on some Prawitz-fashion incompleteness proofs for IL based on the notion of (intuitionistic) construction, I provide in what follows a set of reductions which are surely uniform (however uniformity is defined) and constructive, and which make the atomic Split rule logically valid over miP-tV, thus implying the incompleteness of IL over a Prawitzian (monotonic, introduction-based) framework strictly understood. |
| title | Uniform validity of atomic Split rule in monotonic proof-theoretic semantics |
| topic | Logic |
| url | https://arxiv.org/abs/2503.19930 |