Gödel numbers and arithmetic functions

Gödel numbers may be used to define a programming language, where sets of propositions may be studied using arithmetic functions.

Everything is a number.-Pythagoras

Let’s suppose we design a formal language, Gödel, using a finite set of symbols \(S \subset \mathbb{N}^*\).

Using the Unique Factorisation Theorem, any logical proposition \(\{\alpha_i\}_{i=1}^n \in S^n\) may be uniquely defined as follows:

\[\begin{equation} \mathcal{A} = \prod_{k=1}^n p_k^{\alpha_k} \tag{1} \end{equation}\]

where \(p_k\) is the kth prime.

To define a sequence of propositions, such as a proof or program, we may use the Unique Factorisation Theorem a second time:

\[\begin{equation} \zeta = \prod_{j=1}^n p_j^{\mathcal{A}_j} \tag{2} \end{equation}\]

and to encode a sequence of programs, we may use the Unique Factorisation Theorem yet again:

\[\begin{equation} \mathcal{T} = \prod_{i=1}^n p_i^{\zeta_i} \tag{3} \end{equation}\]

where \(\mathcal{T}\) denotes a theory.

One issue we have not yet carefully addressed is how we may distinguish integers of type \(\mathcal{A}, \zeta, \mathcal{T}\). In order to address this problem, it is necessary and sufficient to define a type hierarchy: \(\mathcal{A} \subset \zeta \subset \mathcal{T}\).

Thus, we have a formal system which allows us to encode programs, libraries of programs, and mathematical theorems in a uniquely-decodable manner via the Unique Factorisation Theorem. For an explicit decoder, it is sufficient to use an algorithm for integer factorisation.

As a natural consequence, sets of logical propositions may be studied using arithmetic functions.

References:

1. Gödel, K. “Über Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme, I.” Monatshefte für Math. u. Physik 38, 173-198, 1931.
2. Gödel, K. On Formally Undecidable Propositions of Principia Mathematica and Related Systems. New York: Dover, 1992.
3. Hardy, G. H.; Wright, E. M. (1979) [1938]. An Introduction to the Theory of Numbers (5th ed.). Oxford: Clarendon Press.