Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version. (English) Zbl 07695716
Summary: We mechanise the undecidability of various first-order axiom systems in Coq, employing the synthetic approach to computability underlying the growing Coq Library of Undecidability Proofs. Concretely, we cover both semantic and deductive entailment in fragments of Peano arithmetic (PA) as well as ZF and related finitary set theories, with their undecidability established by many-one reductions from solvability of Diophantine equations, i.e. Hilbert’s tenth problem (H10), and the Post correspondence problem (PCP), respectively. In the synthetic setting based on the computability of all functions definable in a constructive foundation, such as Coq’s type theory, it suffices to define these reductions as meta-level functions with no need for further encoding in a formalised model of computation. The concrete cases of PA and the considered set theories are supplemented by a general synthetic theory of undecidable axiomatisations, focusing on well-known connections to consistency and incompleteness. Specifically, our reductions rely on the existence of standard models, necessitating additional assumptions in the case of full ZF, and all axiomatic extensions still justified by such standard models are shown incomplete. As a by-product of the undecidability of set theories formulated using only membership and no equality symbol, we obtain the undecidability of first-order logic with a single binary relation.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
Keywords:
undecidability; synthetic computability; first-order logic; incompleteness; Peano arithmetic; ZF set theory; constructive type theory; CoqReferences:
| [1] | Aczel, P.; Macintyre, A.; Pacholski, L.; Paris, J., The type theoretic interpretation of constructive set theory, Studies in Logic and the Foundations of Mathematics, 55-66 (1978), Heidelberg: Springer, Heidelberg · Zbl 0481.03035 |
| [2] | Aczel, P., Non-Well-Founded Sets (1988), Palo Alto: CSLI Lecture Notes, Palo Alto · Zbl 0668.04001 |
| [3] | Barras, B., Sets in Coq, Coq in sets, J. Formaliz. Reason., 3, 1, 29-48 (2010) · Zbl 1211.03023 |
| [4] | Bauer, A., First steps in synthetic computability theory, Electron. Notes Theor. Comput. Sci., 155, 5-31 (2006) · Zbl 1273.03144 · doi:10.1016/j.entcs.2005.11.049 |
| [5] | Braibant, T., Pous, D.: An efficient Coq tactic for deciding Kleene algebras. In: International Conference on Interactive Theorem Proving, 163-178. Springer, Berlin, Heidelberg (2010) · Zbl 1291.68330 |
| [6] | Bundy, A., Giunchiglia, F., Villafiorita, A., Walsh, T.: An incompleteness theorem via abstraction. Technical Report (1996) · Zbl 0890.03004 |
| [7] | Church, A., A note on the Entscheidungsproblem, J. Symb. Log., 1, 1, 40-41 (1936) · Zbl 0014.38503 · doi:10.2307/2269326 |
| [8] | de Bruijn, NG, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Math., 75, 5, 381-392 (1972) · Zbl 0253.68007 · doi:10.1016/1385-7258(72)90034-0 |
| [9] | Doner, J.; Hodges, W., Alfred Tarski and decidable theories, J. Symb. Logic, 53, 1, 20-35 (1988) · Zbl 0647.03001 · doi:10.1017/S0022481200028905 |
| [10] | Forster, Y., Heiter, E., Smolka, G.: Verification of PCP-related computational reductions in Coq. In: International Conference on Interactive Theorem Proving, pp. 253-269 (2018). Springer · Zbl 1511.68310 |
| [11] | Forster, Y., Kirst, D., Smolka, G.: On synthetic undecidability in coq, with an application to the entscheidungsproblem. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (2019) |
| [12] | Forster, Y., Kunze, F.: A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving. Leibniz International Proceedings in Informatics (LIPIcs), Vol.141, pp. 17-11719. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). doi:10.4230/LIPIcs.ITP.2019.17. http://drops.dagstuhl.de/opus/volltexte/2019/11072 · Zbl 07649966 |
| [13] | Forster, Y., Larchey-Wendling, D., Dudenhefner, A., Heiter, E., Kirst, D., Kunze, F., Smolka, G., Spies, S., Wehr, D., Wuttke, M.: A Coq library of undecidable problems. In: CoqPL 2020, New Orleans, LA, United States (2020). https://github.com/uds-psl/coq-library-undecidability |
| [14] | Forster, Y.: Church’s Thesis and related axioms in Coq’s type theory. In: Baier, C., Goubault-Larrecq, J. (Eds.) 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). LIPIcs, Vol. 183, pp. 21-12119. Dagstuhl, Germany (2021) |
| [15] | Forster, Y.; Kirst, D.; Wehr, D., Completeness theorems for first-order logic analysed in constructive type theory: extended version, J. Logic Comput., 31, 1, 112-151 (2021) · Zbl 07471462 · doi:10.1093/logcom/exaa073 |
| [16] | Friedman, H.; Scott, D.; Muller, G., Classically and intuitionistically provably recursive functions, Higher Set Theory, 21-27 (1978), Berlin: Springer, Berlin · Zbl 0396.03045 · doi:10.1007/BFb0103100 |
| [17] | Han, J., van Doorn, F.: A formal proof of the independence of the continuum hypothesis. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 353-366 (2020) |
| [18] | Hilbert, D.; Ackermann, W., Grundzüge der Theoretischen Logik (1928), Berlin: Springer, Berlin · JFM 54.0055.01 |
| [19] | Hostert, J., Koch, M., Kirst, D.: A toolbox for mechanised first-order logic. In: Coq Workshop, vol. 2021 (2021) |
| [20] | Kirby, L., Finitary set theory, Notre Dame J. Form. Log., 50, 3, 227-244 (2009) · Zbl 1190.03043 · doi:10.1215/00294527-2009-009 |
| [21] | Kirst, D., Hermes, M.: Synthetic undecidability and incompleteness of first-order axiom systems in coq. In: 12th International Conference on Interactive Theorem Proving (ITP 2021) (2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik |
| [22] | Kirst, D., Larchey-Wendling, D.: Trakhtenbrot’s theorem in Coq: a constructive approach to finite model theory. In: International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France. Springer, Paris, France (2020) · Zbl 07614663 |
| [23] | Kirst, D., Smolka, G.: Large model constructions for second-order ZF in dependent type theory. Certified Programs and Proofs—7th International Conference, CPP 2018, Los Angeles, USA, 2018 (2018) |
| [24] | Kreisel, G.: Church’s thesis: a kind of reducibility axiom for constructive mathematics. In: Studies in Logic and the Foundations of Mathematics, Vol. 60, pp. 121-150 (1970) · Zbl 0199.30001 |
| [25] | Larchey-Wendling, D., Forster, Y.: Hilbert’s tenth problem in Coq. In: 4th International Conference on Formal Structures for Computation and Deduction. LIPIcs, 131, pp. 27-12720 (2019) · Zbl 1528.03181 |
| [26] | Laurent, O.: An anti-locally-nameless approach to formalizing quantifiers. In: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 300-312 (2021) |
| [27] | Maksimović, P., Schmitt, A.: HOCore in Coq. In: International Conference on Interactive Theorem Proving, pp. 278-293. Springer, Berlin (2015) · Zbl 1465.68196 |
| [28] | Myhill, J.: Some properties of intuitionistic Zermelo-Frankel set theory. In: Cambridge Summer School in Mathematical Logic, pp. 206-231. Springer, Berlin (1973) · Zbl 0272.02039 |
| [29] | O’Connor, R.; Hurd, J.; Melham, T., Essential incompleteness of arithmetic verified by Coq, Theorem Proving in Higher Order Logics, 245-260 (2005), Berlin: Springer, Berlin · Zbl 1152.03315 · doi:10.1007/11541868_16 |
| [30] | Paulson, LC, A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle, J. Autom. Reason., 55, 1, 1-37 (2015) · Zbl 1357.68200 · doi:10.1007/s10817-015-9322-8 |
| [31] | Popescu, A., Traytel, D.: A formally verified abstract account of Gödel’s incompleteness theorems. In: International Conference on Automated Deduction, pp. 442-461 (2019). Springer · Zbl 1535.03284 |
| [32] | Post, E. L., Recursively enumerable sets of positive integers and their decision problems, Bull. Am. Math. Soc., 50, 5, 284-316 (1944) · Zbl 0063.06328 · doi:10.1090/S0002-9904-1944-08111-1 |
| [33] | Presburger, M.z; Jabcquette, D., On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation, Hist. Philos. Logic, 12, 2, 225-233 (1991) · Zbl 0741.03027 · doi:10.1080/014453409108837187 |
| [34] | Quaife, A., Automated proofs of Löb’s theorem and Gödel’s two incompleteness theorems, J. Autom. Reason., 4, 2, 219-231 (1988) · Zbl 0657.03007 · doi:10.1007/BF00244396 |
| [35] | Richman, F., Church’s thesis without tears, J. Symbol. Logic, 48, 3, 797-803 (1983) · Zbl 0527.03036 · doi:10.2307/2273473 |
| [36] | Schäfer, S., Smolka, G., Tebbi, T.: Completeness and decidability of de Bruijn substitution algebra in Coq. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, pp. 67-73. ACM, New York, NY, USA (2015) |
| [37] | Shankar, N.: Proof-checking Metamathematics, The University of Texas at Austin (1986). PhD Thesis |
| [38] | Sieg, W., Field, C.: Automated search for Gödel’s proofs. In: Deduction, Computation, Experiment, pp. 117-140. Springer, Berlin (2008) · Zbl 1191.03010 |
| [39] | Smolka, G., Stark, K.: Hereditarily finite sets in constructive type theory. In: Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-27, 2016. LNCS, vol. 9807, pp. 374-390. Springer, Cham (2016) · Zbl 1478.03073 |
| [40] | Smullyan, RM; Fitting, M., Set Theory and the Continuum Problem (2010), Mineola: Dover Publications, Mineola |
| [41] | Sozeau, M.; Anand, A.; Boulier, S.; Cohen, C.; Forster, Y.; Kunze, F.; Malecha, G.; Tabareau, N.; Winterhalter, T., The MetaCoq Project, J. Autom. Reason., 64, 5, 947-999 (2020) · Zbl 1468.68075 · doi:10.1007/s10817-019-09540-0 |
| [42] | Stark, K., Schäfer, S., Kaiser, J.: Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In: International Conference on Certified Programs and Proofs, pp. 166-180 (2019). ACM |
| [43] | Tarski, A.: I: A general method in proofs of undecidability. In: Tarski, A. (ed.) Undecidable Theories. Studies in Logic and the Foundations of Mathematics, 13, pp. 1-34 (1953) |
| [44] | Team, T.C.D.: The Coq Proof Assistant, version 8.12.0. Zenodo (2020). doi:10.5281/zenodo.4021912 |
| [45] | Tennenbaum, S., Non-Archimedean models for arithmetic, Not. Am. Math. Soc., 6, 270, 44 (1959) |
| [46] | Trakhtenbrot, BA, The impossibility of an algorithm for the decidability problem on finite classes, Dokl. Akad. Nok. SSSR, 70, 4, 569-572 (1950) · Zbl 0038.15001 |
| [47] | Turing, AM, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, 2, 1, 230-265 (1937) · JFM 62.1059.03 · doi:10.1112/plms/s2-42.1.230 |
| [48] | Werner, B.; Ito, T.; Abadi, M., Sets in types, types in sets, Theoretical Aspects of Computer Software, 530-546 (1997), Berlin: Springer, Berlin · Zbl 0885.03017 · doi:10.1007/BFb0014566 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
