nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory

verfasst von : Yannick Forster, Dominik Kirst, Dominik Wehr

Erschienen in: Logical Foundations of Computer Science

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game semantics. As completeness with respect to standard model-theoretic semantics is not readily constructive, we analyse the assumptions necessary for particular syntax fragments and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Countermodel Construction via Optimal Hypersequent Calculi for Non-normal Modal Logics

Nächstes Kapitel On the Constructive Truth and Falsity in Peano Arithmetic

Nur mit Berechtigung zugänglich

Accepted in Russian constructivism while in conflict with Brouwer’s intuitionism.

On www.ps.uni-saarland.de/extras/fol-completeness and hyperlinked with this pdf.

Bauer, A.: First steps in synthetic computability theory. Electron. Notes Theor. Comput. Sci. 155, 5–31 (2006). Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI)CrossRef

Berardi, S.: Intuitionistic completeness for first order classical logic. J. Symbolic Logic 64(1), 304–312 (1999)MathSciNetCrossRef

Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed lambda-calculus. In: 1991 Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 203–211. IEEE (1991)

Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 46–60. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_4CrossRef

Braselmann, P., Koepke, P.: Gödel’s completeness theorem. Formalized Math. 13(1), 49–53 (2005)

Constable, R., Bickford, M.: Intuitionistic completeness of first-order logic. Ann. Pure Appl. Logic 165(1), 164–198 (2014)MathSciNetCrossRef

Coquand, T., Mannaa, B.: The independence of Markov’s principle in type theory. Logical Methods Comput. Sci. 13(3), 18605974 (2017). arXiv: 1602.04530

de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75(5), 381–392 (1972)MathSciNetCrossRef

Delaware, B., d S Oliveira, B.C., Schrijvers, T.: Meta-theory à la carte. In: ACM SIGPLAN Notices, vol. 48, pp. 207–218. ACM (2013)

10.

Dybjer, P., Filinski, A.: Normalization and partial evaluation. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 137–192. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45699-6_4CrossRef

11.

Felscher, W.: Dialogues, strategies, and intuitionistic provability. Ann. Pure Appl. Logic 28(3), 217–254 (1985)MathSciNetCrossRef

12.

Forster, Y., Larchey-Wendling, D., Dudenhefner, A., Heiter, E., Kirst, D., Kunze, F., Gert, S., Spies, S., Wehr, D., Wuttke, M.: A Coq Library of Undecidable Problems (2019). https://github.com/uds-psl/coq-library-undecidability

13.

Forster, Y., Heiter, E., Smolka, G.: Verification of PCP-related computational reductions in Coq. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 253–269. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94821-8_15CrossRef

14.

Forster, Y., Kirst, D., Smolka, G.: On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In: International Conference on Certified Programs and Proofs, pp. 38–51. ACM (2019)

15.

Forster, Y., Kunze, F.: Verified extraction from Coq to a Lambda-Calculus. In: Coq Workshop, vol. 2016 (2016)

16.

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, volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, pp. 17:1–17:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)

17.

Forster, Y., Smolka, G.: Weak call-by-value lambda calculus as a model of computation in Coq. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 189–206. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_13CrossRef

18.

Gödel, K.: Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik 37, 349–360 (1930)MathSciNetCrossRef

19.

Han, J., van Doorn, F.: A formalization of forcing and the consistency of the failure of the continuum hypothesis. In: International Conference on Interactive Theorem Proving. Springer, Heidelberg (2019). https://doi.org/10.4230/LIPIcs.ITP.2019.19

20.

Hasenjaeger, G.: Eine Bemerkung zu Henkin’s Beweis für die Vollständigkeit des Prädikatenkalküls der Ersten Stufe. J. Symbolic Logic 18(1), 42–48 (1953)MathSciNetCrossRef

21.

Henkin, L.: The completeness of the first-order functional calculus. J. Symbolic Logic 14(3), 159–166 (1949)MathSciNetCrossRef

22.

Herbelin, H., Ilik, D.: An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem. Draft (2016)

23.

Herbelin, H., Lee, G.: Forcing-based cut-elimination for gentzen-style intuitionistic sequent calculus. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds.) WoLLIC 2009. LNCS (LNAI), vol. 5514, pp. 209–217. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02261-6_17CrossRef

24.

Ilik, D.: Constructive completeness proofs and delimited control. Ph.D. thesis, Ecole Polytechnique X (2010)

25.

Ishihara, H.: Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientae 6, 43–59 (2006)CrossRef

26.

Keuchel, S., Schrijvers, T.: Generic datatypes à la carte. In: ACM SIGPLAN Workshop on Generic Programming, pp. 13–24. ACM (2013)

27.

Kirst, D., Smolka, G.: Categoricity results and large model constructions for second-order ZF in dependent type theory. J. Autom. Reasoning 63, 415–438 (2018)MathSciNetCrossRef

28.

Kreisel, G.: On weak completeness of intuitionistic predicate logic. J. Symbolic Logic 27(2), 139–158 (1962)MathSciNetCrossRef

29.

Kreisel, G., Troelstra, A.S.: Formal systems for some branches of intuitionistic analysis. Ann. Math. Logic 1(3), 229–387 (1970)MathSciNetCrossRef

30.

Krivine, J.-L.: Une preuve formelle et intuitionniste du théorème de complétude de la logique classique. Bull. Symbolic Logic 2(4), 405–421 (1996)MathSciNetCrossRef

31.

Krivtsov, V.N.: An intuitionistic completeness theorem for classical predicate logic. Studia Logica 96(1), 109–115 (2010)MathSciNetCrossRef

32.

Krivtsov, V.N.: Semantical completeness of first-order predicate logic and the weak fan theorem. Studia Logica 103(3), 623–638 (2015)MathSciNetCrossRef

33.

Leivant, D.: Failure of completeness properties of intuitionistic predicate logic for constructive models. Annales scientifiques de l’Université de Clermont. Mathématiques 60(13), 93–107 (1976)

34.

Lorenzen, P.: Logik und Agon. Atti del XII Congresso Internazionale di Filosofia 4, 187–194 (1960)

35.

Lorenzen, P.: Ein dialogisches Konstruktivitätskriterium. In: Proceedings of the Symposium on Foundations of Mathematics (Warsaw, 2–9 September 1959), pp. 193–200 (1961)

36.

MacNeille, H.M.: Partially ordered sets. Trans. Am. Math. Soc. 42(3), 416–460 (1937)MathSciNetCrossRef

37.

Mannaa, B., Coquand, T.: The independence of Markov’s principle in type theory. Logical Methods Comput. Sci. 13(3:10), 1–28 (2017)

38.

McCarty, C.: Constructive validity is nonarithmetic. J. Symbolic Logic 53, 1036–1041 (1988)MathSciNetCrossRef

39.

McCarty, C.: Completeness and incompleteness for intuitionistic logic. J. Symbolic Logic 73(4), 1315–1327 (2008)MathSciNetCrossRef

40.

McCarty, D.C., et al.: Incompleteness in intuitionistic metamathematics. Notre Dame J. Formal Logic 32(3), 323–358 (1991)MathSciNetCrossRef

41.

Pédrot, P.-M., Tabareau, N.: Failure is not an option. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 245–271. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_9CrossRef

42.

Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)MathSciNetCrossRef

43.

Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 294–309. Springer, Heidelberg (2005). https://doi.org/10.1007/11541868_19CrossRefMATH

44.

Schlichtkrull, A.: Formalization of the resolution calculus for first-order logic. J. Autom. Reason. 61(1–4), 455–484 (2018)MathSciNetCrossRef

45.

Schumm, G.F.: A Henkin-style completeness proof for the pure implicational calculus. Notre Dame J. Formal Logic 16(3), 402–404 (1975)MathSciNetCrossRef

46.

Scott, D.: The algebraic interpretation of quantifiers: intuitionistic and classical. In: Ehrenfeucht, V.M.A., Srebrny, M. (eds.) Andrzej Mostowski and Foundational Studies. IOS Press (2008)

47.

Sørensen, M.H., Urzyczyn, P.: Sequent calculus, dialogues, and cut elimination. Reflections Type Theor. \(\lambda \)-Calculus Mind 253–261 (2007). http://www.cs.ru.nl/barendregt60/essays/

48.

Sozeau, M., Mangin, C.: Equations reloaded: high-level dependently-typed functional programming and proving in Coq. Proc. ACM Program. Lang. 3(ICFP), 86 (2019)CrossRef

49.

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. ACM (2019)

50.

The Coq Proof Assistant (2019). http://coq.inria.fr

51.

Timany, A., Sozeau, M.: Cumulative inductive types in Coq. In: Kirchner, H. (ed.) International Conference on Formal Structures for Computation and Deduction, volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany,, pp. 29:1–29:16. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)

52.

Underwood, J.: Aspects of the computational content of proofs. Technical report, Cornell University (1994)

53.

Veldman, W.: An intuitiomstic completeness theorem for intuitionistic predicate logic 1. J. Symbolic Logic 41(1), 159–166 (1976)MathSciNetMATH

54.

Wehr, D.: A constructive analysis of first-order completeness theorems in Coq. Bachelor’s thesis, Saarland University (2019)

55.

Wuttke, M.: Verified programming of turing machines in Coq. Bachelor’s thesis, Saarland University (2018)

Titel: Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory
verfasst von: Yannick Forster
Dominik Kirst
Dominik Wehr
Verlag: Springer International Publishing
Buch: Logical Foundations of Computer Science
Print ISBN: 978-3-030-36754-1

Electronic ISBN: 978-3-030-36755-8

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-36755-8_4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"