Related papers: On the Concept of Arithmetic Conseqeunce
Classical interpretations of Goedel's formal reasoning imply that the truth of some arithmetical propositions of any formal mathematical language, under any interpretation, is essentially unverifiable. However, a language of general,…
In this note we observe that automated theorem provers (ATPs) that recursively enumerate theorems in a particular way will fail to identify some valid theorems for a reason that is analogous to how G\"odel proved the existence of what are…
Hilbert and Ackermann asked for a method to consistently extend incomplete theories to complete theories. G\"odel essentially proved that any theory capable of encoding its own statements and their proofs contains statements that are true…
The proofs of Kleene, Chaitin and Boolos for G\"odel's First Incompleteness Theorem are studied from the perspectives of constructivity and the Rosser property. A proof of the incompleteness theorem has the Rosser property when the…
Our main result (Theorem A) shows the incompleteness of any consistent sequential theory T formulated in a finite language such that T is axiomatized by a collection of sentences of bounded quantifier-alternation-depth. Our proof employs an…
Godelian sentences of a sufficiently strong and recursively enumerable theory, constructed in Godel's 1931 groundbreaking paper on the incompleteness theorems, are unprovable if the theory is consistent; however, they could be refutable.…
In this paper we prove that no consistent finitely axiomatized theory one-dimensionally interprets its own extension with predicative comprehension. This constitutes a result with the flavor of the Second Incompleteness Theorem whose…
Many theorems of mathematics have the form that for a certain problem, e.g. a differential equation or polynomial (in)equality, there exists a solution. The sequential version then states that for a sequence of problems, there is a sequence…
We construct here an iterative evaluation of all PR map codes: progress of this iteration is measured by descending complexity within "Ordinal" O := N[\omega] of polynomials in one indeterminate, ordered lexicographically. Non-infinit…
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…
In this paper, we examine the limit of applicability of G\"{o}del's first incompleteness theorem ($\sf G1$ for short). We first define the notion "$\sf G1$ holds for the theory $T$". This paper is motivated by the following question: can we…
G{\"o}del's second incompleteness theorem forbids to prove, in a given theory U, the consistency of many theories-in particular, of the theory U itself-as well as it forbids to prove the normalization property for these theories, since this…
This is a short paper about the relationship between logic and computation. More specifically, it is about a relationship between the completeness proof for intuitionistic propositional logic within the form of proof-theoretic semantics…
We consider extensions of the language of Peano arithmetic by transfinitely iterated truth definitions satisfying uniform Tarskian biconditionals. Without further axioms, such theories are known to be conservative extensions of the original…
For which choices of $X,Y,Z\in\{\Sigma^1_1,\Pi^1_1\}$ does no sufficiently strong $X$-sound and $Y$-definable extension theory prove its own $Z$-soundness? We give a complete answer, thereby delimiting the generalizations of G\"odel's…
We investigate relationships between versions of derivability conditions for provability predicates. We show several implications and non-implications between the conditions, and we discuss unprovability of consistency statements induced by…
In this paper, we use G\"{o}del's incompleteness theorem as a case study for investigating mathematical depth. We take for granted the widespread judgment by mathematical logicians that G\"{o}del's incompleteness theorem is deep, and focus…
The famous G\"odel incompleteness theorem states that for every consistent sufficiently rich formal theory T there exist true statements that are unprovable in T. Such statements would be natural candidates for being added as axioms, but…
Analogous to G\"odel's incompleteness theorems is a theorem in physics to the effect that the set of explanations of given evidence is uncountably infinite. An implication of this theorem is that contact between theory and experiment…
We give a precise definition of a formal mathematical object as any symbol for an individual constant, predicate letter, or a function letter that can be introduced through definition into a formal mathematical language without inviting…