Proof Representations: From Theory to Applications

Formal proofs are an important tool in the mathematical study of computational systems, such as certifying the correctness of an abstract model or verifying that an implementation adheres to a specification. The certification and verification role of proofs boils down to questions of proof existence and proof synthesis: Does a given formula (sequent, judgement, etc.) admit a proof? Can a proof be generated for each provable formula (sequent, etc.)? Both questions rest heavily on a third, often unspoken: what constitutes a proof?

A proof is normally understood as a finite tree with vertices labelled from a class of deduction elements (formulas, sequents, judgements, etc.) where each vertex together with its children match the conclusion and premises of one of a fixed collection of inferences, the decision of which should be complexity-theoretically simple, at worst polynomial-time decidable. This definition is computationally sufficient for many logics such as propositional logic, modal logics, even predicate logic. In each case, soundness and completeness theorems for the corresponding notion of proof confirm that proof existence agrees with semantic validity, and normal form theorems – notably admissibility of cut – give rise to proof synthesis.

Logics and theories incorporating inductive and co-inductive concepts strain the traditional notion of proof, however. Proof existence relies on more complex completeness theorems which coax the infinitary behaviour of the inductive and co-inductive constructions into finitary induction principles. Synthesis likewise suffers, becoming a task in discerning induction invariants from mere provability or elaborating the proof calculus to recover desirable normal forms. The latter is the typical approach of sequent calculi for modal logics where inductive properties – transitivity, factivity, well-foundedness, etc. – are internalised in the inferences rules.

Illfounded proofs offer to alleviate the proof-theorist’s burden not by complicating the notion of proofs but by relaxing it. Proofs are no longer constrained to finite trees; they can be infinite trees, or even graphs, at the cost of infinite branches fulfilling some pre-determined correctness condition. Illfounded proofs provide an alternative to the traditional notion of proof that treats logics and theories of inductive concepts as manifestations of a general infinitary framework rather than diverging extensions of finitary logic. With a change in perspective comes the need to revisit the encompassing theory. Indeed, the inductive construction of formal proof plays a non-trivial role in most – if not all – fundamental results of well-founded proof theory: proof transformations, cut elimination, computational interpretations, syntactic approaches to interpolation and so on.

The talk presented an introduction to the theory and application of illfounded and cyclic proof systems. We focused on two aspects, interpolation and completeness, and saw how results concerning illfounded proofs can be reflected to finitary, inductive, proofs.

Abella is an interactive theorem prover for reasoning about higher-order relational specifications. It is particularly well suited for formalizing the meta-theory of deductive formalisms, including proof systems, type systems, operational semantics, process calculi, etc. One of its key features is the ability to define the inductive structure of data with binding constructs such as quantifiers from logic, abstraction from programming languages, and restriction from process calculi.

This talk gives an overview of the system and presents a main example that can be seen as a challenge problem for formalized meta-theory: showing the equivalence of the higher-order and De Bruijn indexed representations of $\lambda$-terms.

Interactive theorem provers commonly have formal proof languages for expressing formal proofs. Such languages are rarely portable across different systems. I propose an alternative interactive proving interface where textual proof languages have a negligible role. Instead, proofs are built by manipulating the theorem using interaction devices such as mice and touch screens, and interaction mechanisms such as clicking, dragging-and-dropping, etc. The proofs can then be extracted in a variety of existing textual languages. This talk covers intuitionistic first-order logic and discusses some open challenges for this technique, particularly for dependent type theory.

A web-based prototype implementation can be found at: https://chaudhuri.info/research/profint/index-dagstuhl-2024.html.

In this tutorial we explore the proof theory of modal logic. It is well-known that Gentzen-style sequent calculi fail to meet basic requirements in the case of modal logic: for instance, no cut-free sequent calculus is known for the modal logic S5. In order to overcome these difficulties, several extensions of Gentzen’s formalism, which we refer to as “exotic” proof systems, have been studied in the literature. These can be approximately grouped into two categories: labelled calculi, which extend the language of the calculus with explicit semantic information, and structured calculi, among which nested sequents, which instead enrich the structure of sequents. In this tutorial, we will cover the basics of labelled calculi and nested calculi for the S5-cube of modal logics.

We present CEGAR-Tableaux, a tableaux-like method for propositional modal logics utilising SAT-solvers, modal clause-learning and multiple optimisations from modal and description logic tableaux calculi. We use the standard Counter-example Guided Abstract Refinement (CEGAR) strategy for SAT-solvers to mimic a tableau-like search strategy that explores a rooted tree-model with the classical propositional logic part of each Kripke world evaluated using a SAT-solver. Unlike modal SAT-solvers and modal resolution methods, we do not explicitly represent the accessibility relation but track it implicitly via recursion. By using “satisfiability under unit assumptions”, we can iterate rather than “backtrack” over the satisfiable diamonds at the same modal level (context) of the tree model with one SAT-solver. By keeping modal contexts separate from one another, we add further refinements for reflexivity and transitivity which manipulate modal contexts once only. Our solver CEGARBox is, overall, the best for modal logics K, KT and S4 over the standard benchmarks, sometimes by orders of magnitude.

Complex descriptive terms are commonly used in natural languages but its role in conveying information is rather neglected in formal languages. This short talk presents the possible way of constructing well-behaved proof systems for operators enabling the expression of complex terms (like definite descriptions, set-abstracts) in proof systems, like sequent calculi, natural deduction, tableaux systems etc.⁵⁵5This work is sponsored by the ERC advanced grant ERC-2021-ADG, ExtenDD 101054714.

The epsilon calculus, which is the oldest formalism in proof theory, provides important algorithms for proof theoretic properties through its theorems. For example, Herbrand disjunctions of existential formulas can be computed via the extended first epsilon theorem. The proof of the second epsilon theorem provides a direct approach for the elimination of Skolem functions from Herbrand disjunctions of existential formulas. However, the epsilon calculus is not widely used in the literature, and an important reason for this is its complex notation. One way to overcome this problem is to translate the epsilon calculus in a sequent calculus format. In this talk we will present possible translations of the epsilon formalism into a sequent calculus format and discuss their advantages and problems.

Propositional Dynamic logic is a sophisticated modal logic tailored to reason about programs. Several worth-of-studying fragments (controlling the complexity) and extensions (aiming to increase expressiveness) exist. We discuss some impacts of restricting to deterministic programs and how to enhance expressiveness using memory.

The first approach [1] relies on the usage of Guarded Kleene Algebras with Tests (GKAT – [2]) to define Strict Deterministic PDL programs (which will compose GPDL). As GKAT programs can be translated to Thompson’s Automata and have its equivalence determined in almost linear time, the proposed algorithm is used to show that in GPDL $\vDash ⟨\pi ⟩p\leftrightarrow ⟨\eta ⟩p\iff \pi =\eta$.

A second approach consists on increasing the expressiveness by adding a memory to PDL [3]. Diferently from typical Memory Logics, the memory is in the syntax and not only in the model. We show that it is possible to reason about some context-sensitive languages and, for bounded memory, present a [factorial] translation to standard PDL.

Information and opinions come to us daily from a wide range of actors, including scientists, journalists, and pundits. Some actors may be biased or malicious, while others rely on physical measurements, statistics, or in-depth research. Some sources may be signed or edited, while others are anonymous and unmoderated. Trusting information from such diverse sources is a serious challenge facing society today. In this paper, we will describe another domain – the world of machine-checked logic and mathematics – in which many similar issues can appear but in which tractable solutions are possible. Many actors (people or software systems) assert that certain logical statements are theorems in this domain. We describe the Distributed Assertion Management Framework (DAMF) that explicitly manages claims by theorem provers that they have proved certain theorems from associated contexts. Provers willing to trust other provers will be able to avoid rechecking proofs.

The expressive capabilities of first-order logic are significantly expanded by second-order logic, which allows quantification over sets and properties. This extension addresses the natural demand in mathematics of expressing properties that involve quantification over all subsets or families of subsets of a given structure. Despite these advantages, full second-order logic lacks essential metalogical properties due to its impredicativity, which presents challenges in the development of proof systems. Our study tackles these challenges by introducing a G3-style calculus that admits the predicative comprehension schema, enabling a constructive cut elimination proof.

The calculi are extended to explore the proof theory of mathematical theories, with methods from first-order calculi being adapted, and structural results being established for both classical and intuitionistic calculi. Additionally, extensional equality and apartness are defined in second-order logic, showcasing the reduction of mathematical notions to pure logic. As an example, the theory of predicative second-order arithmetic is presented, and a variant of Herbrand’s theorem tailored for predicative second-order intuitionistic logic is established, leading to the conservativity of predicative second-order Heyting arithmetic over its first-order counterpart. Furthermore, the interpolation theorem and the modal embedding of intuitionistic logic are extended to predicative second-order logic.

In this talk, we demonstrate how inductive properties of propositional sequent systems can be automatically proved using the rewriting logic framework and its implementation in Maude. The properties of interest include the admissibility of weakening and contraction, rule invertibility, cut-admissibility, and identity expansion. We present examples of the L-Framework tool (https://carlosolarte.github.io/L-framework/) applied to various logical systems, including single-conclusion and multi-conclusion intuitionistic logic, classical logic, classical linear logic (and its dyadic system), intuitionistic linear logic, and normal modal logics.

We demonstrate how to use proof-theoretic methods, specifically for a series of philosophically motivated deontic logics, to show that the principle of not deriving an “ought” from an “is” holds.

In this talk, I ask about the limitations on various types of deductive systems for logics featuring numerical quantification. By “numerical quantification” I understand the use of constructions such as “There exist at most/at least/exactly $n$ $x$ such that …”, where $n$ is a natural number. It is known that many familiar fragments of first-order logic for which satisfiability is decidable can be extended with numerical quantification without losing decidability of satisfiability. At issue in this talk is what the decision methods in question have to look like. I begin with a negative result concerning the extension of the Aristotelian syllogistic with numerical quantification: I show that there exist no sound and complete collections of Aristotelian-like syllogisms for such logics. I then switch to the extension of the two-variable fragment of first-order logic with numerical quantification: I present a high-level account of decision procedures for this logic based on reduction to integer linear programming. Finally, I turn my attention to the one-variable fragment of first-order logic extended with numerical quantification: I ask whether there is a numerical extension of propositional resolution which is sound and complete for this logic.

A simple criterion for the validity of an abstract Glivenko master theorem facilitates to instantiate the latter not only in conventional contexts such as Kuroda’s but always when an axiom, e.g. stability, is added to a basic provability relation.

In this short talk I will discuss the problem of proof identity and explain how it is related to Hilbert’s 24${}^{\text{th}}$ problem. I will also argue that not knowing when two proofs are “the same” has embarrassing consequences not only for proof theory but also for certain areas of computer science where formal proofs play a fundamental role, in particular the formal verification of software.

The talk contains material from a programmatic paper written in the context of an ERC grant, ERC-2020-ADG, ConLog, Contradictory Logics: A Radical Challenge to Logical Orthodoxy, H. Wansing, Beyond paraconsistency. A plea for a radical breach with the Aristotelean orthodoxy in logic, in: Walter Carnielli on Reasoning, Paraconsistency, and Probability, A. Rodrigues, H. Antunes, and A. Freire (eds), 2022, Springer, to appear 2024, and some comments on Gentzen-style proof systems for a certain non-trivial negation inconsistent logic.

After some terminological preliminaries on the notions of contradiction, inconsistency, and negation, I will make comments on paraconsistency, classical logic, and consistency. Then I will go beyond paraconsistency and will present a list of non-trivial negation inconsistent logics. Finally, I will introduce the non-trivial negation inconsistent connexive logic C and bilateral proof systems for C.

The references below may be considered selected references on this topic.

The epsilon operator [1, 3] is mainly studied in the context of classical logic. It is a term forming operator: if $A(x)$ is a formula, then $\epsilon xA(x)$ is a term – intuitively, a witness for $A(x)$ if one exists, but arbitrary otherwise. Its dual $\tau xA(x)$ is a counterexample to $A(x)$ if one exists. Classically, it can be defined as $\epsilon x\neg A(x)$. Epsilon and tau terms allow the classical quantifiers to be defined: $\exists xA(x)$ as $A(\epsilon xA(x))$ and $\forall xA(x)$ as $A(\tau xA(x))$.

Epsilon operators are closely related to Skolem functions, and the fundamental so-called epsilon theorems to Herbrand’s theorem. Recent work with Matthias Baaz [2] investigates the proof theory of $\epsilon \tau$-calculi in superintuitionistic logics. In contrast to the classical $\epsilon$-calculus, the addition of $\epsilon$- and $\tau$-operators to intuitionistic and intermediate logics is not conservative, and the epsilon theorems hold only in special cases. However, it is conservative as far as the propositional fragment is concerned.

Despite these results, the proof theory and semantics of $\epsilon \tau$-systems on the basis of non-classical logics remains underexplored.

Universal Proof Theory is a recent research program that aims to study the mathematical properties of proof systems in a generic manner (analogous to the generic study of algebras in Universal Algebra). The term Universal Proof Theory was first introduced in preprint [1]. The program consists of three fundamental problems: (1) the existence problem to investigate the existence of certain kinds of proof systems for a given logic, (2) the equivalence problem to study the natural notions of equivalence of proof systems, and (3) the characterization problem to investigate the possible characterizations of proof systems. In the session, we provide an overview of the results which are mainly achieved for the existence problem (i.e., [3, 1, 4, 5, 2]). We discuss a small unsolved problem to provide a flavor of what this research involves. We invite the audience to connect their work to this program so that we create a better understanding of Universal Proof Theory within the broader community of Proof Theory.

Special session held on 22nd August 2024
Contributors: Anupam DAS, Abhishek DE & Alexis SAURIN

Non-wellfounded proofs and their regular fragment – cyclic, or circular proofs – appear in a very natural way when studying inductive and coinductive reasoning [5, 8, 12, 13] (such as in variants of the $\mu$-calculus, or in logics with inductively-defined predicates). While the complex inference rules for induction and coinduction are replaced by simpler fixed-point unfolding rules, the existence of infinite branches in proof trees requires that a global condition is imposed on derivations in order to ensure soundness and to allow a structured proof-theoretical analysis as shown below:

The special session presented some complements on Bahareh Afshari’s invited talk along the following lines and with a specific focus on the Curry-Howard correspondence between proofs and programs.

• $\mathrm{■}$

  Abhishek De presented the logical frameworks under study as well as the thread progress-condition for non-wellfounded and regular proofs (illustrated below, with $F=\nu X.(a\vee \overline{a})\wedge (X\wedge \mu Y.X)$) and discussed its decidability and complexity. He also explained how the condition ensures the soundness of the proof system [5, 7, 8, 12].

• $\mathrm{■}$

  Anupam Das compared finitary (co)induction inference rules [1, 5] and the provability in cyclic proofs [5, 8]: he showed that, under a very general condition, circular proofs subsume finitary induction and coinduction [8] (see figure below) and reviewed the literature studying the converse property [3, 4, 8, 11].

• $\mathrm{■}$

  Finally, Alexis Saurin reviewed cut-elimination theorems for those proof systems [2, 8, 9, 10] including non-wellfounded derivations and the challenge raised by the non-wellfounded proof trees. On the way, he showed, on some examples, how inductive and coinductive data can be represented as non-wellfounded and circular proofs [6, 8].