Proof-theoretic methods in quantifier-free definability
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910805135458304 |
|---|---|
| author | Kocsis, Zoltan A. |
| author_facet | Kocsis, Zoltan A. |
| contents | We introduce a proof-theoretic approach to showing nondefinability of second-order intuitionistic connectives by quantifier-free schemata. We apply the method to prove that Taranovsky's "realizability disjunction" connective does not admit a quantifier-free definition, and use it to obtain new results and more nuanced information about the nondefinability of Kreisel's and Połacik's unary connectives. The finitary and combinatorial nature of our method makes it resilient to changes in metatheory, and suitable even for settings with axioms that are explicitly incompatible with classical logic. Furthermore, the problem-specific subproofs arising from this approach can be readily transcribed into univalent type theory and verified using the Agda proof assistant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_03640 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Proof-theoretic methods in quantifier-free definability Kocsis, Zoltan A. Logic Logic in Computer Science 03F03 (Primary) 03B16, 03B20 (Secondary) We introduce a proof-theoretic approach to showing nondefinability of second-order intuitionistic connectives by quantifier-free schemata. We apply the method to prove that Taranovsky's "realizability disjunction" connective does not admit a quantifier-free definition, and use it to obtain new results and more nuanced information about the nondefinability of Kreisel's and Połacik's unary connectives. The finitary and combinatorial nature of our method makes it resilient to changes in metatheory, and suitable even for settings with axioms that are explicitly incompatible with classical logic. Furthermore, the problem-specific subproofs arising from this approach can be readily transcribed into univalent type theory and verified using the Agda proof assistant. |
| title | Proof-theoretic methods in quantifier-free definability |
| topic | Logic Logic in Computer Science 03F03 (Primary) 03B16, 03B20 (Secondary) |
| url | https://arxiv.org/abs/2310.03640 |