A note on the independence of premiss rule
Hajime Ishihara, Takako Nemoto · Mathematical logic quarterly · 2016
In this note, we prove that certain theories of (many‐sorted) intuitionistic predicate logic are closed under the independence of premiss rule (IPR). As corollaries, we show that and extended by some non‐classical axioms and non‐constructive axioms are closed under IPR.