2026-08-01T15:00:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20483 2024-08-20T13:53:45Z ddc:004 open_access

Consistent Ultrafinitist Logic Gajda, Michał J. ultrafinitism bounded Turing completeness logic of computability decidable logic explicit complexity strict finitism 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". Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michał J. Gajda 2024 Is Part Of LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2023.5 urn:nbn:de:0030-drops-204833 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.5 eng https://creativecommons.org/licenses/by/4.0/legalcode