# Does the existence of Gödel Encoding imply that any formal system is itself already included in Peano arithmetic?

The notion of Gödel Encoding is extremely important from a philosophy of mathematics standpoint, but seems to be rarely noted explicitly. Take the following claims for example (which are implied by the inner-machinations of proofs such as Gödel's Second Incompleteness Theorem):

Claim #1: A consistent axiomatic system which includes Peano arithmetic can Gödel Encode ANY axiomatic system.

Claim #2: There does not exist any property of any consistent formal system which is not representable within Peano arithmetic.

Are these claims widely accepted as true? If so, it seems like this implies a perspective where the structure generated by Peano arithmetic contains all possible structures, and what formal systems do is merely select a subset of this structure to discuss with a particular language. If not, how can one hold the affirmative of something like Gödel's Second Incompleteness Theorem?

And finally, if lambda calculus includes Peano arithmetic (it does) and a universal turing machine includes Peano arithmetic (it does), then does this imply an affirmative proof of the Church-Turing Thesis?

• You claim 1 is already problematic since if there were such a consistent system including PA then Con(PA) becomes absolutely true which is not yet. It's well-known that ZFC ⊢ Con(ZFC – Infinity) together with the fact that we can build a model of ZFC – Infinity + (¬Infinity), thus the theory of (ZFC – Infinity) acts just like PA in a strong sense and consistent with the common conclusion that PA is relatively consistent with ZFC but Con(ZFC) is not absolute either. Your claim 2 is also violates Tarski's undefinability thm... Jul 29 at 3:05
• Also re your claim 1 for formal systems including PA but with some additional rules such as the famous infinitary ω-rule, then Gödel scheme obviously fails to encode such infinitary rule/axiom in any finite proof-theoretic way and you may need oracle machine. It's known with a random oracle P≠NP. As for CTT it's almost universally accepted but cannot be formally proved since its core concept of effective calculability/method/algo is not a purely formal mathematical concept... Jul 29 at 3:50
• IMO, the "encoding mechanism" is not "an extremely important from a philosophy of mathematics standpoint". The idea originated with Leibniz (and back to Ramon Llull) with the project of "arithmetize" the language and "compute" every problem/issue. If we formalize a theory T in e.g. first order language, we can encode into first order arithmetic the expressions of that theory, but I cannot imagine in what way this fact can improve our understanding of the mathematical facts that theory T is about... Jul 29 at 9:37

By my lights, claim number 1 is uncontroversial, we only need the fundamental theorem of arithmetic and some encoding scheme to get off the ground.

Claim number 2 is false, at least depending on your notion of representable. In particular, the property "there exists a proof for x", where x is the godel number of some formula, is only weakly representable. More generally, this will depend on the formal system. If the formal system is not recursively axiomatizable, the property "is an axiom of" is presumably not representable either.

As for your last question, it is unclear what a proof of the church -turing thesis would look like, as it is not a mathematical claim. But many people have thought that "equivalence" between turing machines, lambda calculi, and recursive functions is evidence for the CTT.

• Thank you. If the system contained the statement for saying "there exists a proof for x" wouldn't that make it the system inconsistent and thus in violation of a stated assumption of claim 2?
– TCP
Jul 28 at 19:50
• @TCP where is the inconsistency? Godel's result utilizes both (a) the consistency of the formal system F and (b) the predicate $\phi(x)$, where $\phi$ is the predicate saying there exists a proof for x. Jul 28 at 20:39
• Ah yes, my mistake, the predicate is a good counter example.
– TCP
Jul 29 at 2:49