Essential Incompleteness of Arithmetic Verified by Coq
Russell O'Connor
备注：
This paper is part of the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005). For the associated Coq source files see the TeX sources, or see <http://r6.ca/Goedel20050512.tar.gz>
发表信息：
Russell O'Connor, Essential Incompleteness of Arithmetic Verified by Coq, Lecture Notes in Computer Science, Volume 3603, Aug 2005, Pages 245 - 260
A constructive proof of the Goedel-Rosser incompleteness theorem 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.
An Isabelle/HOL formalisation of Gödel's two incompleteness theorems is presented. The work follows Świerczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical encodings of syntax eliminates the necessity to formalise elementary number theory within an embedded logical calculus. The Isabelle formalisation uses two separate treatments of variable binding: the nominal package is shown to scale to a development of this complexity, while de Bruijn indices turn out to be ideal for coding syntax. Critical details of the Isabelle proof are…
Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead using the processor's floating-point unit, and propose code that the compiler can easily interleave with other computations. We fully proved the correctness of our algorithm, which mixes floating-point …
Interval arithmetic libraries provide the four elementary arithmetic operators for operand intervals bounded by floating-point numbers. Actual implementations need to make a large case analysis that considers, e.g., magnitude relations between all pairs of argument bounds, positional relations between the arguments and zero, and handling of the special values, infinities and NaN. Their correctness is not obvious as they are implemented by human hands, which comes to be critical for the reliability. This work provides a mechanically-verified interval arithmetic library. For this purpose, we uti…
This paper exposes a contradiction in the Zermelo-Fraenkel set theory with the axiom of choice (ZFC). While Godel's incompleteness theorems state that a consistent system cannot prove its consistency, they do not eliminate proofs using a stronger system or methods that are outside the scope of the system. The paper shows that the cardinalities of infinite sets are uncontrollable and contradictory. The paper then states that Peano arithmetic, or first-order arithmetic, is inconsistent if all of the axioms and axiom schema assumed in the ZFC system are taken as being true, showing that ZFC is in…
This paper is about the bar recursion operator in the context of classical realizability. After the pioneering work of Berardi, Bezem & Coquand [1], T. Streicher has shown [10], by means of their bar recursion operator, that the realizability models of ZF, obtained from usual models of $λ$-calculus (Scott domains, coherent spaces, . . .), satisfy the axiom of dependent choice. We give a proof of this result, using the tools of classical realizability. Moreover, we show that these realizability models satisfy the well ordering of $\mathbb{R}$ and the continuum hypothesis These formulas are ther…
It is quite well-known from Kurt Godel's (1931) ground-breaking result on the Incompleteness Theorem that rudimentary relations (i.e., those definable by bounded formulae) are primitive recursive, and that primitive recursive functions are representable in sufficiently strong arithmetical theories. It is also known, though perhaps not as well-known as the former one, that some primitive recursive relations are not rudimentary. We present a simple and elementary proof of this fact in the first part of the paper. In the second part, we review some possible notions of representability of function…
Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
National Technical University of Athens（雅典国立技术大学）；Harvey Mudd College（哈维穆德学院）；Boğaziçi University（博阿齐吉大学）；EPFL（洛桑联邦理工学院）；University of Belgrade（贝尔格莱德大学）；Indian Institute of Science（印度科学学院）
