arXiv:2106.13309cs.PL
Consistent ultrafinitist logic
Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.
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.
The assumption of this theorem is that we may encode any problem that is unbounded and infinite. What if we limit ourselves to *bounded* and *computable* functions only? See draft presented at many top logic conferences yet: https://arxiv.org/abs/2106.13309 Since the observable…
migaView on HNParent context
Trying to find a formal system that encodes unbounded infinitary mathematical objects including most of maths, but yet to require that all statements are decidable within a finite number of steps... Is it contradiction in the proof, or rather a contradiction in assumptions? More…
migaView on HNParent context