arXiv subjects

Ana de Almeida Borges

Publications and source records attributed to Ana de Almeida Borges.

7 recordsLinked to original sources

arXiv2023

Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic

We determine the strictly positive fragment $\mathsf{QPL}^+(\mathsf{HA})$ of the quantified provability logic $\mathsf{QPL}(\mathsf{HA})$ of Heyting Arithmetic. We show that $\mathsf{QPL}^+(\mathsf{HA})$ is decidable and that it coincides with $\mathsf{QPL}^+(\mathsf{PA})$, which is the strictly positive fragment of the quantified provability logic of of Peano Arithmetic. This positively resolves a previous conjecture of the authors. On our way to proving these results, we carve out the strictly positive fragment $\mathsf{PL}^+(\mathsf{HA})$ of the provability logic $\mathsf{PL}(\mathsf{HA})$ of Heyting Arithmetic, provide a simple axiomatization, and prove it to be sound and complete for two types of arithmetical interpretations. The simple fragments presented in this paper should be contrasted with a 2022 result by Mojtahedi, where an axiomatization for $\mathsf{PL}(\mathsf{HA})$ is provided. This axiomatization, although decidable, is of considerable complexity.

math.LO↗

arXiv2023

UTC Time, Formally Verified

FV Time is a small-scale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet non-trivial, it nicely illustrates our methodology for verifying software with Coq. In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some general-purpose solutions that were produced as by-products and may be used in other verification projects. These include a refinement package between proof-oriented MathComp numbers and computation-oriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through brute-force computation.

cs.SE↗

arXiv2022

Towards a Coq formalization of a quantified modal logic

We present a Coq formalization of the Quantified Reflection Calculus with one modality, or $\mathsf{QRC}_1$. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The highlights are a deep embedding of $\mathsf{QRC}_1$ in the Coq proof assistant, a mechanization of the notion of Kripke model with varying domains and a formalization of the soundness theorem. We focus on the design decisions inherent to the formalization and the insights that led to new and simplified proofs.

cs.LO↗

arXiv2021

An Escape from Vardanyan's Theorem

Vardanyan's Theorems state that $\mathsf{QPL}(\mathsf{PA})$ - the quantified provability logic of Peano Arithmetic - is $Π^0_2$ 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 $\mathsf{QGL}$ and a fragment of $\mathsf{QPL}(\mathsf{PA})$.

math.LO↗

arXiv2020

Quantified Reflection Calculus with one modality

This paper presents the logic QRC$_1$, which is a strictly positive fragment of quantified modal logic. The intended reading of the diamond modality is that of consistency of a formal theory. Predicate symbols are interpreted as parametrized axiomatizations. We prove arithmetical soundness of the logic QRC$_1$ with respect to this arithmetical interpretation. Quantified provability logic is known to be undecidable. However, the undecidability proof cannot be performed in our signature and arithmetical reading. We conjecture the logic QRC$_1$ to be arithmetically complete. This paper takes the first steps towards arithmetical completeness by providing relational semantics for QRC$_1$ with a corresponding completeness proof. We also show the finite model property, which implies decidability.

math.LO↗

arXiv2019

The Worm Calculus

We present a propositional modal logic $\sf WC$, which includes a logical $verum$ constant $\top$ but does not have any propositional variables. Furthermore, the only connectives in the language of $\sf WC$ are consistency-operators $\langle α\rangle$ for each ordinal $α$. As such, we end up with a class-size logic. However, for all practical purposes, we can consider restrictions of $\sf WC$ up to a given ordinal. Given the restrictive signature of the language, the only formulas are iterated consistency statements, which are called worms. The theorems of $\sf WC$ are all of the form $A \vdash B$ for worms $A$ and $B$. The main result of the paper says that the well-known strictly positive logic $\sf RC$, called Reflection Calculus, is a conservative extension of $\sf WC$. As such, our result is important since it is the ultimate step in stripping spurious complexity off the polymodal provability logic $\sf{GLP}$, as far as applications to ordinal analyses are concerned. Indeed, it may come as a surprise that a logic as weak as $\sf WC$ serves the purpose of computing something as technically involved as the proof theoretical ordinals of formal mathematical theories.

math.LO↗

arXiv2018

When logic lays down the law

We analyse so-called computable laws, i.e., laws that can be enforced by automatic procedures. These laws should be logically perfect and unambiguous, but sometimes they are not. We use a regulation on road transport to illustrate this issue, and show what some fragments of this regulation would look like if rewritten in the image of logic. We further propose desiderata to be fulfilled by computable laws, and provide a critical platform from which to assess existing laws and a guideline for composing future ones.

cs.AI↗