• Types, Sets and Constructions
• Workshop: Proofs and Computation

• Schedule
• Participants

In the Hilbertian tradition proofs are finite trees with only axiomatic leaves, but cyclic and ill-founded proofs are an important alternative in applied logic for they can be seen as encoding termination arguments and can be utilised to generate induction invariants, often an intractable problem for traditional proof systems. In this talk I will discuss cyclic proof theory for modal fixed point logic and its application to deriving completeness results.

Recorded Talk 

Aschenbrenner and Pong asked, what is the type (maximum linearization) of the set of lower sets of N^m?  In this talk we'll answer this question and generalize to lower sets (or bounded lower sets) in products of larger ordinals, and ask a related question about weakly decreasing sequences in well partial orders.

Recorded talk

A well-principled notion of epistemic theory as an axiomatic description of a given scenario incorporated into the possible worlds environment is conspicuously absent in epistemic modal logic. We suggest filling this void and introduce a framework of hypertheories and corresponding models for epistemic reasoning with partial information.

Recorded Talk

In this lecture we provide an elementary procedure to eliminate prenex cuts in LJ without v. (For LK without v the elimination of prenex cuts is nonelementary). As corollary we obtain an elementary function F such that cuts in LK with ≤ n quantifiers can be eliminated at the expense of ≤ iterations of F. (This result might seem surprising, as the bound of iterations of F does not depend on the number of implications.)

Recorded talk

We introduce Hyper Natural Deduction as an extension of Gentzen's Natural Deduction system by communication like rules. The motivation is to obtain a natural deduction like system which is equivalent to Avron's Hypersequent Calculus for Goedel-Dummett Logic, and which permits natural conversion rules for normalisation as an extension of the well-known conversion rules for Natural Deduction. The ultimate goal of this project is to establish a Curry-Howard correspondance to some (yet to be found) model of parallel computation. An additional aim is to shed light on Avron's suggestion [in A. Avron: Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence, 4(1991), 225-248] "to contribute towards a better understanding of the notion of logical consequence in general, and especially its possible relations with parallel computations."

This is joint work with Norbert Preining, supported by a Royal Society Daiwa Anglo-Japanese Foundation International Exchanges Award #IE130639.

Recorded talk

Some results about functions which map a natural number $n$ injectively into a smaller natural $m<n$, i.e., which witness a failure of the pigeonhole principle, in a nonstandard model of arithmetic. Joint work with C.T. CHONG, Wei WANG, Tin Lok WONG, and Yue YANG.

We give a combinatorial analysis of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [2002], and show that this analysis can be formalized in the bounded arithmetic system VNC1 (corresponding to "NC1 reasoning''). As a corollary, we prove the assumption made by Jerabek [2011] that a construction of certain bipartite expander graphs can be formalized in VNC1. This in turn implies that every proof in Gentzen's sequent calculus LK of a monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlak [2002].

This is joint work with V. Kabanets, A. Kolokolova, and M. Koucky. 

Recorded talk

A dilator T transforms each well-order X into another well-order T[X], in a particularly uniform way. An order X is called a Bachmann-Howard fixed point of T if there is an almost order preserving function from T[X] into X. In my talk I will explain this notion by means of an example. I will then show how to construct Bachmann-Howard fixed points in general. Finally, I will present the main result of my PhD thesis: The assertion that "every dilator has a well-founded Bachmann-Howard fixed point" is equivalent to ∏₁¹-comprehension.

Recorded talk

Abstract

Updated slides

Recorded talk

Computing with Markov's principle via a realizability interpretation is standard, using unbounded search as in Kleene's realizability or by selecting the first valid witness out of a list of the potential witnesses that a Dialectica interpretation would extract from the proof. Note incidentally that in the first case, the corresponding computational content is justified by Markov's principle itself. Another approach is Friedman's A-translation which justifies Markov's rule by a transformation of proofs. Friedman's A-translation has been extended by Coquand and Hofmann to justify Markov's principle and these translations implicitly provide with a computational content to Markov's principle.

Both Friedman's A-translation and Coquand-Hofmann's translation can be seen as indirect (computational) interpretations of Markov's rule or principle, in the same sense as Kolmogorov-Gentzen-Gödel's double-negation translations can be seen as indirect (computational) interpretations of reasoning by contradiction.

We shall then give a direct-style computational counterpart to Coquand-Hofmann's translation consisting in a proof-as-program-based intuitionistic logic which proves Markov's principle by means of an "exception" programming construct.

Recorded Talk 

We present some reverse mathematics within a constructive set theory in terms of non-deterministic inductive definition (NID) principles. This is a joint work with Ayana Hirata, Tatsuji Kawai and Takako Nemoto.

Recorded talk

Computational interpretations of classical logic are entwined with constructive proofs of Herbrand's Theorem which states, its simplest form, that for every valid existential formula "exists x F(x)" there is a finite set of terms {t₁,...,t_k} such that the quantifier-free disjunction F(t₁) v ... v F(t_k) is a tautology. Such disjunctions can be computed in many ways, including via cut-elimination, interpretations of classical logic in intuitionistic logic and term calculi for classical natural deduction. Each approach endows computational content to classical logic proofs.

In this talk I will outline a language-theoretic representation of Herbrand's Theorem for the classical sequent calculus. Specifically, I will introduce a class of higher order recursion schemes (HORS) that compute Herbrand disjunctions from LK proofs. HORS are a generalisation of regular tree grammars to finite types which equate to the simple-typed λY-calculus with non-deterministic reductions. The representation interprets inference rules of proofs as non-terminals whose production rules operate compositionally to extract the term instantiations that result from reductive cut-elimination. Novel features compared to other approaches are modularity of the translation and that the cut rule is explicitly interpreted as term application.

This is a joint work with Bahareh Afshari (Grothenburg) and Stefan Hetzl (TU Wien).

Recorded Talk 

Tensorial logic is a primitive logic of tensor and negation, which refines linear logic by relaxing the hypothesis that linear negation is involutive. The logic is designed to provide a proof-theoretic and algebraic account of the dialogical interpretation of proofs and programs, and to explore the mechanisms at work in double negation translations. In this introductory talk, I will explain the relationship between tensorial logic, dialogue games and dialogue categories.

If you are curious to know more about that topic
https://www.irif.fr/~mellies/tensorial-logic.html
https://www.irif.fr/~mellies/habilitation.html
https://www.irif.fr/~mellies/hdr-mellies.pdf

Recorded talk

Topological generalizations of possible worlds semantics will be defined and it will be shown how they can be used to build complete proof systems for wide families of modal and conditional logics.Both structural and computational issues will be addressed.

[This is an overview of ongoing research largely based on work in collaboration with Nicola Olivetti, Marianna Girlando, Tiziano Delmonte.]

Recorded talk

Monotone functions abound in the theory of computation, e.g. sorting a string, and detecting cliques in graphs. They have been comprehensively studied in the setting of circuit complexity via negation-free circuits (usually called 'monotone circuits'). The study of 'uniform' monotone computation is a much less developed subject. In this talk we recall the main results of the area concerning the class of positive polynomial-time predicates. Moreover, we describe a function algebra for the class of positive polynomial-time functions (posFP), similar to Cobham's function algebra for the polynomial-time functions, but with a 'uniform' version of recursion. This is joint work with Anupam Das.

Kleene's original notion of realizability (1945) makes use of all (partial) computable functions as potential realisers. Later Kreisel (1959) presented a "modified" notion of realizability based on (total) primitive recursive functionals, in the style of Gödel's Dialectica interpretation. A natural question to ask is whether one can also go to the other way, and have a Dialectica-like version of Kleene's original realizability, which works with all partial computable functions. This has been attemped by Beetson (1978) in a paper entitled "A type-free Gödel interpretation" (JSL). In this talk I'll point out a mistake in Beeson's interpretation, and suggest an alternative solution to this problem.

Recorded talk

(joint work with Sara Negri)

This paper provides the first proof-theoretic study of quantified non-normal modal logics. It introduces labelled sequent calculi for the first order extension, both with free and with classical quantification, of all the monotone non-normal modal logics, as well as of some interesting extensions thereof, and it studies the role of the Barcan Formulas in these calculi. It will be shown that the calculi introduced have good structural properties: they have invertibility of the rules, height-preserving admissibility of weakening and contraction, and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames with either constant or varying domains. In particular the completeness proof constructs a formal proof for derivable sequents and a countermodel for underivable ones, and it gives a semantic proof of the admissibility of cut. Finally, some preliminay results on the extension of our approach to the non-monotonic case are discussed.  

Recorded Talk 

It is well-known that natural axiomatic theories are well-ordered by consistency strength. However, it is possible to construct descending chains of artificial theories with respect to consistency strength. We provide an explanation of this well-orderness phenomenon by studying a coarsening of the consistency strength order, namely the ∏¹₁ reflection strength order. We prove that there are no descending sequences of ∏¹₁ sound extensions of ACA₀ in this order. Accordingly, we can attach a rank in this order, which we call reflection rank, to any ∏¹₁ sound extension of ACA₀. We prove that for any ∏¹₁ sound theory T extending ACA₀⁺ the reflection rank of T equals the proof-theoretic ordinal of T. We also prove that the proof-theoretic ordinal of α iterated  ∏¹₁ reflection is ε_α. Finally, we use our results to provide straightforward well-foundedness proofs of ordinal notation systems based on reflection principles. Based on joint work with James Walsh.

Recorded talk

In this talk we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos.

[1] Erik Palmgren. A constructive examination of a Russell-style ramified type theory. The Bulletin of Symbolic Logic Volume 24, Number 1, March 2018.

Recorded talk

In his seminal paper [1] Myhill developed his formal system CST of sets and functions in order to formalize Bishop's informal system of constructive mathematics developed in [2]. Following Bishop, Myhill considered the natural numbers as a primitive set, and functions as primitive objects that are not sets. He avoided the powerset axiom, using the exponentiation axiom instead, and he included the extensionality axiom for functions and the choice principles used by Bishop. In contrast to Bishop, who considered a defined equality and membership specific to each set, Myhill employed a global notion of equality and a global membership predicate. Moreover, Myhill considered only one notion of function, while Bishop explicitly used also the notion of a family of subsets of a set A indexed by some given set B, and tacitly, the notion of a family of sets indexed by some given set B, a concept defined later by Richman. We present the first steps towards a constructive formal system of set-like and function-like objects in the style of Myhill's CST, aiming at a possible more faithful formalization of Bishop's practice of constructive mathematics. [1] J. Myhill: Constructive Set Theory, J. Symbolic Logic 40, 1975, 347-382 [2] E. Bishop: Foundations of Constructive Analysis, McGraw-Hill, 1967.

Recorded talk

Traditional methods for extracting computational content from proofs typically interpret proofs in some fixed calculus of functionals, such as System T. In this talk I discuss an alternative approach, whereby the computational content of classical proofs is described using a kind of abstract state machine, the purpose being to provide some insight into *algorithms* connected to classical reasoning. This is work in progress.

The talk will present a general machinery for showing derived rules for intuitionistic set theories.

Recorded Talk 

In previous joint work with B. Biering, L. Birkedal, C. Butz, J.M.E. Hyland, J. van Oosten, and T. Streicher, the problem of a semantic presentation of the functional interpretation given by Gödel in his Dialectica paper was addressed. We used the categorical structure of a tripos to address that problem. Triposes were introduced in a seminal paper by M. Hyland, P.T. Johnstone and A.M. Pitts in 1980. In the talk I shall review part of the joint work and suggest how to use appropriate categories to study the Dialectica interpretation. In particular, I shall suggest possible solutions to a question posed by P. Oliva.

Recorded talk

The 19th century saw a systematic (pre-set theory) development of real analysis in which many theorems were proved using compactness. In the work of Dini, Pincherle, and arguably even Bolzano and Lebesgue, one finds such proofs which additionally are highly uniform in the sense that objects proved to exist only dependent on few of the parameters of the theorem. More recently, similarly uniform results have been obtained as part of the redevelopment of analysis based on techniques from gauge interpretation. Our aim is to study such 'highly uniform' theorems, including the intermediate value theorem and Ramsey's theorem, in Reverse Mathematics and computability theory. We will show that these 'highly uniform' theorems defy the traditional hierarchy of logical systems, and even call into question the intuitive notion of "direct versus indirect proof". In particular, we claim that from the classical point of view, 'proof by contradiction' is (often) more effective and makes use of weaker axioms, than traditional/elementary direct proofs. 

Recorded talk

As the intuitionistic logic is included in the classical logic, the class of intuitionistic theories is wider than that of classical theories. Thus the former class admits more methods of model constructions or of interpretations, among which are various kinds of realizability, Kripke-style forcing and double negation translation. We combine these intuitionistic methods in order to obtain interpretability/reducibility results between classical theories. In this talk, the conservation of collection and closure schemata (which are variants of AC and DC, respectively) over several famous classical subsystems of second order arithmetic will be given, with "ultrafinistic" proofs that yield non-speed-up results as well. For these, two variants of realizability, that are not so famous, will be used: van Oosten's Lifschiz-style functional realizability and hyperarithmetical realizability.

Caristi's fixed point theorem is a fixed point theorem for functions that are controlled by continuous functions but are necessarily continuous themselves. Let a 'Caristi system' be a tuple (X,V,f), where X is a complete separable metric space, V is a continuous function from X to the non-negative reals, and f is an arbitrary function from X to X such that for all x in X, d(x,f(x)) ≤ V(x) - V(f(x)). Caristi's fixed point theorem states that if (X,V,f) is a Caristi system, then f has a fixed point. In fact, Caristi's fixed point theorem also holds if V is only lower semi-continuous. in this talk, we explore the strengths of Caristi's fixed point theorem and related statements, such as Ekeland's variational principle, which vary from WKL₀ in certain special cases to beyond Pi¹₁-CA_0.

Recorded talk

Dedekind’s 1887-proof of the Cantor-Bernstein Theorem is based on his chain theory, not on Cantor’s well-ordering principle. A careful analysis of the proof extracts an argument structure that can be seen in the many other proofs that have been given since. I contend, there is essentially one proof that comes in two variants due to Dedekind and Zermelo, respectively. The mathematical analysis of the proofs will be followed by (the description of) their natural formalization using the system AProS as a proof checker. This full formal verification is unusual in two respects: the underlying logical calculus is a bi-directional natural deduction one, and the foundational framework is Zermelo Fraenkel set theory ZF.

Recorded talk

We present a case study of "proof mining'', a program introduced by Kohlenbach, devoted to obtaining quantitative information out of proofs which do not necessarily look constructive. A problem in convex optimization is the convex feasibility problem -- to find common fixed points of a finite family of firmly nonexpansive self-mappings of a convex subset of a Hilbert or CAT(0) space -- and the usual solution is to iterate the composition ("alternating projections'') or a convex combination ("averaged projections'') of the family, taking advantage of the fact that the latter map has as its set of fixed points the set of common fixed points of the family. More generally, even if both sets are empty, this iteration may still be asymptotically regular, a case studies extensively by Bauschke and his collaborators. There is also an "in-between'' case, namely when the common fixed point set is empty but the fixed point set of the auxiliary mapping is not -- therefore the iteration may be useful in order to find e.g. best approximation pairs. In this case, the alternating projections method has been studied (for a family of two mappings) in the context of CAT(0) spaces by Ariza-Ruiz, Lopez-Acedo and Nicolae, and quantitatively analyzed together with Kohlenbach. What we do is to treat the averaged projection method in the same context, from both qualitative and quantitative standpoints (giving weak convergence and asymptotic regularity results), using a trick to reduce it to the other method. The main proof mining contribution is the analysis of this trick, considered as a set inclusion, in the specific case where the two mappings are projections onto closed, convex sets.

Recorded Talk 

A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will present a theory for these computational flows to design a classical direct reading of the Dialectica interpretation. This theory makes a sound and complete interpretation for bounded theories of arithmetic as well as the low complexity statements of strong unbounded systems. We will first use this fact to extract the computational content of the low complexity statements in some bounded theories of arithmetic such as IU_k, T^k_n, IΔ₀(exp) and PRA. And then we will apply the theory on some strong unbounded mathematical theories such as PA and PA+TI(α) using the bridge of continuous cut elimination technique.

Recorded Talk

This talk will consist of two parts. In the first part I explain a convenient formalisation of arithmetic in finite types, with both extensional and intensional models, with all atomic formulas decidable and in which there is a version of equality at higher types for which one has all congruence laws. In the second part I discuss negative translations: the Goedel-Gentzen negative translation has been generalised to arbitrary nuclei. I will explain that one can do the same for the Kuroda negative translation and mention some simple applications.

Recorded talk

A recently discovered notebook of 1928/29 by Gödel shows that his first work in logic consisted in the formalization of proofs in higher-order arithmetic and set theory. In this mini-talk, his proof system is described.

The absorption law for slow provability states that, if it is provable that A is slowly provable, then A is provable. We give a simple proof of the absorption law for a version of slow provability. This version is due to Fedor Pakhomov. We give an application of the result to the study of the provability logic of Heyting Arithmetic.

Recorded talk

We display the entire structure R2 coding Σ₁- and Σ₂- elementarity on the ordinals. This leads to the first steps for analyzing pure Σ₃-elementary substructures.

Recorded talk 

The usual syntactic approach (e.g. to totality or majorizability) does not work for proving continuity of Gödel's System T definable functions (N → N) → N. To make it work, we perform a translation of T terms into T in which natural numbers are translated into functions (N → N) → N. Using a logical relation, we show that every f : (N → N) → N is pointwisely equal to f^b(Ω), where f^b is the translation of f and Ωa is a T-definable generic sequence. By structural induction, we show that the interpretation of any term satisfies a certain continuity predicate, which leads to the desired result of continuity of T-definable functions. Our development has been formalised in the Agda proof assistant and hence can be executed to compute moduli of continuity. By replacing the base case of the above predicate, we can obtain various properties of T definable functions. For instance if we take a predicate B(t) to be the existence of a T-definable bar recursion functional whose termination condition is given by t, then we recover Oliva and Steila's proof of Schwichtenberg's bar recursion closure theorem. More examples will be illustrated during the talk.

Recorded talk