Realizability and independence of premiss : a note

Abstract

Independence of premiss is the axiom scheme ∀x[(¬A(x) → ∃yB(x, y)) → ∃y(¬A(x) → B(x, y))] The principle is underivable in HA, since it is inconsistent with ECT0. However, HA is closed under the derived rule: if HA ¬A → ∃yB(y), then HA ¬A → B(n), for some natural number n. A variation is the principle IP0: ∀x(Ax ∨ ¬Ax) ∧ (∀xAx → ∃yBy) → ∃y(∀xAx → By)