A Step Towards Absolute Versions of Metamathematical Results

There is a well-known gap between metamathematical theorems and their philosophical interpretations. Take Tarski's Theorem. According to its prevalent interpretation, the collection of all arithmetical truths is not arithmetically definable. However, the underlying metamathematical theorem merely establishes the arithmetical undefinability of a set of specific Godel codes of certain artefactual entities, such as infix strings, which are true in the standard model. That is, as opposed to its philosophical reading, the metamathematical theorem is formulated (and proved) relative to a specific choice of the Godel numbering and the notation system. A similar observation applies to Godel's and Church's theorems, which are commonly taken to impose severe limitations on what can be proved and computed using the resources of certain formalisms. The philosophical force of these limitative results heavily relies on the belief that these theorems do not depend on contingencies regarding the underlying formalisation choices. The main aim of this paper is to provide metamathematical facts which support this belief. While employing a fixed notation system, I showed in previous work (Review of Symbolic Logic, 2021, 14(1):51-84) how to abstract away from the choice of the Godel numbering. In the present paper, I extend this work by establishing versions of Tarski's, Godel's and Church's theorems which are invariant regarding both the notation system and the numbering. This paper thus provides a further step towards absolute versions of metamathematical results which do not rely on contingent formalisation choices.

Automated summary

There is a gap between metamathematical theorems and their philosophical interpretations, and the philosophical force of these theorems heavily relies on the belief that they do not depend on contingencies regarding formalisation choices. The paper aims to provide metamathematical facts that support this belief and extends previous work by establishing invariant versions of important theorems that are not affected by choices of notation systems and numberings.