Document Open Access Logo

Consistent Ultrafinitist Logic

Author Michał J. Gajda

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2023.5.pdf
  • Filesize: 0.82 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • ultrafinitism
  • bounded Turing completeness
  • logic of computability
  • decidable logic
  • explicit complexity
  • strict finitism

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Ultrafinitism postulates that we can only compute on relatively short objects, and numbers beyond a certain value are not available. This approach would also forbid many forms of infinitary reasoning and allow removing certain paradoxes stemming from enumeration theorems. For a computational application of ultrafinitist logic, we need more than a proof system, but a logical framework to express both proofs, programs, and theorems in a single framework. We present its inference rules, reduction relation, and self-encoding to allow direct proving of the properties of ultrafinitist logic within itself. We also provide a justification why it can express all bounded Turing programs, and thus serve as a "logic of computability".

Cite As Get BibTex

Michał J. Gajda. Consistent Ultrafinitist Logic. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.TYPES.2023.5

Author Details

Michał J. Gajda
  • Migamake Pte Ltd, Singapore

Acknowledgements

We thank Vendran Čačić, Seth Chaiken, Bhupinder Singh Anand, Orestis Melkonian, Anton Setzer for their invaluable feedback. Thanks to Daniel Schwartz for sparkling my interest in Kleene normal form.

References

  1. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. Proc. ACM Program. Lang., 2(ICFP), July 2018. URL: https://doi.org/10.1145/3236789.
  2. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. A log-sensitive encoding of turing machines in the λ-calculus, 2023. URL: https://arxiv.org/abs/2301.12556.
  3. Wilhelm Ackermann. Zum hilbertschen aufbau der reellen zahlen. Mathematische Annalen, 99(1):118-133, December 1928. URL: https://doi.org/10.1007/BF01459088.
  4. Yehoshua Bar-Hillel and Rudolf Carnap. Semantic information. British Journal for the Philosophy of Science, 4(14):147-157, 1953. URL: https://doi.org/10.1093/bjps/IV.14.147.
  5. Pablo Barenbaum and Eduardo Bonelli. Optimality and the Linear Substitution Calculus. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), volume 84 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.9.
  6. Jose Benardete. Infinity: An Essay in Metaphysics. Clarendon Press, 1964. Google Scholar
  7. Albert A. Bennett. Note on an operation of the third grade. Annals of Mathematics. Second Series, 17 (2):74-75, December 1915. URL: https://doi.org/10.2307/2007124.
  8. Yves Bertot and Vladimir Komendantsky. Fixed point semantics and partial recursion in Coq. In MPC 2008, Marseille, France, July 2008. URL: https://hal.inria.fr/inria-00190975.
  9. Tobias Boolakee, Christian Heide, Antonio Garzon-Ramirez, Heiko B. Weber, Ignacio Franco, and Peter Hommelhoff. Light-field control of real and virtual charge carriers. Nature, 605(7909):251-255, May 2022. URL: https://doi.org/10.1038/s41586-022-04565-9.
  10. Manuel Bremer. Varieties of finitism. Metaphysica, 8:131-148, October 2007. URL: https://doi.org/10.1007/s12133-007-0012-9.
  11. l. e. j. Brouwer. Over de grondslagen der wiskunde, volume 1 of mc varia. Mathematisch Centrum, Amsterdam, 1981. including unpublished fragments, correspondence with D. J. Korteweg and reviews by G. Mannoury, edited and with an introduction by D. Van Dalen. Google Scholar
  12. Samuel R. Buss. The polynomial hierarchy and intuitionistic bounded arithmetic. In Alan L. Selman, editor, Structure in Complexity Theory, Proceedings of the Conference hold at the University of California, Berkeley, California, USA, June 2-5, 1986, volume 223 of Lecture Notes in Computer Science, pages 77-103. Springer, 1986. URL: https://doi.org/10.1007/3-540-16486-3_91.
  13. Thierry Coquand. An analysis of girard’s paradox. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pages 227-236. IEEE Computer Society Press, June 1986. Google Scholar
  14. Ugo Dal Lago. Implicit computation complexity in higher-order programming languages: A survey in memory of martin hofmann. Math. Struct. Comput. Sci., 32(6):760-776, 2022. URL: https://doi.org/10.1017/S0960129521000505.
  15. Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, volume 75, pages 381-392. Elsevier, 1972. Google Scholar
  16. P. J. Denning, J. B. Dennis, and J. E. Qualitz. Machines, Languages, and Computation. Prentice-Hall, 1978. Google Scholar
  17. Michael Dummett. Wang’s paradox. Synthese, 30(3/4):301-324, 1975. URL: https://link.springer.com/article/10.1007/BF00485048.
  18. Liu Dun. A comparison of archimedes' and liu hui’s studies of circles. In Chinese Studies in the History and Philosophy of Science and Technology 179, pages 279-287. Kluwer Academic Publishers, 1966. Google Scholar
  19. Marie Duzi. The paradox of inference and the non-triviality of analytic information. Journal of Philosophical Logic, 39:473-510, October 2010. URL: https://doi.org/10.1007/s10992-010-9127-5.
  20. Lisa Dyson, Matthew Kleban, and Leonard Susskind. Disturbing implications of a cosmological constant. Journal of High Energy Physics, 2002(10):011, November 2002. URL: https://doi.org/10.1088/1126-6708/2002/10/011.
  21. Solomon Feferman. Systems of predicative analysis. Journal of Symbolic Logic, 29:1-30, 1964. URL: https://api.semanticscholar.org/CorpusID:35126801.
  22. Amanda Gefter. Mind-bending mathematics: Why infinity has to go. New Scientist, 219(2930):32-35, 2013. URL: https://doi.org/10.1016/S0262-4079(13)62043-6.
  23. Jean-Yves Girard. Interprétation fonctionnelle et Élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris Diderot - Paris 7, 1972. URL: https://www.cs.cmu.edu/~kw/scans/girard72thesis.pdf.
  24. Nicolas Gisin. Indeterminism in physics, classical chaos and bohmian mechanics. are real numbers really real?, 2019. URL: https://arxiv.org/abs/1803.06824.
  25. Kurt Gödel. Über formal unentscheidbare sätze der principia mathematica und verwandter systeme i. Monatshefte für Mathematik und Physik, 38(1):173-198, December 1931. URL: https://doi.org/10.1007/BF01700692.
  26. Kurt Gödel, S. Feferman, J.W. Dawson, S.C. Kleene, G. Moore, R. Solovay, and J. van Heijenoort. Kurt Gödel: Collected Works: Volume I: Publications 1929-1936. Collected Works of Kurt Godel. OUP USA, 1986. URL: https://books.google.pl/books?id=5ya4A0w62skC.
  27. R. L. Goodstein. On the restricted ordinal theorem. The Journal of Symbolic Logic, 9(2):33-41, 1944. URL: https://doi.org/10.2307/2268019.
  28. Gennady Gorelik. Bremermann’s limit and cgh-physics, 2010. URL: https://arxiv.org/abs/0910.3424.
  29. Judith V. Grabiner. Who gave you the epsilon? cauchy and the origins of rigorous calculus. The American Mathematical Monthly, 90(3):185-194, 1983. URL: http://www.jstor.org/stable/2975545.
  30. Joel David Hamkins. Every function can be computable! Blog post., March 2016. URL: http://jdh.hamkins.org/every-function-can-be-computable/.
  31. Hans Hermes. Enumerability, decidability, computability - an introduction to the theory of recursive functions. Springer, 1969. Google Scholar
  32. David Hilbert. Mathematical problems. Bulletin of the American Mathematical Society, 8(10):437-479, 1902. Google Scholar
  33. David Hilbert. Über das unendliche. Mathematische Annalen, 95:161-190, 1926. URL: https://doi.org/10.1007/BF01206605.
  34. John E. Hopcroft and Jeffrey D. Ullman. Relations between time and tape complexities. J. ACM, 15(3):414-427, July 1968. URL: https://doi.org/10.1145/321466.321474.
  35. William A. Howard. The formulae-as-types notion of construction. In J. Hindley and J. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, λ-calculus and Formalism, pages 479-490. Academic Press, 1980. Google Scholar
  36. Jan Martin Jansen. Programming in the λ-Calculus: From Church to Scott and Back, pages 168-180. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-40355-2_12.
  37. Emil Jeřábek. A simplified lower bound for implicational logic, 2023. URL: https://arxiv.org/abs/2303.15090.
  38. Laurie Kirby and Jeff Paris. Accessible independence results for peano arithmetic. Bulletin of the London Mathematical Society, 14(4):285-293, 1982. URL: https://doi.org/10.1112/blms/14.4.285.
  39. Don Knuth, Frank Ellerman, and Natan Arie Consigli. A001764 - a(n) = binomial(3*n,n)/(2*n+1) (enumerates ternary trees and also noncrossing trees). (formerly m2926 n1174), 2016. URL: https://oeis.org/A001764.
  40. Don Knuth, Frank Ellerman, and Natan Arie Consigli. A046859: Simplified ackermann function (main diagonal of ackermann-péter function), 2016. URL: https://oeis.org/A046859.
  41. Cynthia Kop and Deivid Vale. Tuple Interpretations for Higher-Order Complexity. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), volume 195 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:22, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.31.
  42. Andras Kornai. Explicit finitism. International Journal of Theoretical Physics, 42:301-307, February 2003. URL: https://doi.org/10.1023/A:1024451401255.
  43. Jan Krajicek. Bounded Arithmetic, Propositional Logic and Complexity Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1995. URL: https://doi.org/10.1017/CBO9780511529948.
  44. Lawrence M. Krauss and Glenn D. Starkman. Universal limits on computation. Preprint arXiV., 2004. URL: https://arxiv.org/abs/astro-ph/0404510.
  45. John Lamping. An algorithm for optimal lambda calculus reduction. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pages 16-30, New York, NY, USA, 1989. Association for Computing Machinery. URL: https://doi.org/10.1145/96709.96711.
  46. Jean-Luc Lehners and Jerome Quintin. A small universe, 2023. URL: https://arxiv.org/abs/2309.03272.
  47. Jonathan Lenchner. A finitist’s manifesto: Do we need to reformulate the foundations of mathematics?, 2020. URL: https://arxiv.org/abs/2009.06485.
  48. Seth Lloyd. Ultimate physical limits to computation. Nature, 406(6799):1047-1054, August 2000. URL: https://doi.org/10.1038/35023282.
  49. Seth Lloyd. Computational capacity of the universe. Physical review letters, 88 23:237901, 2002. Google Scholar
  50. José Pedro Magalhães, Atze Dijkstra, Johan Jeuring, and Andres Löh. A generic deriving mechanism for haskell. SIGPLAN Not., 45(11):37-48, September 2010. URL: https://doi.org/10.1145/2088456.1863529.
  51. Ofra Magidor. Strict finitism refuted? Proceedings of the Aristotelian Society, 107(1pt3):403-411, 2007. URL: https://doi.org/10.1111/j.1467-9264.2007.00230.x.
  52. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in proof theory. Bibliopolis, 1984. Google Scholar
  53. Albert R. Meyer and Dennis M. Ritchie. The complexity of loop programs. In Proceedings of the 1967 22nd National Conference, ACM '67, pages 465-469, New York, NY, USA, 1967. Association for Computing Machinery. URL: https://doi.org/10.1145/800196.806014.
  54. Aran Nayebi. Practical intractability: A critique of the hypercomputation movement. Minds and Machines, 24:275-305, 2012. URL: https://api.semanticscholar.org/CorpusID:9328713.
  55. Daniel Nolan. Lessons from infinite clowns (1st edition). In Karen Bennett and Dean Zimmerman, editors, Oxford Studies in Metaphysics Vol. 14. Oxford University Press, forthcoming. Google Scholar
  56. B. Nordström. Terminating general recursion. BIT, 28(3):605-619, July 1988. URL: https://doi.org/10.1007/BF01941137.
  57. Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer. Live functional programming with typed holes. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290327.
  58. Christine Paulin-Mohring. Inductive definitions in the system coq - rules and properties. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 328-345. Springer, 1993. URL: https://doi.org/10.1007/BFb0037116.
  59. Rózsa Péter. Über die verallgemeinerung der theorie der rekursiven funktionen für abstrakte mengen geeigneter struktur als definitionsbereiche. Acta Mathematica Academiae Scientiarum Hungaricae, 12(3):271-314, May 1964. URL: https://doi.org/10.1007/BF02023919.
  60. Gordon D. Plotkin. A structural approach to operational semantics, 2004. Google Scholar
  61. Karlis Podnieks. Towards a real finitism? Web page published online., December 2005. URL: http://www.ltn.lv/~podnieks/finitism.htm.
  62. António G. Porto and Armando B. Matos. Ackermann and the superpowers. SIGACT News, 12(3):90-95, September 1980. URL: https://doi.org/10.1145/1008861.1008872.
  63. Pavel Pudlák. Incompleteness in the finite domain. Bulletin of Symbolic Logic, 23(4):405-441, 2017. URL: https://doi.org/10.1017/bsl.2017.32.
  64. Raphael M. Robinson. Primitive recursive functions. Bulletin of the American Mathematical Society, 53(10):p. 925-942, 1947. URL: https://doi.org/bams/1183511140.
  65. David Sands. Calculi for time analysis of functional programs. PhD thesis, University of London, 1990. Google Scholar
  66. Vladimir Yu. Sazonov. On feasible numbers. In Daniel Leivant, editor, Logic and Computational Complexity, pages 30-51, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  67. Matthias Schirn and Karl-Georg Niebergall. Finitism = pra? on a thesis of w. w. tait. Reports on Mathematical Logic, January 2005. Google Scholar
  68. Kurt Schütte. Predicative well-orderings. Studies in logic and the foundations of mathematics, 40:280-303, 1965. URL: https://api.semanticscholar.org/CorpusID:117343586.
  69. Galina Iwanowna Sinkiewicz. On history of epsilontics. Antiquitates Mathematicae, 10(0):183-204, 2017. URL: https://doi.org/10.14708/am.v10i0.805.
  70. G. Sudan. Sur le nombre transfini ω ^ω. Bulletin Mathématique de la Société Roumaine des Sciences, 30:11-30, 1927. Google Scholar
  71. Yngve Sundblad. The ackermann function. a theoretical, computational, and formula manipulative study. BIT Numerical Mathematics, 11(1):107-119, March 1971. URL: https://doi.org/10.1007/BF01935330.
  72. Morten Heine b. Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Studies in Logic and Foundations of Mathematics. Elsevier, 1998. URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385.
  73. Alfred Tarski, Andrzej Mostowski, and Raphael M. Robinson. Undecidable theories. Philosophy, 30(114):278-279, 1955. Google Scholar
  74. A. S. Troelstra. Constructivism in Mathematics: An Introduction. Elsevier, 1988. URL: https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/121/suppl/C.
  75. Dirk Van Dalen. Intuitionistic Logic, pages 225-339. Springer Netherlands, Dordrecht, 1986. URL: https://doi.org/10.1007/978-94-009-5203-4_4.
  76. Herman Van Looy. A chronology and historical analysis of the mathematical manuscripts of gregorius a sancto vincentio (1584–1667). Historia Mathematica, 11(1):57-75, 1984. URL: https://doi.org/10.1016/0315-0860(84)90005-3.
  77. Nik Weaver. What is predicativism? Unpublished manuscript online., 2013. URL: https://api.semanticscholar.org/CorpusID:40352024.
  78. Karl Weierstraß. Rechnen mit komplexen Zahlen, pages 25-44. Vieweg+Teubner Verlag, Wiesbaden, 1861-1862. URL: https://doi.org/10.1007/978-3-663-06846-4_3.
  79. Aleksandr S Yessenin-Volpin. The ultra-intuitionistic criticism and the antitraditional program for foundations of mathematics. In Studies in Logic and the Foundations of Mathematics, volume 60, pages 3-45. Elsevier, 1970. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact