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.

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property.

In this paper we describe a framework for the construction of entities that can serve as interpretations of arbitrary contiguous chunks of text. An important part of the paper is devoted to describing stacking cells, or the proposed meanings for bracket-structures.

This paper studies a propositional logic which is obtained by interpreting implication as formal provability. It is also the logic of finite irreflexive Kripke Models.A Kripke Model completeness theorem is given and several completeness theorems for interpretations into Provability Logic and Peano Arithmetic.

In this note we compare propositional logics for closed substitutions and propositional logics for open substitutions in constructive arithmetical theories. We provide a strong example where these logics diverge in an essential way. We prove that for Markov's Arithmetic, that is, Heyting's Arithmetic plus Markov's principle plus Extended Church's Thesis, the logic of closed and the logic of open substitutions are the same.

In this paper, we show that the predicate logics of consistent extensions of Heyting's Arithmetic plus Church's Thesis with uniqueness condition are complete $\Pi _{2}^{0}$. Similarly, we show that the predicate logic of HA*, i.e. Heyting's Arithmetic plus the Completeness Principle (for HA*) is complete $\Pi _{2}^{0}$. These results extend the known results due to Valery Plisko. To prove the results we adapt Plisko's method to use Tennenbaum's Theorem to prove 'categoricity of interpretations' under certain assumptions.

In this paper we study proofs of some general forms of the Second Incompleteness Theorem. These forms conform to the Feferman format, where the proof predicate is fixed and the representation of the set of axioms varies. We extend the Feferman framework in one important point: we allow the interpretation of number theory to vary.

In this paper we examine various requirements on the formalisation choices under which self-reference can be adequately formalised in arithmetic. In particular, we study self-referential numberings, which immediately provide a strong notion of self-reference even for expressively weak languages. The results of this paper suggest that the question whether truly self-referential reasoning can be formalised in arithmetic is more sensitive to the underlying coding apparatus than usually believed. As a case study, we show how this sensitivity affects the formal study (...) of certain principles of self-referential truth. (shrink)

This paper contains a careful derivation of principles of Interpretability Logic valid in extensions of I0+1.

In this paper, we study finitely axiomatizable conservative extensions of a theoryUin the case whereUis recursively enumerable and not finitely axiomatizable. Stanisław Krajewski posed the question whether there are minimal conservative extensions of this sort. We answer this question negatively.Consider a finite expansion of the signature ofUthat contains at least one predicate symbol of arity ≥ 2. We show that, for any finite extensionαofUin the expanded language that is conservative overU, there is a conservative extensionβofUin the expanded language, such that$\alpha (...) \vdash \beta$and$\beta \not \vdash \alpha$. The result is preserved when we consider eitherextensionsormodel-conservative extensionsofUinstead ofconservative extensions. Moreover, the result is preserved when we replace$\dashv$as ordering on the finitely axiomatized extensions in the expanded language by a relevant kind of interpretability, to witinterpretability that identically translates the symbols of the U-language.We show that the result fails when we consider an expansion with only unary predicate symbols for conservative extensions ofUordered by interpretability that preserves the symbols ofU. (shrink)

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.

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.

We show that a consistent, finitely axiomatized, sequential theory cannot prove its own inconsistency on every definable cut. A corollary is that there are at least three degrees of global interpretability of theories equivalent modulo local interpretability to a consistent, finitely axiomatized, sequential theory U.

In this paper, we characterize the strength of the predicative Frege hierarchy, , introduced by John Burgess in his book [J. Burgess, Fixing frege, in: Princeton Monographs in Philosophy, Princeton University Press, Princeton, 2005]. We show that and are mutually interpretable. It follows that is mutually interpretable with Q. This fact was proved earlier by Mihai Ganea in [M. Ganea, Burgess’ PV is Robinson’s Q, The Journal of Symbolic Logic 72 619–624] using a different proof. Another consequence of the our (...) main result is that is mutually interpretable with Kalmar Arithmetic . The fact that interprets EA was proved earlier by Burgess. We provide a different proof. Each of the theories is finitely axiomatizable. Our main result implies that the whole hierarchy taken together, , is not finitely axiomatizable. What is more: no theory that is mutually locally interpretable with is finitely axiomatizable. (shrink)

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)

This paper is concerned with notions of consequence. On the one hand, we study admissible consequence, specifically for substitutions of Σ 1 0 -sentences over Heyting arithmetic . On the other hand, we study preservativity relations. The notion of preservativity of sentences over a given theory is a dual of the notion of conservativity of formulas over a given theory. We show that admissible consequence for Σ 1 0 -substitutions over HA coincides with NNIL -preservativity over intuitionistic propositional logic . (...) Here NNIL is the class of propositional formulas with no nestings of implications to the left . The identical embedding of IPC -derivability into a consequence relation has in many cases a left adjoint. The main tool of the present paper will be an algorithm to compute this left adjoint in the case of NNIL -preservativity. In the last section, we employ the methods developed in the paper to give a characterization the closed fragment of the provability logic of HA. (shrink)

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 how to interpret Robinson’s arithmetic Q and the theory R of Tarski, Mostowski, and Robinson as theories of cardinals in very weak theories of relations over a domain.

In this paper we study 1. the frame-theory of certain bimodal provability logics involving the reflection principle and we study2. certain specific bimodal logics with a provability predicate for a subtheory of Peano arithmetic axiomatized by a non-standardly finite number of axioms.

A Kripke model ? is a submodel of another Kripke model ℳ if ? is obtained by restricting the set of nodes of ℳ. In this paper we show that the class of formulas of Intuitionistic Predicate Logic that is preserved under taking submodels of Kripke models is precisely the class of semipositive formulas. This result is an analogue of the Łoś-Tarski theorem for the Classical Predicate Calculus.In Appendix A we prove that for theories with decidable identity we can take (...) as the embeddings between domains in Kripke models of the theory, the identical embeddings. This is a well known fact, but we know of no correct proof in the literature. In Appendix B we answer, negatively, a question posed by Sam Buss: whether there is a classical theory T, such that ℋT is HA. Here ℋT is the theory of all Kripke models ℳ such that the structures assigned to the nodes of ℳ all satisfy T in the sense of classical model theory. (shrink)

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 note we derive Robinson???s Arithmetic from Hume???s Principle in the context of very weak theories of classes and relations.

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.

The problem of Uniqueness and Explicit Definability of Fixed Points for Interpretability Logic is considered. It turns out that Uniqueness is an immediate corollary of a theorem of Smoryński.

In this paper we formulate a version of Second Incompleteness Theorem. The idea is that a sequential sentence has ‘consistency power’ over a theory if it enables us to construct a bounded interpretation of that theory. An interpretation of V in U is bounded if, for some n , all translations of V -sentences are U -provably equivalent to sentences of complexity less than n . We call a sequential sentence with consistency power over T a pro-consistency statement for T (...) . We study pro-consistency statements. We provide an example of a pro-consistency statement for a sequential sentence A that is weaker than an ordinary consistency statement for A . We show that, if A is $${{\sf S}^{1}_{2}}$$ , this sentence has some further appealing properties, specifically that it is an Orey sentence for EA . The basic ideas of the paper essentially involve sequential theories. We have a brief look at the wider environment of the results, to wit the case of theories with pairing. (shrink)

In his 1967 paper Vaught used an ingenious argument to show that every recursively enumerable first order theory that directly interprets the weak system VS of set theory is axiomatizable by a scheme. In this paper we establish a strengthening of Vaught's theorem by weakening the hypothesis of direct interpretability of VS to direct interpretability of the finitely axiomatized fragment VS2 of VS. This improvement significantly increases the scope of the original result, since VS is essentially undecidable, but VS2 has (...) decidable extensions. We also explore the ramifications of our work on finite axiomatizability of schemes in the presence of suitable comprehension principles. (shrink)

In this paper we prove that the preordering $\lesssim $ of provable implication over any recursively enumerable theory $T$ containing a modicum of arithmetic is uniformly dense. This means that we can find a recursive extensional density function $F$ for $\lesssim $. A recursive function $F$ is a density function if it computes, for $A$ and $B$ with $A\lnsim B$, an element $C$ such that $A\lnsim C\lnsim B$. The function is extensional if it preserves $T$-provable equivalence. Secondly, we prove a (...) general result that implies that, for extensions of elementary arithmetic, the ordering $\lesssim $ restricted to $\Sigma_{n}$-sentences is uniformly dense. In the last section we provide historical notes and background material. (shrink)

In this paper we introduce a notion of context for Groenendijk & Stokhof's Dynamic Predicate Logic DPL. We use these contexts to give a characterization of the relations on assignments that can be generated by composition from tests and random resettings in the case that we are working over an infinite domain. These relations are precisely the ones expressible in DPL if we allow ourselves arbitrary tests as a starting point. We discuss some possible extensions of DPL and the way (...) these extensions interact with our notion of context. (shrink)

In this paper we study the combined structure of the relations of theory-extension and interpretability between theories for the case of finitely axiomatised theories. We focus on two main questions. The first is definability of salient notions in terms of the structure. We show, for example, that local tolerance, locally faithful interpretability and the finite model property are definable over the structure. The second question is how to think about ‘good’ properties of theories that are independent of implementation details and (...) of ‘bad’ properties that do depend on implementation details. Our degree structure is suitable to study this contrast, since one of our basic relations, to wit theory-extension, is dependent on implementation details and the other relation, interpretability, is not. Nevertheless, we can define new good properties using bad ones. We introduce a new notion of sameness of theories i-bisimilarity that is second-order definable over our structure. We define a notion of goodness in terms of this relation. We call this notion being capital. We illustrate that some intuitively good properties, like being a complete theory, are not capital. (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 prove that the principles in the languagewith relation composition and dynamic implication, valid forall binary relations, are the same ones as the principlesvalid when we restrict ourselves to DPL-relations,i.e. relations generated from conditions (tests) and resettings.

We argue that thinking of the man-machine comparison in terms of a contest involves, in a reasonable scenario, a criterion of success that is neutral. This is because we want to avoid a petitio principii. We submit, however, that, by looking at things this way, one makes the most essential human things invisible. Thus, in a sense, the contest approach is self-defeating.

We study the arithmetical schema asserting that every eventually decreasing elementary recursive function has a limit. Some other related principles are also formulated. We establish their relationship with restricted parameter-free induction schemata. We also prove that the same principle, formulated as an inference rule, provides an axiomatization of the Σ2-consequences of IΣ1.Using these results we show that ILM is the logic of Π1-conservativity of any reasonable extension of parameter-free Π1-induction schema. This result, however, cannot be much improved: by adapting a (...) theorem of D. Zambella and G. Mints we show that the logic of Π1-conservativity of primitive recursive arithmetic properly extends ILM.In the third part of the paper we give an ordinal classification of -consequences of the standard fragments of Peano arithmetic in terms of reflection principles. This is interesting in view of the general program of ordinal analysis of theories, which in the most standard cases classifies Π-classes of sentences. (shrink)