Proof Society Seminar 20.04.2026 (at 13:00 UTC = 14:00 BST = 15:00 CEST)
16 views
Skip to first unread message
Elaine Pimentel
Mar 24, 2026, 4:27:18 AM (2 days ago) Mar 24
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Dear all,
The next Proof Society Seminar will take place on Monday 20 April 2026 at 15:00 CEST. Our speaker will be Albert Visser from Utrecht University. Details can be found below.
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 next Proof Society Seminar will take place on Monday 20 April 2026 at 15:00 CEST. Our speaker will be Albert Visser from Utrecht University. Details can be found below.
20 April 2026, 13:00 UTC (= 14:00 BST = 15:00 CEST) Proof Society Seminar
Albert Visser (Utrecht University)
Markov CodingIn 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.
To find out how to attend, please visit the page:
Elaine.
-----------------------------------
Elaine Pimentel
Schools Outreach Lead
Professor of Logic and Computation
Deputy Director of the Computer Science and Philosophy programme
Programming Principles, Logic, and Verification
Department of Computer Science, Office: Room 3.11, 66-72 Gower Street
University College London
UCL Computer Science is an Athena Swan Gold award winner for gender equality
UCL is ranked among the top ten in the QS World University Rankings 2024 and is winner of The Times and Sunday Times University of the Year 2024
-----------------------------------
Reply all
Reply to author
Forward
0 new messages