Por Ana Borges (University of Barcelona).
Vardanyan's Theorem states that quantified provability logic is Π^0_2-complete, and in particular impossible to recursively axiomatize for consistent theories containing a minimum of arithmetic. However, the proof of this fact cannot be performed in a strictly positive signature.
We define a (decidable) quantified strictly positive logic called QRC_1 and show that it is a provability logic: there is a Solovay-like completeness theorem relating QRC_1 to Peano Arithmetic.
This is joint work with Joost J. Joosten.
Transmissão via Zoom.