  The usual reading of logical implication "A implies B" as "if A then B" fails
in intuitionistic logic: there are formulas A and B such that "A implies B" is
not provable, even though B is provable whenever A is provable. Intuitionistic
rules apparently do not capture interesting meta-properties of the logic and,
from a computational perspective, the programs corresponding to intuitionistic
proofs are not powerful enough. Such non-provable implications are nevertheless
admissible, and we study their behavior by means of a proof term assignment and
related rules of reduction. We introduce V, a calculus that is able to
represent admissible inferences, while remaining in the intuitionistic world by
having normal forms that are just intuitionistic terms. We then extend
intuitionistic logic with principles corresponding to admissible rules. As an
example, we consider the Kreisel-Putnam logic KP, for which we prove the strong
normalization and the disjunction property through our term assignment. This is
our first step in understanding the essence of admissible rules for
intuitionistic logic.
