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.