Gödel's Second Incompleteness Theorem for General Recursive Arithmetic

We assume familiarity with our earlier paper [6]. In particular, we assume the formulation of the general recursive equational calculus, denoted by &gc, given in [6. 5 31. As in [6] we use PR as an abbreviation for “primitive recursive”. The implication sign -+ is defined as in [I, Ch. 31. We define x 12, yI = 0 (see [ l , Ch. 31). We assume familiarity with the PR functions and predicates defined in [3, pp. 69-71, 90-1001 and [6, 5 11. We also assume familiarity with the PR functions and predicates concerning the Godel numbering of the first-order PR arithmetic RA defined in [3, pp. 100-1101 (with the corrections noted in [6, S. i j ) .