This paper will introduce the notion of a naming convention and use this paradigm to both develop a new version of the Second Incompleteness Theorem and to describe when an axiom system can partially evade the Second Incompleteness Theorem.

The central result of this paper is the small‐is‐very‐small principle for restricted sequential theories. The principle says roughly that whenever the given theory shows that a definable property has a small witness, i.e., a witness in a sufficiently small definable cut, then it shows that the property has a very small witness: i.e., a witness below a given standard number. Which cuts are sufficiently small will depend on the complexity of the formula defining the property. We draw various consequences from (...) the central result. E.g., roughly speaking, (i) every restricted, recursively enumerable sequential theory has a finitely axiomatized extension that is conservative with respect to formulas of complexity ; (ii) every sequential model has, for any n, an extension that is elementary for formulas of complexity, in which the intersection of all definable cuts is the natural numbers; (iii) we have reflection for ‐sentences with sufficiently small witness in any consistent restricted theory U; (iv) suppose U is recursively enumerable and sequential. Suppose further that every recursively enumerable and sequential V that locally inteprets U, globally interprets U. Then, U is mutually globally interpretable with a finitely axiomatized sequential theory. The paper contains some careful groundwork developing partial satisfaction predicates in sequential theories for the complexity measure depth of quantifier alternations. (shrink)

In this paper we study the interpretations of a weak arithmetic, like Buss’s theory $\mathsf{S}^{1}_{2}$, in a given theory $U$. We call these interpretations the arithmetics of $U$. We develop the basics of the structure of the arithmetics of $U$. We study the provability logic of $U$ from the standpoint of the framework of the arithmetics of $U$. Finally, we provide a deeper study of the arithmetics of a finitely axiomatized sequential theory.

In this paper we study the idea of theories with containers, like sets, pairs, sequences. We provide a modest framework to study such theories. We prove two concrete results. First, we show that first-order theories of finite signature that have functional non-surjective ordered pairing are definitionally equivalent to extensions in the same language of the basic theory of non-surjective ordered pairing. Second, we show that a first-order theory of finite signature is sequential (is a theory of sequences) iff it is (...) definitionally equivalent to an extension in the same language of a system of weak set theory called WS. (shrink)

Vardanyan's theorem states that the set of PA-valid principles of Quantified Modal Logic, QML, is complete Π0 2. We generalize this result to a wide class of theories. The crucial step in the generalization is avoiding the use of Tennenbaum's Theorem.

In this paper we study local induction w.r.t. Σ1‐formulas over the weak arithmetic. The local induction scheme, which was introduced in, says roughly this: for any virtual class that is progressive, i.e., is closed under zero and successor, and for any non‐empty virtual class that is definable by a Σ1‐formula without parameters, the intersection of and is non‐empty. In other words, we have, for all Σ1‐sentences S, that S implies, whenever is progressive. Since, in the weak context, we have (at (...) least) two definitions of Σ1, we obtain two minimal theories of local induction w.r.t. Σ1‐formulas, which we call Peano Corto and Peano Basso.In the paper we give careful definitions of Peano Corto and Peano Basso. We establish their naturalness both by giving a model theoretic characterization and by providing an equivalent formulation in terms of a sentential reflection scheme.The theories Peano Corto and Peano Basso occupy a salient place among the sequential theories on the boundary between weak and strong theories. They bring together a powerful collection of principles that is locally interpretable in. Moreover, they have an important role as examples of various phenomena in the metamathematics of arithmetical (and, more generally, sequential) theories. We illustrate this by studying their behavior w.r.t. interpretability, model interpretability and local interpretability. In many ways the theories are more like Peano arithmetic or Zermelo Fraenkel set theory, than like finitely axiomatized theories as Elementary Arithmetic, and. On the one hand, Peano Corto and Peano Basso are very weak: they are locally cut‐interpretable in. On the other hand, they behave as if they were strong: they are not contained in any consistent finitely axiomatized arithmetical theory, however strong. Moreover, they extend, the theory of parameter‐free Π1‐induction. (shrink)

In this paper we show that the degrees of interpretability of finitely axiomatized extensions-in-the-same-language of a finitely axiomatized sequential theory—like Elementary Arithmetic EA, IΣ1, or the Gödel–Bernays theory of sets and classes GB—have suprema. This partially answers a question posed by Švejdar in his paper (Commentationes Mathematicae Universitatis Carolinae 19:789–813, 1978). The partial solution of Švejdar’s problem follows from a stronger fact: the convexity of the degree structure of finitely axiomatized extensions-in-the-same-language of a finitely axiomatized sequential theory in the degree (...) structure of the degrees of all finitely axiomatized sequential theories. In the paper we also study a related question: the comparison of structures for interpretability and derivability. In how far can derivability mimic interpretability? We provide two positive results and one negative result. (shrink)

A theory T is trustworthy iff, whenever a theory U is interpretable in T, then it is faithfully interpretable. In this paper we give a characterization of trustworthiness. We provide a simple proof of Friedman’s Theorem that finitely axiomatized, sequential, consistent theories are trustworthy. We provide an example of a theory whose schematic predicate logic is complete Π20.

In his paper "Undecidability without arithmetization," Andrzej Grzegorczyk introduces a theory of concatenation $\mathsf{TC}$. We show that pairing is not definable in $\mathsf{TC}$. We determine a reasonable extension of $\mathsf{TC}$ that is sequential, that is, has a good sequence coding.

Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal (...) logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are such that there is an algorithm for checking if they are satisfied by a sequent calculus. (shrink)

Extending previous results from work on the complexity of cut elimination for the sequent calculus LK, we discuss the role of quantifier alternations and develop a measure to describe the complexity of cut elimination in terms of quantifier alternations in cut formulas and contractions on such formulas.

It can be argued that only the equational theories of some sub-elementary function algebras are finitistic or intuitive according to a certain interpretation of Hilbert's conception of intuition. The purpose of this paper is to investigate the relation of those restricted forms of equational reasoning to classical quantifier logic in arithmetic. The conclusion reached is that Edward Nelson's ‘predicative arithmetic’ program, which makes essential use of classical quantifier logic, cannot be justified finitistically and thus requires a different philosophical foundation, possibly (...) as a restricted form of logicism. (shrink)

Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is animpassable barrierin the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted inbut also what cannot be so (...) interpreted. We explain some of these results and rely on them to discuss Nelson's position. (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)

By a result of Paris and Friedman, the collection axiom schema for $\Sigma_{n+1}$ formulas, $B\Sigma_{n+1}$ , is $\Pi_{n+2}$ conservative over $I\Sigma_n$ . We give a new proof-theoretic proof of this theorem, which is based on a reduction of $B\Sigma_n$ to a version of collection rule and a subsequent analysis of this rule via Herbrand's theorem. A generalization of this method allows us to improve known results on reflection principles for $B\Sigma_n$ and to answer some technical questions left open by Sieg (...) [23] and Hájek [9]. We also give a new proof of independence of $B\Sigma_{n+1}$ over $I\Sigma_n$ by a direct recursion-theoretic argument and answer an open problem formulated by Gaifman and Dimitracopoulos [8]. (shrink)

This paper is concerned with the logical structure of arithmetical theories. We survey results concerning logics and admissible rules of constructive arithmetical theories. We prove a new theorem: the admissible propositional rules of Heyting Arithmetic are the same as the admissible propositional rules of Intuitionistic Propositional Logic. We provide some further insights concerning predicate logical admissible rules for arithmetical theories.