 Arithmetized deduction theorem

For standard effective proof presentations, the syntactic deduction theorem and its reverse give effective transformations between proofs in a one-sentence extension and proofs of an implication in the base theory. Arithmetic can verify these transformations, yielding the displayed internal equivalence under the usual representation and proof-predicate hypotheses. It distinguishes internal proof transformations from an unlicensed reflection step taking provability to truth.