Proof Society Seminar

Date: 28/04/2025
Speaker: Stepan Kuznetsov (Steklov Mathematical Institute of RAS)
Title:  Circular and infinitary proofs for complexity analysis of action logic
Abstract:  Action logic is the extension of the full Lambek calculus (intuitionistic-style non-commutative substructural logic) with the operation of Kleene iteration. The natural algebraic semantics for action logic is given by residuated Kleene lattices (RKLs). Action logic appears in two variants: the logic of all RKLs (action logic itself), with an inductive axiomatisation for iteration, and a stronger infinitary system, where iteration is governed by an omega-rule. The latter corresponds to the natural subclass of *-continuous RKLs. In this talk, we discuss how calculi with circular and infinitary proofs help analyse algorithmic complexity for theoremhood and entailment from hypotheses in action logic and its infinitary extension. Namely, using circular proofs we show \Sigma^0_1-completeness of action logic. The theoremhood problem in infinitary action logic is \Pi^0_1-complete. For entailment from *-free hypotheses in the latter, we get an \omega^\omega upper bound on the closure ordinal (for the system with an omega-rule) and the corresponding hyperarithmetical complexity bound, which is actually exact. Finally, entailment from arbitrary hypotheses in infinitary action logic is \Pi^1_1-complete, the closure ordinal being \omega_1^{CK}.

Partially based on joint work with Tikhon Pshenitsyn and Stanislav Speranski.

Date: 03/03/2025
Speaker: Henry Towsner (University of Pennsylvania)
Title: Proofs that Modify Proofs
Abstract:  In this talk, we outline an approach to cut-elimination for full second order arithmetic using a modified form of the Buchholz Omega-rule. The usual Buchholz Omega-rule is a rule branching over (“small”) deductions; this method works for systems around the strength of Pi11-comprehension, but breaks down approaching Pi12-comprehension.
We describe an extended sequent calculus in which the cut-elimination functions can themselves be represented by non-well-founded deductions. The Omega-rule can then be reinterpreted as a rule which takes a function as a premise. The extension to Pi12-comprehension then requires us to work with functionals—that is, functions on functions—and iterating through the finite types extends the method to full second order arithmetic. We will also briefly describe how to assign “ordinals” to non-well-founded deductions to extract an ordinal analysis from the cut-elimination algorithm.

Date: 03/02/2025
Speaker: Jeremy Avigad (Carnegie Mellon University)
Title: Verifying Proofs on Blockchain
Abstract: In cryptography, a *proof system* is a protocol between a prover and a verifier that enables the prover to convince the verifier that a claim is true. They are often probabilistic; given a source of randomness, it is often more efficient to convince the verifier only that it is very likely that the claim is true. Such proof systems now have interesting applications to blockchain technology, where they are used, among other things, to validate the execution of smart contracts. It is easy to make mistakes when implementing cryptographic protocols and designing smart contracts, and billions of dollars are lost to hacks every year. Fortunately, another proof technology can help: interactive proof assistants, which have long been used to verify hardware and software systems, can also be used to verify the correctness of cryptographic protocols. In this talk, I will describe some formal verification efforts I have carried out with colleagues at StarkWare Industries using the Lean proof assistant.. I will explain some of the ideas behind smart contracts and interactive proof assistants without assuming familiarity with either.
Slides and Recording