A note on the independence of premiss rule

In this paper, we prove that certain theories of (many-sorted) intuitionistic predicate logic is closed under the independence of premiss rule (IPR). As corollaries, we show that HA and HAω extended by some non-classical axioms and non-constructive axioms are closed under IPR.

• Type: Journal
• Year: 2016
• Where: MLQ
• Authors: Hajime Ishihara, Takako Nemoto
• Keywords: MLQ 2016