2

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?

Improve this question
3
  • 1
    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...
    – Double Knot
    Commented Jul 29, 2022 at 3:05
  • 1
    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...
    – Double Knot
    Commented Jul 29, 2022 at 3:50
  • 1
    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...
    – Mauro ALLEGRANZA
    Commented Jul 29, 2022 at 9:37

2 Answers 2

Reset to default
2

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

Yes, any computable formal system S can be encoded in PA, meaning that there is a translation of each statement of the form ( S proves X ) to an arithmetic statement that can be proven by PA iff S proves X. This fact can be proven assuming that PA is (arithmetically) sound (i.e. proves only true arithmetic sentences).

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

No. Arithmetical soundness of a formal system that interprets PA cannot be encoded within PA, because PA cannot capture arithmetical truth.

Improve this answer
1
  • The CT thesis is not a precise statement, and hence cannot have a precise answer.
    – user21820
    Commented Mar 16 at 15:17
1

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.

Improve this answer
3
  • 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
    Commented Jul 28, 2022 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.
    – emesupap
    Commented Jul 28, 2022 at 20:39
  • Ah yes, my mistake, the predicate is a good counter example.
    – TCP
    Commented Jul 29, 2022 at 2:49

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .