Consistent ultrafinitist logic

TL;DR

The paper tackles the problem of consistency for ultrafinitist logic by proposing a bounded, Curry-Howard-inspired proof system (UFL) where all proof terms and normalization steps are bounded by input sizes, using monotone polyvariate bounds. It demonstrates that many classical infinitary theorems fail under such bounds while some opposite statements become provable, and frames paradoxes as artifacts of transfinite reasoning. Consistency is established by reduction to intuitionistic logic, and the work envisions a computable foundations program for mathematics built on explicit finite bounds. Together, these contributions provide a finitary, executable interpretation of constructive mathematics and clarify how ultrafinitist reasoning can ground mathematics in bounded computation.

Abstract

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.