in T ). From this, and the proof of the second part of G1 itself (in which the first Derivability Condition, which is just the ‘only if’ direction of (c), figures prominently), we arrive at the following result, which is a generalized form of G2: If S is any consistent representing theory up to and including the represented theory T itself, ‘ProvT (x)’ any provability predicate for T, and ConT any formula of T of the form ‘- ProvT ([#])’, then ConT is not a theorem of S. To the extent that, in being a provability predicate for T, ‘ProvT (x)’ ‘expresses’ the notion of provability of the represented theory T, it seems fair to say that ConT expresses its consistency. And to the extent that this is true, it is sensible to read G2 as saying that for any representing theory S and any represented theory T extending S, if S is consistent, then the consistency of T is not provable in S.
See also COMPUTER THEORY, CONSISTENCY , HILBERT ‘ S PROGRAM , PROOF THEOR. M.D.