Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq Article Swipe
Dominik Kirst
,
Marc Hermes
·
YOU?
·
· 2023
· Open Access
·
· DOI: https://doi.org/10.1007/s10817-022-09647-x
YOU?
·
· 2023
· Open Access
·
· DOI: https://doi.org/10.1007/s10817-022-09647-x
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.
Related Topics
Concepts
Metadata
- Type
- article
- Language
- en
- Landing Page
- https://doi.org/10.1007/s10817-022-09647-x
- https://link.springer.com/content/pdf/10.1007/s10817-022-09647-x.pdf
- OA Status
- hybrid
- Cited By
- 4
- References
- 36
- Related Works
- 10
- OpenAlex ID
- https://openalex.org/W4323980065
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W4323980065Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.1007/s10817-022-09647-xDigital Object Identifier
- Title
-
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in CoqWork title
- Type
-
articleOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2023Year of publication
- Publication date
-
2023-03-01Full publication date if available
- Authors
-
Dominik Kirst, Marc HermesList of authors in order
- Landing page
-
https://doi.org/10.1007/s10817-022-09647-xPublisher landing page
- PDF URL
-
https://link.springer.com/content/pdf/10.1007/s10817-022-09647-x.pdfDirect link to full text PDF
- Open access
-
YesWhether a free full text is available
- OA status
-
hybridOpen access status per OpenAlex
- OA URL
-
https://link.springer.com/content/pdf/10.1007/s10817-022-09647-x.pdfDirect OA link when available
- Concepts
-
Undecidable problem, Mathematics, Axiom, Decidability, Finitary, Discrete mathematics, Gödel's incompleteness theorems, Mathematical proof, Peano axioms, Computability, Binary relation, Algebra over a field, Computer science, Pure mathematics, Programming language, Gödel, GeometryTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
4Total citation count in OpenAlex
- Citations by year (recent)
-
2025: 1, 2024: 1, 2023: 1, 2022: 1Per-year citation counts (last 5 years)
- References (count)
-
36Number of works referenced by this work
- Related works (count)
-
10Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W4323980065 |
|---|---|
| doi | https://doi.org/10.1007/s10817-022-09647-x |
| ids.doi | https://doi.org/10.22028/d291-39696 |
| ids.openalex | https://openalex.org/W4323980065 |
| fwci | 0.76632866 |
| type | article |
| title | Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq |
| biblio.issue | 1 |
| biblio.volume | 67 |
| biblio.last_page | |
| biblio.first_page | |
| topics[0].id | https://openalex.org/T10126 |
| topics[0].field.id | https://openalex.org/fields/17 |
| topics[0].field.display_name | Computer Science |
| topics[0].score | 0.9976000189781189 |
| topics[0].domain.id | https://openalex.org/domains/3 |
| topics[0].domain.display_name | Physical Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1702 |
| topics[0].subfield.display_name | Artificial Intelligence |
| topics[0].display_name | Logic, programming, and type systems |
| topics[1].id | https://openalex.org/T12002 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.9927999973297119 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1703 |
| topics[1].subfield.display_name | Computational Theory and Mathematics |
| topics[1].display_name | Computability, Logic, AI Algorithms |
| topics[2].id | https://openalex.org/T11010 |
| topics[2].field.id | https://openalex.org/fields/17 |
| topics[2].field.display_name | Computer Science |
| topics[2].score | 0.9927999973297119 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/1702 |
| topics[2].subfield.display_name | Artificial Intelligence |
| topics[2].display_name | Logic, Reasoning, and Knowledge |
| funders[0].id | https://openalex.org/F4320323322 |
| funders[0].ror | https://ror.org/01jdpyv68 |
| funders[0].display_name | Universität des Saarlandes |
| is_xpac | False |
| apc_list.value | 2290 |
| apc_list.currency | EUR |
| apc_list.value_usd | 2890 |
| apc_paid.value | 2290 |
| apc_paid.currency | EUR |
| apc_paid.value_usd | 2890 |
| concepts[0].id | https://openalex.org/C192034797 |
| concepts[0].level | 3 |
| concepts[0].score | 0.7798871994018555 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q3502995 |
| concepts[0].display_name | Undecidable problem |
| concepts[1].id | https://openalex.org/C33923547 |
| concepts[1].level | 0 |
| concepts[1].score | 0.6455463767051697 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q395 |
| concepts[1].display_name | Mathematics |
| concepts[2].id | https://openalex.org/C167729594 |
| concepts[2].level | 2 |
| concepts[2].score | 0.5691430568695068 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q17736 |
| concepts[2].display_name | Axiom |
| concepts[3].id | https://openalex.org/C153269930 |
| concepts[3].level | 2 |
| concepts[3].score | 0.5560007691383362 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q430001 |
| concepts[3].display_name | Decidability |
| concepts[4].id | https://openalex.org/C2778003309 |
| concepts[4].level | 2 |
| concepts[4].score | 0.49974775314331055 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q5450381 |
| concepts[4].display_name | Finitary |
| concepts[5].id | https://openalex.org/C118615104 |
| concepts[5].level | 1 |
| concepts[5].score | 0.4631373882293701 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q121416 |
| concepts[5].display_name | Discrete mathematics |
| concepts[6].id | https://openalex.org/C180937797 |
| concepts[6].level | 3 |
| concepts[6].score | 0.45135414600372314 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q200787 |
| concepts[6].display_name | Gödel's incompleteness theorems |
| concepts[7].id | https://openalex.org/C108710211 |
| concepts[7].level | 2 |
| concepts[7].score | 0.4382857382297516 |
| concepts[7].wikidata | https://www.wikidata.org/wiki/Q11538 |
| concepts[7].display_name | Mathematical proof |
| concepts[8].id | https://openalex.org/C97489613 |
| concepts[8].level | 2 |
| concepts[8].score | 0.4350185990333557 |
| concepts[8].wikidata | https://www.wikidata.org/wiki/Q842755 |
| concepts[8].display_name | Peano axioms |
| concepts[9].id | https://openalex.org/C152062344 |
| concepts[9].level | 2 |
| concepts[9].score | 0.42562225461006165 |
| concepts[9].wikidata | https://www.wikidata.org/wiki/Q818888 |
| concepts[9].display_name | Computability |
| concepts[10].id | https://openalex.org/C65180967 |
| concepts[10].level | 2 |
| concepts[10].score | 0.4158875048160553 |
| concepts[10].wikidata | https://www.wikidata.org/wiki/Q130901 |
| concepts[10].display_name | Binary relation |
| concepts[11].id | https://openalex.org/C136119220 |
| concepts[11].level | 2 |
| concepts[11].score | 0.37950077652931213 |
| concepts[11].wikidata | https://www.wikidata.org/wiki/Q1000660 |
| concepts[11].display_name | Algebra over a field |
| concepts[12].id | https://openalex.org/C41008148 |
| concepts[12].level | 0 |
| concepts[12].score | 0.2445201575756073 |
| concepts[12].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[12].display_name | Computer science |
| concepts[13].id | https://openalex.org/C202444582 |
| concepts[13].level | 1 |
| concepts[13].score | 0.2311646044254303 |
| concepts[13].wikidata | https://www.wikidata.org/wiki/Q837863 |
| concepts[13].display_name | Pure mathematics |
| concepts[14].id | https://openalex.org/C199360897 |
| concepts[14].level | 1 |
| concepts[14].score | 0.19908025860786438 |
| concepts[14].wikidata | https://www.wikidata.org/wiki/Q9143 |
| concepts[14].display_name | Programming language |
| concepts[15].id | https://openalex.org/C2781302003 |
| concepts[15].level | 2 |
| concepts[15].score | 0.18193331360816956 |
| concepts[15].wikidata | https://www.wikidata.org/wiki/Q3294091 |
| concepts[15].display_name | Gödel |
| concepts[16].id | https://openalex.org/C2524010 |
| concepts[16].level | 1 |
| concepts[16].score | 0.0 |
| concepts[16].wikidata | https://www.wikidata.org/wiki/Q8087 |
| concepts[16].display_name | Geometry |
| keywords[0].id | https://openalex.org/keywords/undecidable-problem |
| keywords[0].score | 0.7798871994018555 |
| keywords[0].display_name | Undecidable problem |
| keywords[1].id | https://openalex.org/keywords/mathematics |
| keywords[1].score | 0.6455463767051697 |
| keywords[1].display_name | Mathematics |
| keywords[2].id | https://openalex.org/keywords/axiom |
| keywords[2].score | 0.5691430568695068 |
| keywords[2].display_name | Axiom |
| keywords[3].id | https://openalex.org/keywords/decidability |
| keywords[3].score | 0.5560007691383362 |
| keywords[3].display_name | Decidability |
| keywords[4].id | https://openalex.org/keywords/finitary |
| keywords[4].score | 0.49974775314331055 |
| keywords[4].display_name | Finitary |
| keywords[5].id | https://openalex.org/keywords/discrete-mathematics |
| keywords[5].score | 0.4631373882293701 |
| keywords[5].display_name | Discrete mathematics |
| keywords[6].id | https://openalex.org/keywords/gödels-incompleteness-theorems |
| keywords[6].score | 0.45135414600372314 |
| keywords[6].display_name | Gödel's incompleteness theorems |
| keywords[7].id | https://openalex.org/keywords/mathematical-proof |
| keywords[7].score | 0.4382857382297516 |
| keywords[7].display_name | Mathematical proof |
| keywords[8].id | https://openalex.org/keywords/peano-axioms |
| keywords[8].score | 0.4350185990333557 |
| keywords[8].display_name | Peano axioms |
| keywords[9].id | https://openalex.org/keywords/computability |
| keywords[9].score | 0.42562225461006165 |
| keywords[9].display_name | Computability |
| keywords[10].id | https://openalex.org/keywords/binary-relation |
| keywords[10].score | 0.4158875048160553 |
| keywords[10].display_name | Binary relation |
| keywords[11].id | https://openalex.org/keywords/algebra-over-a-field |
| keywords[11].score | 0.37950077652931213 |
| keywords[11].display_name | Algebra over a field |
| keywords[12].id | https://openalex.org/keywords/computer-science |
| keywords[12].score | 0.2445201575756073 |
| keywords[12].display_name | Computer science |
| keywords[13].id | https://openalex.org/keywords/pure-mathematics |
| keywords[13].score | 0.2311646044254303 |
| keywords[13].display_name | Pure mathematics |
| keywords[14].id | https://openalex.org/keywords/programming-language |
| keywords[14].score | 0.19908025860786438 |
| keywords[14].display_name | Programming language |
| keywords[15].id | https://openalex.org/keywords/gödel |
| keywords[15].score | 0.18193331360816956 |
| keywords[15].display_name | Gödel |
| language | en |
| locations[0].id | doi:10.1007/s10817-022-09647-x |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S99781599 |
| locations[0].source.issn | 0168-7433, 1573-0670 |
| locations[0].source.type | journal |
| locations[0].source.is_oa | False |
| locations[0].source.issn_l | 0168-7433 |
| locations[0].source.is_core | True |
| locations[0].source.is_in_doaj | False |
| locations[0].source.display_name | Journal of Automated Reasoning |
| locations[0].source.host_organization | https://openalex.org/P4310319900 |
| locations[0].source.host_organization_name | Springer Science+Business Media |
| locations[0].source.host_organization_lineage | https://openalex.org/P4310319900, https://openalex.org/P4310319965 |
| locations[0].source.host_organization_lineage_names | Springer Science+Business Media, Springer Nature |
| locations[0].license | other-oa |
| locations[0].pdf_url | https://link.springer.com/content/pdf/10.1007/s10817-022-09647-x.pdf |
| locations[0].version | publishedVersion |
| locations[0].raw_type | journal-article |
| locations[0].license_id | https://openalex.org/licenses/other-oa |
| locations[0].is_accepted | True |
| locations[0].is_published | True |
| locations[0].raw_source_name | Journal of Automated Reasoning |
| locations[0].landing_page_url | https://doi.org/10.1007/s10817-022-09647-x |
| locations[1].id | pmh:oai:publikationen.sulb.uni-saarland.de:20.500.11880/35767 |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306401551 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | False |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | SciDok (Saarland University and State Library) |
| locations[1].source.host_organization | https://openalex.org/I91712215 |
| locations[1].source.host_organization_name | Saarland University |
| locations[1].source.host_organization_lineage | https://openalex.org/I91712215 |
| locations[1].license | cc-by |
| locations[1].pdf_url | |
| locations[1].version | submittedVersion |
| locations[1].raw_type | doc-type:article |
| locations[1].license_id | https://openalex.org/licenses/cc-by |
| locations[1].is_accepted | False |
| locations[1].is_published | False |
| locations[1].raw_source_name | |
| locations[1].landing_page_url | http://dx.doi.org/10.22028/D291-39696 |
| locations[2].id | doi:10.22028/d291-39696 |
| locations[2].is_oa | True |
| locations[2].source.id | https://openalex.org/S7407052975 |
| locations[2].source.type | repository |
| locations[2].source.is_oa | False |
| locations[2].source.issn_l | |
| locations[2].source.is_core | False |
| locations[2].source.is_in_doaj | False |
| locations[2].source.display_name | Universität des Saarlandes |
| locations[2].source.host_organization | |
| locations[2].source.host_organization_name | |
| locations[2].license | cc-by |
| locations[2].pdf_url | |
| locations[2].version | |
| locations[2].raw_type | article |
| locations[2].license_id | https://openalex.org/licenses/cc-by |
| locations[2].is_accepted | False |
| locations[2].is_published | |
| locations[2].raw_source_name | |
| locations[2].landing_page_url | https://doi.org/10.22028/d291-39696 |
| indexed_in | crossref, datacite |
| authorships[0].author.id | https://openalex.org/A5067282848 |
| authorships[0].author.orcid | https://orcid.org/0000-0003-4126-6975 |
| authorships[0].author.display_name | Dominik Kirst |
| authorships[0].countries | DE |
| authorships[0].affiliations[0].institution_ids | https://openalex.org/I91712215 |
| authorships[0].affiliations[0].raw_affiliation_string | Saarland Informatics Campus, Saarland University, Saarbrücken, Germany |
| authorships[0].institutions[0].id | https://openalex.org/I91712215 |
| authorships[0].institutions[0].ror | https://ror.org/01jdpyv68 |
| authorships[0].institutions[0].type | education |
| authorships[0].institutions[0].lineage | https://openalex.org/I91712215 |
| authorships[0].institutions[0].country_code | DE |
| authorships[0].institutions[0].display_name | Saarland University |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Dominik Kirst |
| authorships[0].is_corresponding | True |
| authorships[0].raw_affiliation_strings | Saarland Informatics Campus, Saarland University, Saarbrücken, Germany |
| authorships[1].author.id | https://openalex.org/A5009337783 |
| authorships[1].author.orcid | https://orcid.org/0000-0002-0375-759X |
| authorships[1].author.display_name | Marc Hermes |
| authorships[1].countries | DE |
| authorships[1].affiliations[0].institution_ids | https://openalex.org/I91712215 |
| authorships[1].affiliations[0].raw_affiliation_string | Department of Mathematics, Saarland University, Saarbrücken, Germany |
| authorships[1].institutions[0].id | https://openalex.org/I91712215 |
| authorships[1].institutions[0].ror | https://ror.org/01jdpyv68 |
| authorships[1].institutions[0].type | education |
| authorships[1].institutions[0].lineage | https://openalex.org/I91712215 |
| authorships[1].institutions[0].country_code | DE |
| authorships[1].institutions[0].display_name | Saarland University |
| authorships[1].author_position | last |
| authorships[1].raw_author_name | Marc Hermes |
| authorships[1].is_corresponding | False |
| authorships[1].raw_affiliation_strings | Department of Mathematics, Saarland University, Saarbrücken, Germany |
| has_content.pdf | True |
| has_content.grobid_xml | True |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://link.springer.com/content/pdf/10.1007/s10817-022-09647-x.pdf |
| open_access.oa_status | hybrid |
| open_access.any_repository_has_fulltext | False |
| created_date | 2025-10-10T00:00:00 |
| display_name | Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq |
| has_fulltext | True |
| is_retracted | False |
| updated_date | 2025-11-06T03:46:38.306776 |
| primary_topic.id | https://openalex.org/T10126 |
| primary_topic.field.id | https://openalex.org/fields/17 |
| primary_topic.field.display_name | Computer Science |
| primary_topic.score | 0.9976000189781189 |
| primary_topic.domain.id | https://openalex.org/domains/3 |
| primary_topic.domain.display_name | Physical Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1702 |
| primary_topic.subfield.display_name | Artificial Intelligence |
| primary_topic.display_name | Logic, programming, and type systems |
| related_works | https://openalex.org/W2771600437, https://openalex.org/W2947474490, https://openalex.org/W1747453711, https://openalex.org/W1658739789, https://openalex.org/W2743782362, https://openalex.org/W1604839944, https://openalex.org/W3022639623, https://openalex.org/W2500186873, https://openalex.org/W3177449200, https://openalex.org/W4323980065 |
| cited_by_count | 4 |
| counts_by_year[0].year | 2025 |
| counts_by_year[0].cited_by_count | 1 |
| counts_by_year[1].year | 2024 |
| counts_by_year[1].cited_by_count | 1 |
| counts_by_year[2].year | 2023 |
| counts_by_year[2].cited_by_count | 1 |
| counts_by_year[3].year | 2022 |
| counts_by_year[3].cited_by_count | 1 |
| locations_count | 3 |
| best_oa_location.id | doi:10.1007/s10817-022-09647-x |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S99781599 |
| best_oa_location.source.issn | 0168-7433, 1573-0670 |
| best_oa_location.source.type | journal |
| best_oa_location.source.is_oa | False |
| best_oa_location.source.issn_l | 0168-7433 |
| best_oa_location.source.is_core | True |
| best_oa_location.source.is_in_doaj | False |
| best_oa_location.source.display_name | Journal of Automated Reasoning |
| best_oa_location.source.host_organization | https://openalex.org/P4310319900 |
| best_oa_location.source.host_organization_name | Springer Science+Business Media |
| best_oa_location.source.host_organization_lineage | https://openalex.org/P4310319900, https://openalex.org/P4310319965 |
| best_oa_location.source.host_organization_lineage_names | Springer Science+Business Media, Springer Nature |
| best_oa_location.license | other-oa |
| best_oa_location.pdf_url | https://link.springer.com/content/pdf/10.1007/s10817-022-09647-x.pdf |
| best_oa_location.version | publishedVersion |
| best_oa_location.raw_type | journal-article |
| best_oa_location.license_id | https://openalex.org/licenses/other-oa |
| best_oa_location.is_accepted | True |
| best_oa_location.is_published | True |
| best_oa_location.raw_source_name | Journal of Automated Reasoning |
| best_oa_location.landing_page_url | https://doi.org/10.1007/s10817-022-09647-x |
| primary_location.id | doi:10.1007/s10817-022-09647-x |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S99781599 |
| primary_location.source.issn | 0168-7433, 1573-0670 |
| primary_location.source.type | journal |
| primary_location.source.is_oa | False |
| primary_location.source.issn_l | 0168-7433 |
| primary_location.source.is_core | True |
| primary_location.source.is_in_doaj | False |
| primary_location.source.display_name | Journal of Automated Reasoning |
| primary_location.source.host_organization | https://openalex.org/P4310319900 |
| primary_location.source.host_organization_name | Springer Science+Business Media |
| primary_location.source.host_organization_lineage | https://openalex.org/P4310319900, https://openalex.org/P4310319965 |
| primary_location.source.host_organization_lineage_names | Springer Science+Business Media, Springer Nature |
| primary_location.license | other-oa |
| primary_location.pdf_url | https://link.springer.com/content/pdf/10.1007/s10817-022-09647-x.pdf |
| primary_location.version | publishedVersion |
| primary_location.raw_type | journal-article |
| primary_location.license_id | https://openalex.org/licenses/other-oa |
| primary_location.is_accepted | True |
| primary_location.is_published | True |
| primary_location.raw_source_name | Journal of Automated Reasoning |
| primary_location.landing_page_url | https://doi.org/10.1007/s10817-022-09647-x |
| publication_date | 2023-03-01 |
| publication_year | 2023 |
| referenced_works | https://openalex.org/W2066815568, https://openalex.org/W1600140070, https://openalex.org/W2064811181, https://openalex.org/W2568721247, https://openalex.org/W4236098198, https://openalex.org/W2769209754, https://openalex.org/W2906883693, https://openalex.org/W4311008361, https://openalex.org/W3122736276, https://openalex.org/W162931075, https://openalex.org/W3001646502, https://openalex.org/W2038625855, https://openalex.org/W3046678492, https://openalex.org/W4243198690, https://openalex.org/W2207376437, https://openalex.org/W3119563194, https://openalex.org/W2231754610, https://openalex.org/W158226905, https://openalex.org/W2121898499, https://openalex.org/W2015224901, https://openalex.org/W2969786701, https://openalex.org/W2045033949, https://openalex.org/W2068523159, https://openalex.org/W2283907753, https://openalex.org/W2047144334, https://openalex.org/W2020686398, https://openalex.org/W2104359558, https://openalex.org/W2490033929, https://openalex.org/W2953833525, https://openalex.org/W2907081672, https://openalex.org/W1855403548, https://openalex.org/W6968821612, https://openalex.org/W2126160338, https://openalex.org/W1647170492, https://openalex.org/W1507376847, https://openalex.org/W4238977241 |
| referenced_works_count | 36 |
| abstract_inverted_index.a | 86, 110, 128, 176, 200 |
| abstract_inverted_index.As | 175 |
| abstract_inverted_index.In | 73 |
| abstract_inverted_index.PA | 119 |
| abstract_inverted_index.We | 1 |
| abstract_inverted_index.ZF | 43 |
| abstract_inverted_index.as | 40, 42, 90, 100 |
| abstract_inverted_index.by | 53, 127, 168 |
| abstract_inverted_index.in | 10, 34, 85, 109, 156 |
| abstract_inverted_index.it | 94 |
| abstract_inverted_index.no | 104, 189 |
| abstract_inverted_index.of | 5, 23, 36, 58, 81, 113, 118, 132, 150, 159, 178, 181, 196 |
| abstract_inverted_index.on | 78, 136, 147 |
| abstract_inverted_index.to | 16, 96, 139 |
| abstract_inverted_index.we | 27, 192 |
| abstract_inverted_index.Coq | 21 |
| abstract_inverted_index.The | 115 |
| abstract_inverted_index.ZF, | 161 |
| abstract_inverted_index.all | 82, 163 |
| abstract_inverted_index.and | 31, 44, 66, 120, 141, 162, 188 |
| abstract_inverted_index.are | 125, 172 |
| abstract_inverted_index.for | 106 |
| abstract_inverted_index.our | 144 |
| abstract_inverted_index.set | 47, 123, 182 |
| abstract_inverted_index.the | 3, 13, 19, 67, 74, 79, 121, 148, 157, 179, 194 |
| abstract_inverted_index.(PA) | 39 |
| abstract_inverted_index.Coq, | 11 |
| abstract_inverted_index.Post | 68 |
| abstract_inverted_index.both | 29 |
| abstract_inverted_index.case | 158 |
| abstract_inverted_index.from | 56 |
| abstract_inverted_index.full | 160 |
| abstract_inverted_index.i.e. | 61 |
| abstract_inverted_index.need | 105 |
| abstract_inverted_index.only | 186 |
| abstract_inverted_index.rely | 146 |
| abstract_inverted_index.such | 89, 169 |
| abstract_inverted_index.type | 92 |
| abstract_inverted_index.well | 41 |
| abstract_inverted_index.with | 49, 103, 199 |
| abstract_inverted_index.Peano | 37 |
| abstract_inverted_index.axiom | 8 |
| abstract_inverted_index.based | 77 |
| abstract_inverted_index.cases | 117 |
| abstract_inverted_index.cover | 28 |
| abstract_inverted_index.logic | 198 |
| abstract_inverted_index.model | 112 |
| abstract_inverted_index.shown | 173 |
| abstract_inverted_index.still | 166 |
| abstract_inverted_index.tenth | 63 |
| abstract_inverted_index.their | 50 |
| abstract_inverted_index.these | 98 |
| abstract_inverted_index.using | 185 |
| abstract_inverted_index.(H10), | 65 |
| abstract_inverted_index.(PCP), | 71 |
| abstract_inverted_index.binary | 202 |
| abstract_inverted_index.define | 97 |
| abstract_inverted_index.models | 171 |
| abstract_inverted_index.obtain | 193 |
| abstract_inverted_index.single | 201 |
| abstract_inverted_index.theory | 131 |
| abstract_inverted_index.Coq’s | 91 |
| abstract_inverted_index.Library | 22 |
| abstract_inverted_index.Proofs. | 25 |
| abstract_inverted_index.further | 107 |
| abstract_inverted_index.general | 129 |
| abstract_inverted_index.growing | 20 |
| abstract_inverted_index.models, | 152 |
| abstract_inverted_index.problem | 64, 70 |
| abstract_inverted_index.related | 45 |
| abstract_inverted_index.setting | 76 |
| abstract_inverted_index.symbol, | 191 |
| abstract_inverted_index.systems | 9 |
| abstract_inverted_index.theory, | 93 |
| abstract_inverted_index.various | 6 |
| abstract_inverted_index.Abstract | 0 |
| abstract_inverted_index.approach | 15 |
| abstract_inverted_index.concrete | 116 |
| abstract_inverted_index.encoding | 108 |
| abstract_inverted_index.equality | 190 |
| abstract_inverted_index.finitary | 46 |
| abstract_inverted_index.focusing | 135 |
| abstract_inverted_index.many-one | 54 |
| abstract_inverted_index.semantic | 30 |
| abstract_inverted_index.standard | 151, 170 |
| abstract_inverted_index.suffices | 95 |
| abstract_inverted_index.theories | 124, 183 |
| abstract_inverted_index.axiomatic | 164 |
| abstract_inverted_index.deductive | 32 |
| abstract_inverted_index.definable | 84 |
| abstract_inverted_index.employing | 12 |
| abstract_inverted_index.existence | 149 |
| abstract_inverted_index.fragments | 35 |
| abstract_inverted_index.functions | 83, 102 |
| abstract_inverted_index.justified | 167 |
| abstract_inverted_index.mechanise | 2 |
| abstract_inverted_index.relation. | 203 |
| abstract_inverted_index.synthetic | 14, 75, 130 |
| abstract_inverted_index.theories, | 48 |
| abstract_inverted_index.additional | 154 |
| abstract_inverted_index.arithmetic | 38 |
| abstract_inverted_index.by-product | 177 |
| abstract_inverted_index.considered | 122 |
| abstract_inverted_index.entailment | 33 |
| abstract_inverted_index.equations, | 60 |
| abstract_inverted_index.extensions | 165 |
| abstract_inverted_index.formalised | 111 |
| abstract_inverted_index.formulated | 184 |
| abstract_inverted_index.membership | 187 |
| abstract_inverted_index.meta-level | 101 |
| abstract_inverted_index.reductions | 55, 99, 145 |
| abstract_inverted_index.underlying | 18 |
| abstract_inverted_index.well-known | 137 |
| abstract_inverted_index.Concretely, | 26 |
| abstract_inverted_index.Diophantine | 59 |
| abstract_inverted_index.Hilbert’s | 62 |
| abstract_inverted_index.assumptions | 155 |
| abstract_inverted_index.connections | 138 |
| abstract_inverted_index.consistency | 140 |
| abstract_inverted_index.established | 52 |
| abstract_inverted_index.first-order | 7, 197 |
| abstract_inverted_index.foundation, | 88 |
| abstract_inverted_index.incomplete. | 174 |
| abstract_inverted_index.solvability | 57 |
| abstract_inverted_index.undecidable | 133 |
| abstract_inverted_index.computation. | 114 |
| abstract_inverted_index.constructive | 87 |
| abstract_inverted_index.supplemented | 126 |
| abstract_inverted_index.Specifically, | 143 |
| abstract_inverted_index.computability | 17, 80 |
| abstract_inverted_index.necessitating | 153 |
| abstract_inverted_index.respectively. | 72 |
| abstract_inverted_index.Undecidability | 24 |
| abstract_inverted_index.correspondence | 69 |
| abstract_inverted_index.undecidability | 4, 51, 180, 195 |
| abstract_inverted_index.incompleteness. | 142 |
| abstract_inverted_index.axiomatisations, | 134 |
| cited_by_percentile_year.max | 95 |
| cited_by_percentile_year.min | 89 |
| corresponding_author_ids | https://openalex.org/A5067282848 |
| countries_distinct_count | 1 |
| institutions_distinct_count | 2 |
| corresponding_institution_ids | https://openalex.org/I91712215 |
| sustainable_development_goals[0].id | https://metadata.un.org/sdg/16 |
| sustainable_development_goals[0].score | 0.4300000071525574 |
| sustainable_development_goals[0].display_name | Peace, Justice and strong institutions |
| citation_normalized_percentile.value | 0.7180449 |
| citation_normalized_percentile.is_in_top_1_percent | False |
| citation_normalized_percentile.is_in_top_10_percent | False |