AN ESCAPE FROM VARDANYAN’S THEOREM

DOI10.1017/JSL.2022.38arXiv2102.13091OpenAlexW3132883413WikidataQ113858278 ScholiaQ113858278MaRDI QIDQ6140187FDOQ6140187

Authors: Ana de Almeida Borges, Joost J. Joosten 

Publication date: 22 December 2023

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

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)$.

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)

Cites Work

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

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)