Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2412.03251 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910726964117504 |
|---|---|
| author | Indrzejczak, Andrzej Kürbis, Nils |
| author_facet | Indrzejczak, Andrzej Kürbis, Nils |
| contents | We present a sequent calculus for first-order logic with lambda terms and definite descriptions. The theory formalised by this calculus is essentially Russellian, but avoids some of its well known drawbacks and treats definite description as genuine terms. A constructive proof of the cut elimination theorem and a Henkin-style proof of completeness are the main results of this contribution. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_03251 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Cut-free, Sound and Complete Russellian Theory of Definite Descriptions Indrzejczak, Andrzej Kürbis, Nils Logic in Computer Science Logic We present a sequent calculus for first-order logic with lambda terms and definite descriptions. The theory formalised by this calculus is essentially Russellian, but avoids some of its well known drawbacks and treats definite description as genuine terms. A constructive proof of the cut elimination theorem and a Henkin-style proof of completeness are the main results of this contribution. |
| title | A Cut-free, Sound and Complete Russellian Theory of Definite Descriptions |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2412.03251 |