A formally verified abstract account of Gödel's incompleteness theorems

Conference paper

Popescu, A. and Traytel, D. 2019. A formally verified abstract account of Gödel's incompleteness theorems. Fontaine, P. (ed.) CADE 27 - 27th International Conference on Automated Deduction. Natel, Brazil 27 - 30 Aug 2019 Springer. pp. 442-461 https://doi.org/10.1007/978-3-030-29436-6_26
TypeConference paper
TitleA formally verified abstract account of Gödel's incompleteness theorems
AuthorsPopescu, A. and Traytel, D.
Abstract

We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL theorem prover. We analyze sufficient conditions for the theorems’ applicability to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser’s variation of the first theorem, Jeroslow’s variation of the second theorem, and the S ́wierczkowski–Paulson semantics-based approach. As part of our framework’s validation, we upgrade Paulson’s Isabelle proof to produce a mech- anization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation.

ConferenceCADE 27 - 27th International Conference on Automated Deduction
Page range442-461
EditorsFontaine, P.
ISSN0302-9743
ISBN
Hardcover9783030294359
Electronic9783030294366
PublisherSpringer
Publication dates
Print20 Aug 2019
Online20 Aug 2019
Publication process dates
Deposited12 Nov 2019
Accepted02 May 2019
Output statusPublished
Accepted author manuscript
Copyright Statement

This is the Author’s accepted version of a paper published in Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science, vol 11716 . The final authenticated version is available online at https://doi.org/10.1007/978-3-030-29436-6_26

Additional information

Popescu A., Traytel D. (2019) A Formally Verified Abstract Account of Gödel’s Incompleteness Theorems. In: Fontaine P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science, vol 11716. Springer, Cham

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-030-29436-6_26
LanguageEnglish
Book titleAutomated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science, vol 11716
Permalink -

https://repository.mdx.ac.uk/item/88966

Log in to edit

Download files

Accepted author manuscript
Goedel_CADE_2019.pdf

  • 83
    total views
  • 25
    total downloads
  • 6
    views this month
  • 1
    downloads this month

Export as

Related outputs

CoCon: A conference management system with formally verified document confidentiality
Popescu, A., Lammich, P. and Hou, P. 2021. CoCon: A conference management system with formally verified document confidentiality. Journal of Automated Reasoning. 65 (2), pp. 321-356. https://doi.org/10.1007/s10817-020-09566-9
Bindings as bounded natural functors
Blanchette, J., Gheri, L., Popescu, A. and Traytel, D. 2019. Bindings as bounded natural functors. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Hotel Cascais Miragem, Cascais, Portugal 13 - 19 Jan 2019 Association for Computing Machinery (ACM). https://doi.org/10.1145/3290335
A formalized general theory of syntax with bindings
Gheri, L. and Popescu, A. 2017. A formalized general theory of syntax with bindings. 8th International Conference Interactive Theorem Proving. Brasilia, Brazil 26 - 29 Sep 2017 Cham Springer International Publishing. pp. 241-261 https://doi.org/10.1007/978-3-319-66107-0_16
Foundational (co)datatypes and (co)recursion for higher-order logic
Biendarra, J., Blanchette, J., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. and Traytel, D. 2017. Foundational (co)datatypes and (co)recursion for higher-order logic. 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017. Brasilia, Brazil 27 - 29 Sep 2017 Cham Springer International Publishing. pp. 3-21 https://doi.org/10.1007/978-3-319-66167-4_1
Safety and conservativity of definitions in HOL and Isabelle/HOL
Kunčar, O. and Popescu, A. 2018. Safety and conservativity of definitions in HOL and Isabelle/HOL. Proceedings of the ACM on Programming Languages. 2, pp. 1-26. https://doi.org/10.1145/3158112
CoSMed: a confidentiality-verified social media platform
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2018. CoSMed: a confidentiality-verified social media platform. Journal of Automated Reasoning. 61 (1-4), pp. 113-119. https://doi.org/10.1007/s10817-017-9443-3
A formalized general theory of syntax with bindings
Gheri, L. and Popescu, A. 2017. A formalized general theory of syntax with bindings. 8th International Conference Interactive Theorem Proving (ITP). Brasília, Brazil 26 - 29 Sep 2017 Springer. pp. 241-261 https://doi.org/10.1007/978-3-319-66107-0_16
Foundational nonuniform (co)datatypes for higher-order logic
Blanchette, J., Meier, F., Popescu, A. and Traytel, D. 2017. Foundational nonuniform (co)datatypes for higher-order logic. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reykjavik, Iceland 20 - 23 Jun 2017 IEEE. https://doi.org/10.1109/LICS.2017.8005071
Soundness and completeness proofs by coinductive methods
Blanchette, J., Popescu, A. and Traytel, D. 2017. Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning. 58 (1), pp. 149-179. https://doi.org/10.1007/s10817-016-9391-3
Friends with benefits: implementing corecursion in foundational proof assistants
Blanchette, J., Bouzy, A., Lochbihler, A., Popescu, A. and Traytel, D. 2017. Friends with benefits: implementing corecursion in foundational proof assistants. 26th European Symposium on Programming, ESOP 2017. Uppsala, Sweden 22 - 29 Apr 2017 Springer. https://doi.org/10.1007/978-3-662-54434-1_5
From types to sets by local type definitions in higher-order logic
Kunčar, O. and Popescu, A. 2016. From types to sets by local type definitions in higher-order logic. ITP 2016: 7th International Conference on Interactive Theorem Proving. Nancy, France 22 - 25 Aug 2016 Springer. https://doi.org/10.1007/978-3-319-43144-4_13
Comprehending Isabelle/HOL's consistency
Kunčar, O. and Popescu, A. 2017. Comprehending Isabelle/HOL's consistency. Yang, H. (ed.) ESOP 2017: 26th European Symposium on Programming (ESOP). Uppsala, Sweden 22 - 29 Apr 2017 Berlin, Heidelberg Springer. https://doi.org/10.1007/978-3-662-54434-1_27
CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2017. CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. 38th IEEE Symposium on Security and Privacy. San Jose, CA, USA 22 - 26 May 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 729-748 https://doi.org/10.1109/SP.2017.24
Encoding monomorphic and polymorphic types
Blanchette, J., Böhme, S., Popescu, A. and Smallbone, N. 2017. Encoding monomorphic and polymorphic types. Logical Methods in Computer Science. 12 (4). https://doi.org/10.2168/LMCS-12(4:13)2016
CoSMed: a confidentiality-verified social media platform
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2016. CoSMed: a confidentiality-verified social media platform. Blanchette, J.C. and Merz, S. (ed.) ITP 2016: 7th International Conference on Interactive Theorem Proving. Nancy, France 22 - 25 Aug 2016 Springer. pp. 87-106 https://doi.org/10.1007/978-3-319-43144-4_6
A consistent foundation for Isabelle/HOL
Kunčar, O. and Popescu, A. 2015. A consistent foundation for Isabelle/HOL. 6th conference on Interactive Theorem Proving (ITP). Nanjing, China 24 - 27 Aug 2015 Springer. pp. 234-252 https://doi.org/10.1007/978-3-319-22102-1_16
Weak bisimilarity coalgebraically
Popescu, A. 2009. Weak bisimilarity coalgebraically. Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009. Udine, Italy 07 - 10 Sep 2009 Springer. pp. 157-172
A semantic approach to interpolation
Popescu, A., Şerbănuţă, T. and Roşu, G. 2009. A semantic approach to interpolation. Theoretical Computer Science. 410 (12-13), pp. 1109-1128. https://doi.org/10.1016/j.tcs.2008.09.038
Incremental pattern-based coinduction for process algebra and its Isabelle formalization
Popescu, A. and Gunter, E. 2010. Incremental pattern-based coinduction for process algebra and its Isabelle formalization. Foundations of Software Science and Computation Structures (FOSSACS). Paphos, Cyprus 20 - 28 Mar 2010 Springer. pp. 109-127
More SPASS with Isabelle: superposition with hard sorts and configurable simplification
Blanchette, J., Popescu, A., Wand, D. and Weidenbach, C. 2012. More SPASS with Isabelle: superposition with hard sorts and configurable simplification. Interactive Theorem Proving (ITP), Third International Conference. Princeton, New Jersey, US 13 - 15 Aug 2012 Springer. pp. 345-360
Proving concurrent noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2012. Proving concurrent noninterference. 2nd International Conference on Certified Programs and Proofs (CPP 2012). Kyoto, Japan 13 - 15 Dec 2012 Springer. pp. 109-125
Formal verification of language-based concurrent noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Formal verification of language-based concurrent noninterference. Journal of Formalized Reasoning. 6 (1), pp. 1-30. https://doi.org/10.6092/issn.1972-5787/3690
Noninterfering schedulers: when possibilistic noninterference implies probabilistic noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Noninterfering schedulers: when possibilistic noninterference implies probabilistic noninterference. 5th Conference on Algebra and Coalgebra in Computer Science (CALCO). Warsaw, Poland 03 - 06 Sep 2013 Springer. pp. 236-252
Mechanizing the metatheory of sledgehammer
Blanchette, J. and Popescu, A. 2013. Mechanizing the metatheory of sledgehammer. 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013). Nancy, France 18 - 20 Sep 2013 Springer. pp. 245-260
Formalizing probabilistic noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Formalizing probabilistic noninterference. 3rd International Conference on Certified Programs and Proofs (CPP 2013). Melbourne, VIC, Australia 11 - 13 Dec 2013 Springer International Publishing. pp. 259-275
Nonfree datatypes in Isabelle/HOL: animating a many-sorted metatheory
Schropp, A. and Popescu, A. 2013. Nonfree datatypes in Isabelle/HOL: animating a many-sorted metatheory. Certified Programs and Proofs (CPP). Melbourne, Australia 11 - 13 Dec 2013 Springer. pp. 114-130 https://doi.org/10.1007/978-3-319-03545-1_8
Witnessing (co)datatypes
Blanchette, J., Popescu, A. and Traytel, D. 2015. Witnessing (co)datatypes. 24th European Symposium on Programming (ESOP 2015). London, UK 11 - 18 Apr 2015 Springer. pp. 359-382
A conference management system with verified document confidentiality
Kanav, S., Lammich, P. and Popescu, A. 2014. A conference management system with verified document confidentiality. Biere, A. and Bloem, R. (ed.) 26th International Conference on Computer Aided Verification (CAV) 2014. Vienna, Austria 18 - 24 Jul 2014 Springer. pp. 167-183 https://doi.org/10.1007/978-3-319-08867-9_11
Unified classical logic completeness: a coinductive pearl
Blanchette, J., Popescu, A. and Traytel, D. 2014. Unified classical logic completeness: a coinductive pearl. 7th International Joint Conference on Automated Reasoning (IJCAR). Vienna, Austria 19 - 22 Jul 2014 Springer International Publishing. pp. 46-60
Making security type systems less ad hoc
Nipkow, T. and Popescu, A. 2014. Making security type systems less ad hoc. Information Technology. 56 (6), pp. 267-272. https://doi.org/10.1515/itit-2014-1060
Strong normalization for System F by HOAS on top of FOAS
Popescu, A., Gunter, E. and Osborn, C. 2010. Strong normalization for System F by HOAS on top of FOAS. 25th Annual IEEE Symposium on Logic in Computer Science (LICS). Edinburgh, United Kingdom 11 - 14 Jul 2010 Institute of Electrical and Electronics Engineers. pp. 31-40
Recursion principles for syntax with bindings and substitution
Popescu, A. and Gunter, E. 2011. Recursion principles for syntax with bindings and substitution. The 16th ACM SIGPLAN International Conference on Functional Programming. Tokyo 19 - 21 Sep 2011 Association for Computing Machinery (ACM). pp. 346-358
Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
Traytel, D., Popescu, A. and Blanchette, J. 2012. Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. 27th Annual IEEE Symposium on Logic in Computer Science (LICS). Dubrovnik, Croatia 25 - 28 Jun 2012 Institute of Electrical and Electronics Engineers (IEEE). pp. 596-605 https://doi.org/10.1109/LICS.2012.75
Truly modular (co)datatypes for Isabelle/HOL
Blanchette, J., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A. and Traytel, D. 2014. Truly modular (co)datatypes for Isabelle/HOL. 5th International Conference on Interactive Theorem Proving (ITP). Vienna, Austria 14 - 17 Jul 2014 Springer International Publishing. pp. 93-110
Cardinals in Isabelle/HOL
Blanchette, J., Popescu, A. and Taytel, D. 2014. Cardinals in Isabelle/HOL. 5th International Conference on Interactive Theorem Proving. Vienna, Austria 14 - 17 Jul 2014 Springer. pp. 111-127
Term-generic logic
Popescu, A. and Roşu, G. 2015. Term-generic logic. Theoretical Computer Science. 577, pp. 1-24. https://doi.org/10.1016/j.tcs.2015.01.047
Foundational extensible corecursion: a proof assistant perspective
Blanchette, J., Popescu, A. and Traytel, D. 2015. Foundational extensible corecursion: a proof assistant perspective. 20th ACM SIGPLAN International Conference on Functional Programming (ICFP). Vancouver, Canada 31 Aug - 02 Sep 2015 Association for Computing Machinery (ACM). pp. 192-204 https://doi.org/10.1145/2784731.2784732
Encoding monomorphic and polymorphic types
Blanchette, J., Böhme, S., Popescu, A. and Smallbone, N. 2013. Encoding monomorphic and polymorphic types. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Rome 16 - 24 Mar 2013 Springer. pp. 493-507