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.

翻译：超有限主义假定我们只能在相对较小的对象上进行计算，超过特定数值的数不可用。这种方法还会禁止许多形式的无穷推理，并消除源于枚举定理的某些悖论。然而，哲学家们对于这种有限主义逻辑是否一致仍存在分歧。我们展示了一项基于Curry-Howard同构的证明系统的初步工作。同时，我们尝试呈现一些在此类系统中不再成立的著名定理，而相反的陈述变得可证明。这种方法将某些不可能性结果呈现为源于对超限推理的过度使用的逻辑悖论。