Logical Axiom Schemes of Peano Arithmetic [000J]

is a term that can be subsituted for in without any of its variables becoming unquantified.