[TYPES/announce] Proof Society Seminar 20.04.2026 (at 13:00 UTC = 14:00 BST = 15:00 CEST)

[Elaine Pimentel]

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.

*20 April 2026, 13:00 UTC** (= 14:00 BST = 15:00 CEST)** Proof Society
Seminar*

*Albert Visser (Utrecht University)*
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 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
<https://urldefense.com/v3/__https://www.proofsociety.org/proof-society-seminar/__;!!IBzWLUs!SysBw4e44P_UhCWnEl-R7RgHa7-eSlqXnZMMtlprjDKT6tHZSX5l5meCgvfyr0lYuXRwQhe1T3raP_uF5OwJoKy7yEXK43DrefvBjV_B$ > 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:
https://urldefense.com/v3/__https://www.proofsociety.org/proof-society-seminar/__;!!IBzWLUs!SysBw4e44P_UhCWnEl-R7RgHa7-eSlqXnZMMtlprjDKT6tHZSX5l5meCgvfyr0lYuXRwQhe1T3raP_uF5OwJoKy7yEXK43DrefvBjV_B$ 

-- 
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
URL: https://urldefense.com/v3/__https://sites.google.com/site/elainepimentel/__;!!IBzWLUs!SysBw4e44P_UhCWnEl-R7RgHa7-eSlqXnZMMtlprjDKT6tHZSX5l5meCgvfyr0lYuXRwQhe1T3raP_uF5OwJoKy7yEXK43DreVgVBXkf$ 

UCL Computer Science is an *Athena Swan Gold award winner for gender
equality
<https://urldefense.com/v3/__https://www.ucl.ac.uk/computer-science/about/equity-diversity-and-inclusion/gender-equality-athena-swan__;!!IBzWLUs!SysBw4e44P_UhCWnEl-R7RgHa7-eSlqXnZMMtlprjDKT6tHZSX5l5meCgvfyr0lYuXRwQhe1T3raP_uF5OwJoKy7yEXK43DreawhCV03$ >*
UCL is ranked among the *top ten in the QS World University Rankings 2024
<https://urldefense.com/v3/__https://www.ucl.ac.uk/news/2023/jun/ucl-ranked-top-10-universities-world-12-years-running__;!!IBzWLUs!SysBw4e44P_UhCWnEl-R7RgHa7-eSlqXnZMMtlprjDKT6tHZSX5l5meCgvfyr0lYuXRwQhe1T3raP_uF5OwJoKy7yEXK43Dreb-NV-07$ >*
and
is winner of *The Times and Sunday Times University of the Year 2024
<https://urldefense.com/v3/__https://www.ucl.ac.uk/news/2023/sep/ucl-named-university-year__;!!IBzWLUs!SysBw4e44P_UhCWnEl-R7RgHa7-eSlqXnZMMtlprjDKT6tHZSX5l5meCgvfyr0lYuXRwQhe1T3raP_uF5OwJoKy7yEXK43DreUvaVknv$ >*
-----------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20260324/a1376891/attachment-0001.htm>