Markov Coding

In this talk, I discuss an alternative to coding sequences over arithmetic using the betafunction. We employ a basic insight, going back to Jacob Nielsen, that the monoid of $\mathrm{SL}_2(\mathbb{Z})$-matrices with nonnegative integer coefficients is isomorphic to the free monoid of binary strings.This idea was employed by Andrej Markov jr for metamathematical purposes. The Markov coding allows us to do the first steps of arithmetisation in an entirely quantifier-free way. We discuss three basic results. First, the most important good properties that we have for the Markov coding over the integers generalise to arbitrary discretely ordered commutative rings. The non-trivial property in this context is Tarski’s Editor Property. This insight yields an alternative proof that $\mathrm{PA}^{-}$ is sequential. If time allows, we will have a brief look at how the coding behaves in some salient rings. Secondly, we have a variant of the incompleteness result by Amala Bezboruah and John Shepherdson. $\mathrm{PA}^{-}$ plus all true universal sentences does not prove the consistency of an extremely weak theory when proofs are coded Markov-style. Thirdly, we do not seem to get Löb’s Logic over $\mathrm{PA}^{-}$ when we use the Markov coding, but we still get a decent provability logic. For example, we have the uniqueness of modalised fixed points. So, e.g., modulo provable equivalence, there is just one Gödel sentence. A nice puzzle: I am more or less sure that the consistency statement for $\mathrm{PA}^{-}$ is not equivalent to its Gödel sentence, but I do not currently have a counterexample.