Papers βΊ An Escape from Vardanyan's Theorem
An Escape from Vardanyan's Theorem
Ana de Almeida Borges, Joost J. Joosten
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
Vardanyan's Theorems state that π°π―π«(π―π ) - the quantified provability logic of Peano Arithmetic - is Ξ β°β 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 π°π±π’β 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 π°π±π’β 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 π°π±π’β is the strictly positive fragment of π°π¦π« and a fragment of π°π―π«(π―π ).
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change Β· a person checks every report against the paper or source before anything changes; decisions are listed on /corrections