This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

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.