eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-08-20
5:1
5:20
10.4230/LIPIcs.TYPES.2023.5
article
Consistent Ultrafinitist Logic
Gajda, Michał J.
1
https://orcid.org/0000-0001-7820-3906
Migamake Pte Ltd, Singapore
Ultrafinitism postulates that we can only compute on relatively short objects, and numbers beyond a certain value are not available. This approach would also forbid many forms of infinitary reasoning and allow removing certain paradoxes stemming from enumeration theorems. For a computational application of ultrafinitist logic, we need more than a proof system, but a logical framework to express both proofs, programs, and theorems in a single framework. We present its inference rules, reduction relation, and self-encoding to allow direct proving of the properties of ultrafinitist logic within itself. We also provide a justification why it can express all bounded Turing programs, and thus serve as a "logic of computability".
https://drops.dagstuhl.de/storage/00lipics/lipics-vol303-types2023/LIPIcs.TYPES.2023.5/LIPIcs.TYPES.2023.5.pdf
ultrafinitism
bounded Turing completeness
logic of computability
decidable logic
explicit complexity
strict finitism