Consistent ultrafinitist logic
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929466781990912 |
|---|---|
| author | Gajda, Michał J. |
| author_facet | Gajda, Michał J. |
| contents | Ultrafinitism postulates that we can only compute on relatively short objects, and numbers beyond certain value are not available. This approach would also forbid many forms of infinitary reasoning and allow to remove certain paradoxes stemming from enumeration theorems. However, philosophers still disagree of whether such a finitist logic would be consistent. We present preliminary work on a proof system based on Curry-Howard isomorphism. We also try to present some well-known theorems that stop being true in such systems, whereas opposite statements become provable. This approach presents certain impossibility results as logical paradoxes stemming from a profligate use of transfinite reasoning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2106_13309 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Consistent ultrafinitist logic Gajda, Michał J. Programming Languages Logic in Computer Science 03A05, 03D10, 03D25, 03F40, 03F50, 03F55 F.4.1; F.1.1 Ultrafinitism postulates that we can only compute on relatively short objects, and numbers beyond certain value are not available. This approach would also forbid many forms of infinitary reasoning and allow to remove certain paradoxes stemming from enumeration theorems. However, philosophers still disagree of whether such a finitist logic would be consistent. We present preliminary work on a proof system based on Curry-Howard isomorphism. We also try to present some well-known theorems that stop being true in such systems, whereas opposite statements become provable. This approach presents certain impossibility results as logical paradoxes stemming from a profligate use of transfinite reasoning. |
| title | Consistent ultrafinitist logic |
| topic | Programming Languages Logic in Computer Science 03A05, 03D10, 03D25, 03F40, 03F50, 03F55 F.4.1; F.1.1 |
| url | https://arxiv.org/abs/2106.13309 |