
TL;DR
This paper explores two methods of encoding sequences in arithmetical theories, focusing on their conditions for effectiveness and introducing the concept of ur-strings, with applications to proving properties of Peano arithmetic.
Contribution
It compares two string coding methods within arithmetical theories and provides new insights into their capabilities and limitations, including an alternative proof of PA's sequentiality.
Findings
Both coding methods work under specific conditions.
The Markov coding offers an alternative proof of PA's sequentiality.
The study clarifies the creation of ur-strings in arithmetical theories.
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\v{r}\'abek. 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 is sequential.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
