Conservativity of Heyting Implication Over Relevant Quantification
It is known that propositional relevant logics can be conservatively extended by the addition of a
Heyting (intuitionistic) implication connective. We show that this same conservativity holds for
a range of first-order relevant logics with strong identity axioms, using an adaptation of
Fine's stratified model theory.
For systems without identity, the question of conservatively adding Heyting implication is thereby
reduced to the question of conservatively adding the axioms for identity.
Some results in this direction are also obtained.
The conservative presence of Heyting implication allows the development of an alternative model
theory for quantified relevant logics.