= Arithmetized deduction theorem
{title2=$\operatorname{Pr}_{T+A}(\ulcorner B\urcorner)\leftrightarrow\operatorname{Pr}_T(\ulcorner A\to B\urcorner)$}
For standard effective proof presentations, the syntactic <deduction theorem for first-order logic>[deduction theorem] and its reverse give effective transformations between proofs in a one-sentence extension and proofs of an implication in the base <first-order theory>[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 <full local reflection in a one-sentence extension is inconsistent>[reflection] step taking provability to truth.
Back to article page
