Propositional combinations of Σ-sentences in Heyting's Arithmetic
Albert Visser · Utrecht University Repository (Utrecht University) · 1994
This paper is mainly about Boolean combinations of Σ-formulas (B(Σ)-formulas) in HA. We prove a theorem guaranteeing that if a B(Σ)-formula is provable in HA, then a simpler one is also provable. Our theorem yields a characterization of the derived rules of HA for Σ-substitutions. Another application is a decision procedure for the closed fragment of the provability logic of HA. The proof of our theorem leads us to such varied subjects as NNIL-formulas, robust formulas and preservativity notions.