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.

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)

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)

We present a basis for the admissible rules of intuitionistic propositional logic. Thereby a conjecture by de Jongh and Visser is proved. We also present a proof system for the admissible rules, and give semantic criteria for admissibility.