AN ESCAPE FROM VARDANYAN’S THEOREM

DOI10.1017/JSL.2022.38MaRDI QIDQ6140187zbMATH OpenOpenAlexWikidataFDO

Authors Ana de Almeida Borges, Joost J. Joosten

Publication date 22 December 2023

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2102.13091

zbMATH Keywords

modal logicprovability logicquantified modal logicstrictly positive logicsarithmetic interpretationsfeasible fragments

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) First-order arithmetic and fragments (03F30) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45) Intuitionistic mathematics (03F55)

Abstract: Vardanyan's Theorems state that $mathsfQPL(mathsfPA)$ - the quantified provability logic of Peano Arithmetic - is $P{i}_2^0$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $mathsf{QRC}_1$ was previously introduced by the authors as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $mathsf{QRC}_1$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $mathsf{QRC}_1$ is the strictly positive fragment of $mathsfQGL$ and a fragment of $mathsfQPL(mathsfPA)$.

Cites work

• scientific article; zbMATH DE number 3976994 (Why is no real title available?)
• scientific article; zbMATH DE number 4010488 (Why is no real title available?)
• scientific article; zbMATH DE number 4087630 (Why is no real title available?)
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• scientific article; zbMATH DE number 1170091 (Why is no real title available?)
• scientific article; zbMATH DE number 1989643 (Why is no real title available?)
• scientific article; zbMATH DE number 755666 (Why is no real title available?)
• scientific article; zbMATH DE number 4118337 (Why is no real title available?)
• scientific article; zbMATH DE number 7585705 (Why is no real title available?)
• scientific article; zbMATH DE number 227056 (Why is no real title available?)
• A note on strictly positive logics and word rewriting systems
• A note on the model theory for positive modal logic
• An Arithmetically Complete Predicate Modal Logic
• Arithmetization of metamathematics in a general setting
• Calibrating provability logic: from modal logic to reflection calculus
• Finite Kripke models and predicate logics of provability
• Islands of tractability for relational constraints: towards dichotomy results for the description logic \({\mathcal{EL}}\)
• Kripke completeness of strictly positive modal logics over meet-semilattices with operators
• No escape from Vardanyan's theorem
• On axiomatizability within a system
• On inclusions between quantified provability logics
• On predicate provability logics and binumerations of fragments of Peano arithmetic
• On the positive fragment of the polymodal provability logic GLP
• PSPACE-decidability of Japaridze's polymodal logic
• Positive modal logic
• Positive provability logic for uniform reflection principles
• Provability interpretations of modal logic
• Provability logic and the completeness principle
• Refining the arithmetical hierarchy of classical principles
• Reflection algebras and conservation results for theories of iterated truth
• The degree of the set of sentences of predicate provability logic that are true under every interpretation
• The predicate modal logic of provability
• The worm principle

This page was built for publication: AN ESCAPE FROM VARDANYAN’S THEOREM

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6140187)