Abstract:
As shown in [3], any two classical Frege systems polynomially simulate each other. The same proof does not work for the intuitionistic Frege systems, since they can have non-derivable admissible rules. (The rule $A/B$ is derivable if formula $A\to B$ is derivable. The rule $A/B$ is admissible if for all substitutions $\sigma$ if $\sigma(A)$ is derivable then $\sigma(B)$ is derivable). In this paper we polynomially simulate a single admissible rule and show that any two intuitionistic Frege systems polynomially simulate each other.