WYKŁAD OTWARTY PROF. ALBERTA VISSERA „THE TWO GREAT PROBLEMS OF PURE PROVABILITY LOGIC”

Serdecznie zapraszamy na wykład otwarty prof. Alberta Vissera (Uniwersytet w Utrechcie), który poświęcony będzie omówieniu dwóch najważniejszych problemów otwartych logiki dowodliwości. Wykład przeznaczony będzie dla szerszej publiczności.

Miejsce: sala nr 4, WFZ, Krakowskie Przedmieście 3

Czas: poniedziałek 13.06.2022, godz. 16.45

Tytuł: The two great Problems of pure Provability Logic

Abstrakt: To study theories with sufficient coding is entering a wild world where one has little control. These theories are  marvelously complex. They include central foundational theories like Peano Arithmetic and Zermelo-Fraenkel Set Theory. In contrast modal propositional theories are relatively tame and allow us a measure of control. Miraculously, we can associate modal propositional theories in a systematic way to theories with coding. This idea is studied in provability logic. Here we interpret the modal necessity operator as provability in a theory.

The modal logic Löb’s Logic turns out to be sound for a wide range of theories (Löb 1955). Löb’s Logic turns out to be complete for a slightly narrower class of theories (Solovay 1976).

In our talk we briefly present the basic definitions of provability logic and then zoom in on the two great open problems of pure provability logic.

The first problem is the provability logic of weak theories. Solovay’s completeness proof works for theories where exponentiation is present. On the other hand, the Löb-style soundness proof works for much weaker theories. Can we extend Solovay’s theorem also to such weaker theories? Or, an even more exciting possibility, do we have more principles?  After the paper by Alessandro Berarducci and Rineke Verbrugge of 1990, the problem has lain dormant. It is generally considered as being too difficult.

The second problem is the provability logic of Heyting Arithmetic. In a sense, Solovay’s completeness result was too successful. The fact that completeness holds for so many theories makes the provability logic of a theory uninformative. If we switch to the consideration of constructive theories, this situation changes dramatically: a lush landscape of possible provability logics with many wild and exciting modal principles emerges.  Already in 1975, Daniel Leivant pointed out a principle valid in the provability logic of Heyting Arithmetic that is not in the intuitionistic version of Löb’s Logic. What is more Leivant’s principle is, in a weak sense, inconsistent with classical Löb’s Logic. The problem of the provability logic of Heyting Arithmetic has been open for more than 40 years. Recently, Mojtaba Mojtahedi wrote a paper in which a characterization is given. I am still checking his proof, but it is very hopeful that it is correct. If so, the problem is solved.

Link do transmisji ZOOM: 

Temat: Albert Visser’s lecture

Czas: 13 cze 2022 04:45 PM Warszawa

Dołącz do spotkania Zoom

https://us02web.zoom.us/j/87158774515?pwd=OVFTejFWN2FGdTVRTWdCUmdWR0djQT09

Identyfikator spotkania: 871 5877 4515

Kod dostępu: 688834