Suitable logics: provability, temporal laws, and formalization

Abstract

This thesis explores various aspects of logic, encompassing provability logic, logical analysis of law, and formalization of both mathematics and software. We are particularly interested in the aspect of suitability, both in the sense of finding expressible and tractable fragments of certain logical systems, and in the sense of finding appropriate formal systems for describing certain legal texts. In the domain of provability logic, we introduce two novel calculi: the Worm Calculus (WC) and the Quantified Reflection Calculus with one modality (QRC1). Both WC and QRC1 are inspired by the Reflection Calculus (RC), introduced by Dashkov in 2012. All three logics are strictly positive provability logics, with WC and RC being propositional and polymodal, while QRC1 features a quantified language with a single modality. Worms are words in a numerical alphabet that have many possible readings, particularly as iterated consistency statements. Although the language of worms is very simple, it is remarkably expressive, and known to fully describe the closed fragment of RC. The Worm Calculus is a calculus in the language of worms that illustrates this power: RC is shown to be conservative over WC. Vardanyan showed in 1986 that the quantified provability logic of Peano Arithmetic (QPL(PA)) is Π02-complete, and in particular not recursively axiomatizable. We investigate the strictly positive fragment of QPL(PA), showing that QRC1 is a decidable axiomatization of that fragment. In the process, we prove soundness and completeness of QRC1 with respect to Kripke semantics and two flavors of arithmetical semantics. We also see that QRC1 is the strictly positive fragment of QK4 and of QGL, and of any logic in between those. In the realm of law and inspired by a collaboration with industry, we focus on two European transport regulations, examining certain articles with curious mathematical properties. Then we identify fragments of Monadic Second-order Logic capable of expressing specific segments of one of these regulations, and show how other fragments are less suitable. This effort illustrates some issues with the way the current regulations specify algorithms, and it hints at the role of model checking as a useful legal tool. Lastly, we delve into the formal verification of both mathematics and software using Coq, presenting two case studies. The first case study involves the formalization of modal logical results on QRC1. We describe the overall formalization strategy, focusing on the difficulties and adaptations of both definitions and proofs helpful for the formalization. Due to this process, we were able to identify a small number of improvements to the original proofs. The formalization of software is somewhat different from the formalization of mathematics, although they share many particularities. We use a general framework for software formalization that starts by writing a basic specification for each function, which is then iteratively refined with better algorithms, data structures, and error handling, culminating in extraction to OCaml. Our case study is the formalization of UTC calendars, particularly functions to translate between human-readable times and timestamps, as well as functions to perform time arithmetic. This is a first step towards the formalization of laws that depend on time keeping, of which there are many, including the ones studied here.

Keywords

Modal logic, provability logic, strictly positive logic, quantified modal logic, feasible fragments, monadic second order logic, formal analysis of law, formal verification, Coq

Citation

de Almeida Borges, A. (2023). Suitable logics: provability, temporal laws, and formalization (Doctoral dissertation). University of Barcelona.

@PhDThesis{AlmeidaBorges2023_PhD,
  author = "{de Almeida Borges}, Ana",
  title = "Suitable logics: provability, temporal laws, and formalization",
  school = "University of Barcelona",
  year = "2023",
  url = "https://mat.ub.edu/pop/doctorat/tesis/Thesis\_Ana\_Almeida.pdf",
  keywords = "Modal logic, provability logic, strictly positive logic, quantified modal logic, feasible fragments, monadic second order logic, formal analysis of law, formal verification, Coq",
  abstract = "This thesis explores various aspects of logic, encompassing provability logic, logical analysis of law, and formalization of both mathematics and software. We are particularly interested in the aspect of suitability, both in the sense of finding expressible and tractable fragments of certain logical systems, and in the sense of finding appropriate formal systems for describing certain legal texts. In the domain of provability logic, we introduce two novel calculi: the Worm Calculus (WC) and the Quantified Reflection Calculus with one modality (QRC1). Both WC and QRC1 are inspired by the Reflection Calculus (RC), introduced by Dashkov in 2012. All three logics are strictly positive provability logics, with WC and RC being propositional and polymodal, while QRC1 features a quantified language with a single modality. Worms are words in a numerical alphabet that have many possible readings, particularly as iterated consistency statements. Although the language of worms is very simple, it is remarkably expressive, and known to fully describe the closed fragment of RC. The Worm Calculus is a calculus in the language of worms that illustrates this power: RC is shown to be conservative over WC. Vardanyan showed in 1986 that the quantified provability logic of Peano Arithmetic (QPL(PA)) is Π02-complete, and in particular not recursively axiomatizable. We investigate the strictly positive fragment of QPL(PA), showing that QRC1 is a decidable axiomatization of that fragment. In the process, we prove soundness and completeness of QRC1 with respect to Kripke semantics and two flavors of arithmetical semantics. We also see that QRC1 is the strictly positive fragment of QK4 and of QGL, and of any logic in between those. In the realm of law and inspired by a collaboration with industry, we focus on two European transport regulations, examining certain articles with curious mathematical properties. Then we identify fragments of Monadic Second-order Logic capable of expressing specific segments of one of these regulations, and show how other fragments are less suitable. This effort illustrates some issues with the way the current regulations specify algorithms, and it hints at the role of model checking as a useful legal tool. Lastly, we delve into the formal verification of both mathematics and software using Coq, presenting two case studies. The first case study involves the formalization of modal logical results on QRC1. We describe the overall formalization strategy, focusing on the difficulties and adaptations of both definitions and proofs helpful for the formalization. Due to this process, we were able to identify a small number of improvements to the original proofs. The formalization of software is somewhat different from the formalization of mathematics, although they share many particularities. We use a general framework for software formalization that starts by writing a basic specification for each function, which is then iteratively refined with better algorithms, data structures, and error handling, culminating in extraction to OCaml. Our case study is the formalization of UTC calendars, particularly functions to translate between human-readable times and timestamps, as well as functions to perform time arithmetic. This is a first step towards the formalization of laws that depend on time keeping, of which there are many, including the ones studied here."
}