Schedule of the Workshop "Proofs and Computation"

Monday, July 2

 10:15 - 10:50 Registration & Welcome coffee 10:50 - 11:00 Opening remarks 11:00 - 11:30 Paul Shafer: Reverse mathematics of Caristi's fixed point theorem and Ekeland's variational principle 11:30 - 12:00 Paulo Oliva: On a Dialectica-like version of Kleene numerical realizability 12:00 - 14:00 Lunch break 14:00 - 14:30 Sam Sanders (joint with Dag Normann): Uniformity in mathematics 14:30 - 15:00 Albert Visser: The absorption law for slow provability 15:00 - 15:30 Break 15:30 - 16:00 Matthias Baaz: Fast cut-elimination in intuitionistic logic 16:00 - 16:30 Tea and cake 16:30 - 17:00 Kentaro Sato: Making a detour via intuitionistic theories: Applications to SOSOA 17:00 - 17:30 Fedor Pakhomov: Reflection ranks and ordinal analysis 17:30 - 17:45 Break 17:45 - 18:15 Graham Leigh: On the computational content of classical sequent calculus afterwards Reception

Tuesday, July 3

 09:30 - 10:00 Anton Freund: Bachmann-Howard Fixed Points 10:00 - 10:30 Gunnar Wilken: Pure Sigma_2-Elementarity beyond the Core 10:30 - 11:00 Group photo and coffee break 11:00 - 11:30 Andrei Sipos: Quantitative results on the method of averaged projections 11:30 - 12:00 Harry Altman: Lower sets in products of well-ordered sets 12:00 - 14:00 Lunch break 14:00 - 14:30 Sergei Artemov: Hyperderivations 14:30 - 15:00 Amir Tabatabai: Mining the Surface: Proof mining in the bounded world 15:00 - 15:30 Break 15:30 - 16:00 Lew Gordeev: Predicative proof theory of PDL 16:00 - 16:30 Tea and cake 16:30 - 17:00 Chuangjie Xu: A syntactic approach to continuity and ...

Wednesday, July 4

 09:30 - 10:00 Iosif Petrakis: Myhill's system CST revisited 10:00 - 10:30 Bahareh Afshari: Cyclic Modal Proofs 10:30 - 11:00 Group photo and coffee break 11:00 - 11:30 Arnold Beckmann: Hyper Natural Deduction 11:30 - 12:00 Silvia Steila: An overview over least fixed points in weak set theories 12:00 - 14:00 Lunch break 14:00 - 14:30 Wilfried Sieg: The Cantor-Bernstein Theorem: How many proofs? 14:30 - 15:00 Sara Negri: Topological generalizations of possible worlds semantics and their proof systems 15:00 - 15:30 Break 15:30 - 16:00 Lars Kristiansen: First-order concatenation theory vs. first-order number theory 16:00 - 16:30 Tea and cake 16:30 - 17:00 Anton Setzer: The extended predicative Mahlo Universe and the need for partial proofs and partial objects in type theory 19:00 - Conference Dinner

Thursday, July 5

 09:30 - 10:00 Sam Buss: Expanders in VNC^1 and Monotone Propositional Proofs 10:00 - 10:30 Hugo Herbelin: Computing with Markov's principle 10:30 - 11:00 Coffee break 11:00 - 11:30 Paul-Andre Mellies: An introduction to tensorial logic and dialogue categories 11:30 - 12:00 Eugenio Orlandelli: Proof theory for quantified monotone modal logics 12:00 - 14:00 Lunch break 14:00 - 14:30 Thomas Powell: Ideal objects and abstract machines 14:30 - 15:00 Giuseppe Rosolini: Triposes and Gödel's Dialectica Interpretation 15:00 - 15:30 Break 15:30 - 16:00 Jan von Plato: Gödel's proof system for higher-order arithmetic 16:00 - 16:30 Tea and cake 16:30 - 17:00 David Belanger: Randomness and the weak pigeonhole principle

Friday, July 6

 09:30 - 10:00 Isabel Maria Oitavem: The positive polynomial-time functions 10:00 - 10:30 Hajime Ishihara: Reverse mathematics of non-deterministic inductive definitions 10:30 - 11:00 Coffee break 11:00 - 11:30 Benno van den Berg: Two observations on intuitionistic logic and arithmetic 11:30 - 12:00 Erik Palmgren: A constructive examination of a Russell-style ramified type theory 12:00 - 12:15 Break 12:15 - 12:45 Michael Rathjen: Derived rules in set theory

Abstracts

Bahareh Afshari: Cyclic Modal Proofs

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

Top

Harry Altman: Lower sets in products of well-ordered sets

Aschenbrenner and Pong asked, what is the type (maximum linearization) of the set of lower sets of Nm?  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

Top

Sergei Artemov: Hyperderivations

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

Top

Matthias Baaz: Fast cut-elimination in intuitionistic logic

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

Top

Arnold Beckmann: Hyper Natural Deduction

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

Top

David Belanger: Randomness and the weak pigeonhole principle

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.

Top

Sam Buss: Expanders in VNC^1 and Monotone Propositional Proofs

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

Top

Anton Freund: Bachmann-Howard Fixed Points

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 ∏11-comprehension.

Recorded talk

Top

Recorded talk

Top

Hugo Herbelin: Computing with Markov's principle

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

Top

Hajime Ishihara: Reverse mathematics of non-deterministic inductive definitions

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

Top

Lars Kristiansen: First-order concatenation theory vs. first-order number theory

First-order concatenation theory can be compared to first-order number theory, e.g., Peano Arithmetic or Robinson Arithmetic. The universe of a standard structure for first-order number theory is the set of natural numbers. The universe of a standard structure for first-order concatenation theory is a set of strings over some alphabet. A first-order language for number theory normally contains two binary functions symbols. In a standard structure these symbols will be interpreted as addition and multiplication. A first-order language for concatenation theory normally contains just one binary function symbol. In a standard structure this symbol will be interpreted as the operator that concatenates two stings. A classical first-order language for concatenation theory contains no other non-logical symbols apart from constant symbols. We will discuss first-similarities and differences between first-order concatenation theory and first-order number theory. Furthermore, we will extend concatenation theory with a binary relation symbol and introduce bounded quantifiersanalogous to the bounded quantifiers (∀x≤t)φ and (∃x≤t)φ we know from number theory, and discuss the results published in [1, 2]

Recorded Talk

References

1. Kristiansen, L. and Murwanashyaka, J.: Notes on Fragments of First-Order Concatenation Theory. arXiv.org. ISSN 2331-8422.

2. Kristiansen, L. and Murwanashyaka, J.: Decidable and Undecidable Fragments of First-Order Concatenation Theory. CiE 2018 - Sailing Routes in the World of Computation, Springer LNCS ????, pp. ??-??, Springer-Verlag 2018.

Top

Graham Leigh: On the computational content of classical sequent calculus

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 {t1,...,tk} such that the quantifier-free disjunction F(t1) v ... v F(tk) 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

Top

Paul-Andre Mellies: An introduction to tensorial logic and dialogue categories

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

Top

Sara Negri: Topological generalizations of possible worlds semantics and their proof systems

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

Top

Isabel Maria Oitavem: The positive polynomial-time functions

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.

Top

Paulo Oliva: On a Dialectica-like version of Kleene numerical realizability

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

Top

Eugenio Orlandelli: Proof theory for quantified monotone modal logics

(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

Top

Fedor Pakhomov: Reflection ranks and ordinal analysis

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 ∏11 reflection strength order. We prove that there are no descending sequences of ∏11 sound extensions of ACA0 in this order. Accordingly, we can attach a rank in this order, which we call reflection rank, to any ∏11 sound extension of ACA0. We prove that for any ∏11 sound theory T extending ACA0+ the reflection rank of T equals the proof-theoretic ordinal of T. We also prove that the proof-theoretic ordinal of α iterated  ∏11 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

Top

Erik Palmgren: A constructive examination of a Russell-style ramified type theory

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

Top

Iosif Petrakis: Myhill's system CST revisited

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

Top

Thomas Powell: Ideal objects and abstract machines

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.

Top

Michael Rathjen: Derived rules in set theory

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

Recorded Talk

Top

Giuseppe Rosolini: Triposes and Gödel's Dialectica Interpretation

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

Top

Sam Sanders (joint with Dag Normann): Uniformity in mathematics

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

Top

Kentaro Sato: Making a detour via intuitionistic theories: Applications to SOSOA

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.

Top

Anton Setzer: The extended predicative Mahlo Universe and the need for partial proofs and partial objects in type theory

(Joint work with Reinhard Kahle, Lisbon)

The Mahlo Universe in Martin-Löf Type Theory has an introduction rule which refers to all total functions from families of sets of the Mahlo universe into itself.This makes it an impredicative definition. Although it can be justified by the fact that no elimination rules are added, a more predicative justification is desirable.

We have defined the extended predicative Mahlo universe in the area of Explicit Mathematics in which we weaken the requirement for adding a subuniverse: instead of demanding closure of the Mahlo universe, all we need is that the subuniverse is closed under a given function. For this to work we need access to the collection of all partial functions, which is not available in type theory.

As a consequence, in this system partial functions are necessary, which will then as well be part of proof objects, so we obtain partial proofs. We will discuss steps towards developing a new type theory in which one has access to the collection of all partial functions.

Recorded Talk

Top

Paul Shafer: Reverse mathematics of Caristi's fixed point theorem and Ekeland's variational principle

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 WKL0 in certain special cases to beyond Pi11-CA0.

Recorded talk

Top

Wilfried Sieg: The Cantor-Bernstein Theorem: How many proofs?

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

Top

Andrei Sipos: Quantitative results on the method of averaged projections

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

Top

Silvia Steila: An overview over least fixed points in weak set theories

(joint work with Gerhard Jäger)

Given a monotone function on a complete lattice the least fixed point is defined as the minimum among the fixed points. Tarski Knaster Theorem states that every monotone function on a complete lattice has a least fixed point.

There are two standard proofs of Tarski Knaster Theorem. The first one exploits the fact that given a monotone function F on a complete lattice “the least fixed point is the intersection of all sets which are closed under F”. Where a set is closed under F if F(z) is below z with respect to the lattice order.  The second one is based instead on the inductive definition by stages. If we define Iα = F(∪{β<α}Iβ),  then there exists an ordinal alpha  such that z = Iα  and F(Iα)=Iα

Over ZFC the powerset of the natural numbers (P(Ω) is not only a set but also a complete lattice, and Tarski Knaster Theorem holds for it. If we move to weaker set theories (e.g., extensions of Kripke Platek Set Theory (KP)) in which we avoid in particular the powerset axiom, Tarski Knaster Theorem for P(Ω) might turn out to be unprovable.

In this talk we focus on the differences between these two standard constructions of the least fixed point over a conservative second order extension of KP.

Recorded talk

Top

Amir Tabatabai: Mining the Surface: Proof mining in the bounded world

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 IUk, Tkn, IΔ0(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

Top

Benno van den Berg: Two observations on intuitionistic logic and arithmetic

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

Top

Jan von Plato: Gödel's proof system for higher-order arithmetic

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.

Top

Albert Visser: The absorption law for slow provability

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

Top

Gunnar Wilken: Pure Sigma_2-Elementarity beyond the Core

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

Recorded talk

Top

Chuangjie Xu: A syntactic approach to continuity and ...

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 fb(Ω), where fb 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

Top