From Numbers to Ur-Strings

TL;DR

The paper investigates two principal strategies for coding sequences in weak arithmetical theories: Smullyan coding, which leverages binary string representations within the arithmetic base, and Markov coding, which encodes strings via the special linear monoid ${ m SL}_2(b N)$. It introduces ur-strings as a flexible container notion that obviates explicit projection or length functions, enabling two modular constructions to produce sequences from ur-strings in weak theories such as ${PA}^-$. The author shows that Markov coding yields a new, direct proof that $PA^-$ is sequential and develops a detailed analysis of the associated string theories ${ m TC}_1$ and its extensions, including partitions and Editors principles, as an intermediary step. The work also provides a comprehensive Markov-coding framework, including normal forms and model-theoretic characterizations, and discusses extensions to Euclidean contexts and higher-level standard models, highlighting both the potential and the limitations of weak-theory sequence arithmetisation. Overall, this advances understanding of how to internalise satisfaction predicates and model extensions in very weak theories via structurally rich coding schemes.

Abstract

In this paper we examine two ways of coding sequences in arithmetical theories. We investigate under what conditions they work. To be more precise, we study the creation of objects of a data-type that we call ur-strings, roughly sequences where the components are ordered but where we do not have an explicitly given projection function. First, we have a brief look at the beta-function which was already carefully studied by Emil Jeřábek. We study in detail our two target constructions. These constructions both employ theories of strings. The first is based on Smullyan coding and the second on the representation of binary strings in the special linear monoid of the non-negative part of discretely ordered commutative rings as introduced by Markov. We use the Markov coding to obtain an alternative proof that ${\sf PA}^{-}$ is sequential.

Theorems & Definitions (169)

• Remark 1.1
• Remark 3.1
• Lemma 3.3: ${\sf PA}^-_{\sf jer}$, Jeřábek
• Lemma 3.4: ${\sf PA}^-_{\sf jer}$, Jeřábek
• Remark 3.5
• Remark 3.7
• Theorem 3.8: ${\sf PA}^-$
• proof
• Theorem 3.9: ${\sf PA}^-_{\sf jer}$ plus pa\ref{['presmurf']} plus pa\ref{['plimp16']}
• proof