 By generalizing Mints’s Rule, Visser and de Jongh identified a recursively enumerable sequence of successively stronger admissible rules (“Visser’s rules”) which, they conjectured, formed a basis for the admissible rules of \(\mathbf{IPC}\) in the sense that every admissible rule is derivable from the disjunction property and one of the rules of the sequence. Building on work of Ghilardi [1999], Iemhoff [2001] succeeded in proving their conjecture. Rybakov [1997] proved that the collection of all admissible rules of \(\mathbf{IPC}\) is decidable but has no finite basis. Visser [2002] showed that his rules are also the admissible propositional rules of \(\mathbf{HA},\) and of \(\mathbf{HA}\) extended by Markov’s Principle MP (defined in Section 5.2 below). More recently, Jerabek [2008] found an independent basis for the admissible rules of \(\mathbf{IPC},\) with the property that no rule in the basis derives another.