Suitable logics: provability, temporal laws, and formalization

Abstract

[eng] 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 Π0-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.

[spa] Esta tesis en lógica formal abarca la lógica de demostrabilidad, el análisis lógico del derecho, y la formalización de las matemáticas y del software. Se introducen dos nuevos cálculos de demostrabilidad estrictamente positivos inspirados en el Reflection Calculus (RC): el Worm Calculus (WC) y el Quantified Reflection Calculus con una modalidad (QRC1). Tanto RC como WC son lógicas proposicionales y polimodales, mientras que QRC1 tiene un lenguaje cuantificado con una sola modalidad. Los “worms” son palabras en un alfabeto numérico con múltiples interpretaciones, en particular como enunciados de consistencia iterada. El Worm Calculus es un cálculo en el lenguaje de los “worms” que describe la totalidad del fragmento cerrado de RC. Vardanyan demostró que la lógica cuantificada de demostrabilidad de la Aritmética de Peano (QPL(PA)) es Π0-completa y, en particular, no axiomatizable de manera recursiva. Esta tesis investiga el fragmento estrictamente positivo de QPL(PA) y presenta QRC1 como una axiomatización decidible de ese fragmento. Se demuestra la corrección y completitud de QRC1 mediante semántica de Kripke y dos semánticas aritméticas, y que QRC1 es el fragmento estrictamente positivo de las lógicas entre QK4 y QGL, inclusive. Asimismo, la tesis incluye un estudio aplicado al ámbito del derecho en el que se examinan dos regulaciones de transporte europeas con remarcables propiedades matemáticas. Se identifican fragmentos de Lógica Monádica de Segundo Orden capaces de expresar segmentos específicos, y otros menos adecuados, sugiriendo que la verificación de modelos puede ser una herramienta legal útil. Se estudia la verificación formal de matemáticas y software utilizando Coq a través de dos ejemplos. Se describe la formalización de resultados lógicos modales sobre QRC1, abordando los desafíos y adaptaciones en definiciones y pruebas, e identificando mejoras a las pruebas originales. Para la formalización del software se emplea un marco general comenzando con una especificación básica de funciones, refinándola de manera iterativa con mejores algoritmos, estructuras de datos y manejo de errores, culminando con extracción a OCaml. Se formaliza el calendario UTC, incluyendo funciones de traducción entre tiempos y timestamps junto con aritmética del tiempo. Este es un primer paso para la formalización de leyes dependientes del tiempo.