#матлог #учёба #спецсеминар #не_мехмат #МИАН #ТД

Семинар отдела математической логики МИАН, Logic Online Seminar (www.mathnet.ru/rus/conf876), понедельник 16:00 MSK (UTC+3), online only

20.04.2026, Proof Society Seminar (https://www.proofsociety.org/activities-and-resources/proof-society-seminar/), Albert Visser (Utrecht University, https://www.uu.nl/staff/AVisser): Markov Coding (online talk)

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 SL_2(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 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. 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 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 PA^- is not equivalent to its Gödel sentence, but I do not currently have a counterexample.

The Proof Society Seminar features leading researchers in proof theory and related areas of logic. Talks are held online via Zoom, usually on Mondays, approximately once per month. They begin at 13:00 UTC and last up to 75 minutes, followed by questions.