Essential incompleteness of arithmetic verified by coq

O'CONNOR, Russell

In: TPHOLs 2005 : theorem proving in higher order logics (Oxford, 22-25 August 2005)Lecture notes in computer science :245-260

Konferenz - print, 14 ref

Wie komme ich dran?

A constructive proof of the Gödel-Rosser incompleteness the[. orem [9] has been completed using the Coq proof assistant. Some theory of classical first-order logic over an arbitrary language is formalized. A development of primitive recursive functions is given, and all primitive recursive functions are proved to be representable in a weak axiom system. Formulas and proofs are encoded as natural numbers, and functions operating on these codes are proved to be primitive recursive. The weak ' axiom system is proved to be essentially incomplete. In particular, Peano arithmetic is proved to be consistent in Coq's type theory and therefore is incomplete.

Titel:	Essential incompleteness of arithmetic verified by coq
Autor/in / Beteiligte Person:	O'CONNOR, Russell
Link:	E-Journal im Bestand der UB Hagen? View record from PASCAL Archive
Quelle:	TPHOLs 2005 : theorem proving in higher order logics (Oxford, 22-25 August 2005)Lecture notes in computer science :245-260
Veröffentlichung:	Berlin: Springer, 2005
Medientyp:	Konferenz
Umfang:	print, 14 ref
ISSN:	0302-9743 (print)
Schlagwort:	Computer science Informatique Mathematics Mathématiques Sciences exactes et technologie Exact sciences and technology Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Informatique théorique Theoretical computing Fonctions logiques, booléennes et de commutation Logical, boolean and switching functions Arithmétique Arithmetics Aritmética Démonstration automatique Automatic proving Demostración automática Démonstration théorème Theorem proving Demostración teorema Fonction récursive Recursive function Función recursiva Logique ordre 1 First order logic Lógica orden 1 Logique ordre supérieur High order logic Lógica orden superior Théorie preuve Proof theory Teoría demonstración Théorie type Type theory Vérification programme Program verification Verificación programa
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: English Original Material: INIST-CNRS Document Type: Conference Paper File Description: text Language: English Author Affiliations: Institute for Computing and Information Science, Faculty of Science, Radboud University Nijmegen, Netherlands ; The Group in Logic and the Methodology of Science, University of California, Berkeley, United States Rights: Copyright 2005 INIST-CNRS ; CC BY 4.0 ; Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS Notes: Computer science; theoretical automation; systems

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.