 every (human) computation is provable in first-order predicate calculus with identity, in the sense that, given an appropriate formalization, each step of the computation can be derived from the instructions (possibly in conjunction with ancillary premises, e.g., well-known mathematical premises, or premises concerning numbers that are supplied to the computer at the start of the computation).