Abstract

Several proof-theoretic notions of validity have been proposed in the literature, for which completeness of intuitionistic logic has been conjectured. We define validity for intuitionistic propositional logic in a way which is common to many of these notions, emphasizing that an appropriate notion of validity must be closed under substitution. In this definition we consider atomic systems whose rules are not only production rules, but may include rules that allow one to discharge assumptions. Our central result shows that Harrop’s rule is valid under substitution, which refutes the completeness conjecture for intuitionistic logic