HIGHER ORDER AND TRANSFINITE INCOMPLETENESS
J Zhang · Chinese Journal of Computers · 1981
Definition 1. Let be the number-theoretic formal system. The formula P(x) (where x is a variable, P(x) contains x free, and P(x) does not contain other variable free) in is said to be the formalization of the provability, if for any statement A in we have(1) If is consistent, then:(2) If is consistent, then:(3) If is ω-consistent, then:where A denote the Gdel number of the folmula A. In the present paper, we give the construction of the provability P(x).Definition 2. For any formalization of the provability P(x), and any statement A, we put where i=0,1,2,…, it is clear that A_i, A~i are all uniquely determined by formulas A, P(x) and natural number i.Theorem 1. If is consistent, for any formalization of the provability P(x) and any natural number n, then there is a statement A, such that where i=0, 1,2, …, n, and denotes B is unprovable in .Theorem 2. If is consistent, for any formalization of the provability P(x), then there is a statement A, such that where i=0, 1, 2, …