Consistent Ultrafinitist Logic

[Bhupinder Singh Anand]

Dear Michal,

1. Apropos your paper, 'Consistent Ultrafinitist Logic', posted by Vladik Kreinovich on 13 Feb 2022 on construc...@googlegroups.com, I quote your abstract:

"Ultrafinitism (Kornai 2003; Podnieks 2005; Yessenin-Volpin 1970; Gefter 2013; Lenchner 2020) postulates that we can only reason and compute relatively short objects(Seth Lloyd 2000; Krauss and Starkman 2004; Sazonov 1995; S. Lloyd 2002; Gorelik 2010), and numbers beyond certain value are not available. Some philosophers also question the physical existence of real numbers beyond a certain level of [accuracy] (Gisin 2019). This approach would also forbid many forms of infinitary reasoning and allow removing many from paradoxes stemming from a countable enumeration.

However, philosophers still disagree on whether such a finitist logic could be consistent (Magidor 2007), while constructivist mathematicians claim that ``\textit{no satisfactory developments exist}" (Troelstra 1988). We present preliminary work on a proof system based on Curry-Howard isomorphism (Howard 1980) and explicit bounds for computational complexity."

2. Permit me to share the evidence-based perspective of my paper [An16], which proves both the weak consistency of ultrafinitist logic, and the strong consistency of finitist logic, as immediate entailments, respectively, of:

(i) Theorem 5.6: The axioms of PA are always algorithmically verifiable as true under the interpretation I_(PA, N, SV), and the rules of inference of PA preserve the properties of algorithmically verifiable satisfaction/truth under I_(PA, N, SV);

(ii) Theorem 6.7: The axioms of PA are always algorithmically computable as true under the interpretation I_(PA, N, SC), and the rules of inference of PA preserve the properties of algorithmically computable satisfaction/truth under I_(PA, N, SC).

3. Here, PA is the first-order Peano Arithmetic PA, and:

(a) the algorithmically verifiable formulas of PA are the formulas that are ultrafinitarily true; in the sense that, for any specified numeral [n], the formula [F(n)] is PA-provable (i.e., [(Ax)F(x)] is numeral-wise provable in PA).

Hence, under any well-defined Tarskian interpretation of PA,, there is some deterministic algorithm (defined upon [n]) that will evidence the PA-formula [F(n)] as true;

(b) the algorithmically computable formulas of PA are the formulas that are finitarily true; in the sense  that [F(n)] is PA-provable. (i.e., [(Ax)F(x)] is provable in PA). 

Hence, under any well-defined Tarskian interpretation of PA, there is some deterministic algorithm (independent of [n]) that will evidence the PA-formula [F(n)] as true.

4. That the above distinction is not vacuous follows from Kurt Goedel's seminal 1931 paper on  formally 'undecidable' arithmetical propositions, where he constructed an arithmetical formula, [(Ax)R(x)], that is unprovable, but numeral-wise provable, in a Peano Arithmetic---hence algorithmically verifiable as true, but not algorithmically computable as true, under any well-defined Tarskian interpretation of PA.

Kind regards,

Bhup

[An16] The truth assignments that differentiate human reasoning from mechanistic reasoning: The evidence-based argument for Lucas' Gödelian thesis. In Cognitive Systems Research. Volume 40, December 2016, 35-45.

https://doi.org/10.1016/j.cogsys.2016.02.004
https://www.dropbox.com/s/lrt2xq0wlzo3wxx/