In 1981, Paris and Wilkie raised the open question about whether and to what extent the axiom system did satisfy the Second Incompleteness Theorem under Semantic Tableaux deduction. Our prior work showed that the semantic tableaux version of the Second Incompleteness Theorem did generalize for the most common definition of appearing in the standard textbooks.However, there was an alternate interesting definition of this axiom system in the Wilkie–Paris article in the Annals of Pure and Applied Logic 35 , pp. 261–302 (...) which we did not examine in our year-2002 article in the Journal of Symbolic Logic. Our first goal is to show that the incompleteness results of our prior paper can generalize in this alternate context. We will also develop a formal analysis, using a new technique called Passive Induction, that is simpler than the formalism we had used before.A further reason our results are of interest is that we have shown in a companion paper published in Electronic Notes in Theoretical Computer Science 165 , pp. 213–226 that some very unorthodox axiomizations for are anti-thresholds for the Herbrandized version of the Second Incompleteness Theorem. Thus, different axiomizations for have nearly fully opposite incompleteness properties.This paper is self-contained. It will not require a knowledge of our earlier results. (shrink)

Traces the development of recursive functions from their origins in the late nineteenth century to the mid-1930s, with particular emphasis on the work and influence of Kurt Gödel.

In this paper, we investigate Rosser provability predicates whose provability logics are normal modal logics. First, we prove that there exists a Rosser provability predicate whose provability logic is exactly the normal modal logic \. Secondly, we introduce a new normal modal logic \ which is a proper extension of \, and prove that there exists a Rosser provability predicate whose provability logic includes \.

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 derivability conditions. First, we classify already known versions of the second incompleteness theorem, and exhibit some new sets of conditions which are sufficient for unprovability of Hilbert–Bernays’ consistency statement. Secondly, we improve Buchholz’s schematic proof of provable $\Sigma_1$ -completeness. Then among other things, we show that Hilbert–Bernays’ conditions and Löb’s conditions are (...) mutually incomparable. We also show that neither Hilbert–Bernays’ conditions nor Löb’s conditions accomplish Gödel’s original statement of the second incompleteness theorem. (shrink)

Against the backdrop of the frequent comparison of theories of truth in the literature on semantic paradoxes with regard to which inferences and metainferences are deemed valid, this paper develops a novel approach to defining a binary predicate for representing the valid inferences and metainferences of a theory within the theory itself under the assumption that the theory is defined with a classical meta-theory. The aim with the approach is to obtain a tool which facilitates the comparison between a theory (...) and its competitors within the theory itself, thereby expressing the disagreement between the theories within the theories. After discussing what we can and should require of an object-linguistic representation of a theory for that purpose, this paper proposes to restrict the representation of valid metainferences to locally valid metainferences, a requirement which turns out to be \-consistent and conservative over classical first-order arithmetic. This approach is then applied to four theories definable on strong Kleene models using a labelled nested sequent calculus. (shrink)

This article will study a class of deduction systems that allow for a limited use of the modus ponens method of deduction. We will show that it is possible to devise axiom systems α that can recognize their consistency under a deduction system D provided that: (1) α treats multiplication as a 3-way relation (rather than as a total function), and that (2) D does not allow for the use of a modus ponens methodology above essentially the levels of Π1 (...) and Σ1 formulae. Part of what will make this boundary-case exception to the Second Incompleteness Theorem interesting is that we will also characterize generalizations of the Second Incompleteness Theorem that take force when we only slightly weaken the assumptions of our boundary-case exceptions in any of several further directions. (shrink)

We give a survey of current research on Gödel’s incompleteness theorems from the following three aspects: classifications of different proofs of Gödel’s incompleteness theorems, the limit of the applicability of Gödel’s first incompleteness theorem, and the limit of the applicability of Gödel’s second incompleteness theorem.