From what i remember from Godel encoding there was alot of freedom in how one chooses to expresses the statement Con(PA), my question is if one can classify all statements, or some subclass of all statements equivalent to Con(PA)?
And if we add Con(PA+Con(PA)) and Con(PA+Con(PA)+Con(PA+Con(PA))) etc we get alot of statements about polyonomials, which are quite central in mathematics, my question is if this new powerful theory with all possible formulations of Con(PA) etc have any uses in pure number theory or other mainstream mathematics, is there a connection here? Can any "interesting" mathematics be encoded as Con(PA) ?
Also, does the sequence of polynomials Con(PA), Con(PA+Con(PA)) etc, converge in any sense? Is there a limiting statement which is approached as its iterated towards infinity?