Substitutions of Σ10-sentences: explorations between intuitionistic propositional logic and intuitionistic arithmetic
✍ Scribed by Albert Visser
- Publisher
- Elsevier Science
- Year
- 2002
- Tongue
- English
- Weight
- 347 KB
- Volume
- 114
- Category
- Article
- ISSN
- 0168-0072
No coin nor oath required. For personal study only.
✦ Synopsis
This paper is concerned with notions of consequence. On the one hand, we study admissible consequence, speciÿcally for substitutions of 0 1 -sentences over Heyting arithmetic (HA). 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 0 1 -substitutions over HA coincides with NNIL-preservativity over intuitionistic propositional logic (IPC). Here NNIL is the class of propositional formulas with no nestings of implications to the left. The identical embedding of IPC-derivability (considered as a preorder and, thus, as a category) into a consequence relation (considered as a preorder) 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.