Journées d'Etude II, 3-4 juin
Preuves, justifications, certificats
***TRANSPARENTS***
Vendredi 3 juin, Institut de Recherche en Informatique de Toulouse (IRIT), Salle des thèses
Session 1, vendredi 3 juin, 9h-10h30, 10h45-12h15, PROVABILITY LOGIC
Lev BEKLEMISHEV (Steklov Mathematical Institute, Russia),
Positive provability logic and reflection calculus: an overview
Several interesting applications of provability logic in proof theory made use of the polymodal logic $\GLP$ due to Giorgi Japaridze. This system, although decidable, is not very easy to handle. In this talk we will advocate the use of a weaker system, called Reflection Calculus, which is much simpler than $\GLP$, yet expressive enough to regain its main proof-theoretic applications, and more. From the point of view of modal logic, $\RC$ can be seen as a fragment of polymodal logic consisting of implications of the form $A\to B$, where $A$ and $B$ are formulas built-up from $\top$ and the variables using just $\land$ and the diamond modalities. We discuss general problems around weak systems of this kind and describe some applications of $\RC$ to the analysis of provability in formal arithmetical theories.
Joost JOOSTEN (Universitat de Barcelona, Spain),
A Calculus of Worms in Coq
In this talk we consider modal provability logics with a series of modalities of length omega that represent a sequence of consistency predicates of increasing strength. The closed fragment of this logic is already quite expressible and constitutes an alternative ordinal notation system up to epsilon_zero. Iterated consistency statements in this closed fragments are also called worms. We present a calculus that manipulates only worms. In particular, the language lacks propositional variables, implications, conjunctions and disjunctions. We compare this Calculus of Worms to the closed fragment of the better known Reflection Calculus. Moreover, we comment on how these worms and their corresponding calculus can be formalized and implemented in Coq.
Joint work with Eduardo Hermo Reyes, Pilar Garcia de la Parra and Alejandro Ramírez Atrio.
Session 2, vendredi 3 juin, 14h15-15h45, 16h-17h30, REALIZABILITY
Fernando FERREIRA (University of Lisbon, Portugal),
Modified realizability and functional interpretations: some logical and mathematical observations
Federico ASCHIERI (Technical University of Vienna, Austria),
From Intuitionistic Realizability to Classical Realizability
Realizability was originally conceived as a constructive semantics for intuitionistic Arithmetic. Since classical Arithmetic looks radically non-constructive, extending realizability to classical fragments of it may appear hopeless. Yet, realizability can be extended to full classical mathematical systems. How is it possible?
The goal of this talk is go through the flow of ideas that lead in a natural way to the many known classical realizabilities. Since realizability appears in disguise under other names such as "validity", "reducibility", "computability", "proof-theoretic semantics", we shall have to look for its origins in unexpected places.
We shall start from Prawitz and Dummett. In Prawitz's work, we find the idea that the introduction rules of natural deduction determine the constructive meaning of logical constants, which leads to realizability based on introduction rules. In Dummett's work, we find the idea that it is the elimination rules of natural deduction that fix the meaning of logical constants, which leads to realizability based on elimination rules.
We shall see that realizability based on introduction rules gives rise to more constructively flavoured semantics, such as realizability for Intuitionistic Arithmetic with Markov's principle, realizability for Intuitionistic Arithmetic with Excluded Middle over formulas with one quantifier and learning based realizability for classical Arithmetic with Skolem choice axioms.
On the other hand, realizability based on elimination rules gives rise to Krivine-style realizability for classical second-order Arithmetic, the only known semantics that can be generalized even to full set theory, but that is also useful for other intermediate logics.
Samedi 4 juin, Institut de Mathématiques de Toulouse (IMT), Amphi Schwartz
Session 3, samedi 4 juin, 9h-10h30, 10h45-12h15, CERTIFICATES
Dale MILLER (Inria Saclay, France),
Defining and checking proof certificates
In order for one theorem prover to export its proofs for other provers to check and trust, proofs-as-documents must be given a clear and precise semantics. After making the case that an infrastructure for sharing proofs should exists, I will describe how recent research in proof theory provides a flexible framework for defining the semantics of proof certificates. I will also briefly describe an implementation that can execute a wide range of such semantic definitions.
Jasmin Christian BLANCHETTE (INRIA Nancy Grand Est, Nancy, France),
Semi-intelligible Isabelle Proofs from Machine-Generated Proofs
Sledgehammer is a component of the Isabelle proof assistant that integrates external automatic theorem provers to discharge proof obligations. As a safeguard against bugs, the proofs found by the external provers are reconstructed in Isabelle. Reconstructing complex arguments involves translating them to Isabelle's Isar format, supplying suitable justifications for each step. Sledgehammer transforms the proofs by contradiction into direct proofs; it iteratively tests and compresses the output, resulting in simpler and faster proofs; and it supports a wide range of automatic provers, including E, LEO-II, Satallax, SPASS, Vampire, veriT, Waldmeister, and Z3.
Joint work with Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier.
Session 4, samedi 4 juin, 14h15-15h45, 16h-17h30, JUSTIFICATION LOGIC
Thomas STUDER (University of Bern, Switzerland), Justification Logic - a short introduction
Traditional modal logics feature formulas of the form K A that stand for 'the agent knows that A'.
The classical semantics for these logics is given by possible world models, in which the formula K A is true if A is true in all worlds that the agent considers possible. However, this approach is missing the justified part of Plato's classic characterization of knowledge as justified true belief. Justification logics can fill this gap. Instead of formulas K A, the language of justification logics includes formulas of the form t : A that mean 'the agent knows that A for reason t'. The evidence term t in this expression can represent a formal proof of A or an informal reason why A is known. Moreover, justification logics include operations on these terms to reflect the agent's reasoning power. For instance, if A -> B is known for reason s and A is known for reason t, then B is known for reason s x t, where the binary operation x models the agent's ability to apply modus ponens.
In our talk, we give a short introduction to justification logic and present some of the main results in this area.
Juan Pablo AGUILERA (Technical University of Vienna, Austria),
An arithmetical interpretation for negative introspection
We introduce verification logic. This variant of Artemov's Logic of Proofs includes proof terms of the form ¡A! that satisfy the axiom schema A -> ¡A!:A. The intention is that terms ¡A! denote a PA-proof of the formula A if it exists. We show that a restriction on the language yields a logic that realizes the axioms of S5 and is sound and complete for its arithmetical interpretation.