related mathoverflow.net/questions/106507/…

I think this is principial point. In prove of the Incompleteness theorem there are two types of "numbers": numbers(individuals) and Godel numbers. And symbol # (out of Godelization and arithmetics). Godel numbers are some kind of codes or "names" for classes, alike irrational, transcendental numbers in analysis(second-order arithmetics) are "names" for classes of convergences. But in case of Godelization this is more large entity. When we meet Prov(#(P)) and Prov(#(Prov(#(P)))), in the Diagonal lemma prove, it is reminiscent of the Fixed-point theorems in analysis(higher-order).

for proof needed Godelization

@Lee Mosher: amen

consistency is a subject matter of Incompleteness theorem

my objections: every sentence or statement form defines class of his own proofs(statement form for every individual for wich he provable) and even classes of proofs between proofs an so on... after Godelization we obtain function that defines the Godel number of sentence(statement form) for sets/classes of Godel numbers of proofs and so on... quantification over sets higher order stuff Thus we have higher-order metatheory obtained from first-order arithmetics after Godelization of sintax

Actually I mean absolute consistency(not relative consistency, equiconsistency) We can not live on a volcano waiting for counterexample

I think that PA or PRA do not suffices And I do not sure that they are consistent

one consistent suffice