Blog Archives
Topic Archive: provability logic
Some abstract versions of Goedel’s Second Incompleteness Theorem based on non-classical logics
We study abstract versions of Goedel’s second incompleteness theorem and formulate generalizations of Loeb’s derivability conditions that work for logics weaker than the classical one. We isolate the role of the contraction and weakening rules in Goedel’s theorem and give a (toy) example of a system based on modal logic without contraction invalidating Goedel’s argument. On the other hand, Goedel’s theorem is established for a version of Peano arithmetic without contraction. (Joint work with Daniyar Shamkanov)
Reflection Principles Involving Provability and Explicit Proofs
Reflection principles are classical objects in proof theory and the areas studying Gödel’s Incompleteness. Reflection principles based on provability predicates were introduced in the 1930s by Rosser and Turing, and later were explored by Feferman, Kreisel & Levi, Schmerl, Artemov, Beklemishev and others.
We study reflection principles of Peano Arithmetic involving both Proof and Provability predicates. We find a classification of these principles and establish their linear ordering with respect to their metamathematical strength.