The predicate modal logic of provability
QGL is the obvious predicate extension of the propositional modal logic GL which is PA-complete, that is complete for the interpretation of necessity as provability in the first order arithmetic PA. It is proved that several good properties of GL do not extend to QGL. It is not PA-complete, the counterexample being of the form \(\diamond\underline T\to\diamond \diamond t,\) where \(t\) is the constant truth, and \(\bar{T}\) is the only axiom of a consistent theory \(T\) such that PA proves \(Con(T)\to Con(PA+Con(PA)).\) To demonstrate the unprovability of the above formula in QGL, a Kripke countermodel is constructed and the completeness of QGL with respect to a suitable class of Kripke models (with transitive and reversely well-founded accessibility relation) is used. On the other hand, the formula \(\neg (\exists u\diamond P(u)\wedge\forall v\exists w\square (P(v)\to\square P(w)))\) is valid in all transitive and reversely well-founded frames, but unprovable in QGL, so QGL is not complete with respect to any class of frames. Propositional provability logics of all \(\Sigma_ 1\) sound r.e. extensions of PA coincide with GL. The formula \(\diamond\underline T\to\diamond \diamond t,\) where \(T\) is a finitely axiomatizable subtheory of ZF strong enough to construct the model of PA (so that PA proves \(Con(T)\to Con(PA+Con(PA))),\) is PA-valid but not ZF-valid. The fixed point theorem fails for QGL: there is no sentence \(B\) such that \(B\leftrightarrow\forall u\exists v\square (B\to P(u,v))\). Familiar proof for GL cannot be extended, since the substitution rule \(D\to (B\leftrightarrow C)/\square D\to (A(B)\leftrightarrow A(C)),\) when substituted occurrences are modalized, fails if some free variables of \(D\) are bound in \(A\). If the latter obstacle is removed, the proof goes through, which proves the uniqueness of fixed points in QGL and in PA. Several problems are formulated.
- Quantified modal logic and self-reference
- Predicate provability logic with non-modalized quantifiers
- Insolubility of Gödel-Löb logic with quantifiers of propositional variables
- Definability and commonsense reasoning
- The incompleteness of RGL
- Obituary: Franco Montagna (1948--2015)
- Incompleteness and the Barcan formula
- Axiomatising the Prior future in predicate logic
- On inclusions between quantified provability logics
- Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
- No escape from Vardanyan's theorem
- scientific article; zbMATH DE number 1670501 (Why is no real title available?)
- A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs
- Franco Montagna's work on provability logic and many-valued logic
- Liar-type paradoxes and the incompleteness phenomena
- Finite Kripke models and predicate logics of provability
- Proof-irrelevant model of CC with predicative induction and judgmental equality
- scientific article; zbMATH DE number 4204315 (Why is no real title available?)
- scientific article; zbMATH DE number 3924750 (Why is no real title available?)
- On modal systems having arithmetical interpretations
- On predicate provability logics and binumerations of fragments of Peano arithmetic
- scientific article; zbMATH DE number 4079379 (Why is no real title available?)
- scientific article; zbMATH DE number 4099258 (Why is no real title available?)
- scientific article; zbMATH DE number 1303428 (Why is no real title available?)
- On first-order theories with provability operator
- A proof-irrelevant model of Martin-Löf's logical framework
- A note on Barcan formula
- A cut-free proof system for a predicate extension of the logic of provability
- scientific article; zbMATH DE number 2174393 (Why is no real title available?)
- Arithmetical interpretations and Kripke frames of predicate modal logic of provability
- scientific article; zbMATH DE number 4197983 (Why is no real title available?)
- On strong provability predicates and the associated modal logics
- MONADIC INTUITIONISTIC AND MODAL LOGICS ADMITTING PROVABILITY INTERPRETATIONS
- An Arithmetically Complete Predicate Modal Logic
- AN ESCAPE FROM VARDANYAN’S THEOREM
- Quantified modal logics: one approach to rule (almost) them all!
- Predicate counterparts of modal logics of provability: high undecidability and Kripke incompleteness
- Variations on the Kripke trick
- Strictly positive fragments of the provability logic of Heyting arithmetic
- Neighbourhood and algebraic models for predicate modal logics with -rules
- Provability in predicate product logic
This page was built for publication: The predicate modal logic of provability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q800346)
