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形态的验证系统。 我们还试图提出一些在这种系统中不再真实存在的众所周知的理论,而相反的论理则则变得容易被证实。 这种方法提出了某些不可能的结果,作为通过使用流线推理产生的逻辑悖论。