Workshop II, 3-4th June

Proofs, justifications, certificates



Friday 3 June, Institut de Recherche en Informatique de Toulouse (IRIT), Salle des thèses

Session 1, Friday 3 June, 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 June, 14h15-15h45, 16h-17h30, REALIZABILITY

Fernando FERREIRA (University of Lisbon, Portugal), Modified realizability and functional interpretations: some logical and mathematical observations

We review some basic and well-known facts about the possibility of extracting computational information from proofs in classical, intuitionistic and semi-intuitionistic systems. Intuitionistic reasoning is tailored to have a clear constructive content and Kleene’s (numerical) realizability was a way of establishing precisely what this means for intuitionistic proofs in arithmetic. We review the variant of modified realizability due to Kreisel and see it as a form of a functional interpretation. An emphasis throughout is on the fact that there are some semi-intuitionistic principles which are amenable for computational extraction. Even Kreisel’s modified realizability displays not only the constructive content of intuitionistic logic but goes a bit further since it also realizes a certain (non-intuitionistic) principle of independence of premises. This principle is a characteristic principle of modified realizability. We explain what are these characteristic principles and compare them with so-called side principles, which are also amenable for computational extraction.
Markov’s principle is a characteristic principle of Gödel’s functional dialectica interpretation. We review the dialectica interpretation and also analyze Markov’s principle via the so-called Friedman’s trick. We make a short comparison between both treatments of Markov’s principle. We introduce a new interpretation (the C-interpretation) and see that LLPO (the lesser limited principle of omniscience) is one of its characteristic principles. The extraction of computational information now takes the form of bounds, not of precise witnesses. We discuss this issue and a monotonicity condition now so central in several recently defined functional interpretations. Finally, we extend the C-interpretation to the second-order arithmetical setting in such a way that WKL (weak König’s lemma) turns out to be a characteristic principle.

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.


Saturday 4 June, Institut de Mathématiques de Toulouse (IMT), Amphi Schwartz

Session 3, Saturday 4 June, 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, Saturday 4 June, 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.

Organisation scientifique: David FERNANDEZ DUQUE, Andreas HERZIG, Ralph MATTHES, Martin STRECKER