## Abstract

This paper is concerned with notions of consequence. On the one hand, we study admissible consequence, specifically 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.

Original language | English |
---|---|

Pages (from-to) | 227-271 |

Number of pages | 45 |

Journal | Annals of Pure and Applied Logic |

Volume | 114 |

Issue number | 1-3 |

DOIs | |

Publication status | Published - 15 Apr 2002 |

## Keywords

- Admissible rule
- Consequence relation
- Constructive logic
- Heyting's arithmetic
- Propositional logic
- Provability logic
- Schema

## Fingerprint

Dive into the research topics of 'Substitutions of Σ^{0}

_{1}-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic'. Together they form a unique fingerprint.