Schedule for: 21w5156 - New Frontiers in Proofs and Computation (Online)

Halpern’s iteration method, invented by Benjamin Halpern in 1967, is a fixed point algorithm for finding fixed points of a nonexpansive mapping. Since many optimization problems can be cast as fixed point problems of nonexpansive mappings, Halpern’s method plays an important role in optimization methods. We will talk about some recent progresses on convergence and rate of convergence results of Halpern’s method and its various applications in optimization problems, including variational inequalities, monotone inclusions, Douglas-Rachford splitting method, and minimax problems.

In this talk I will present some recent results on the application of proof theoretic methods in functional analysis, which focus on producing rates of convergence for algorithms that compute fixpoints for a special class of contractive mappings. I will outline the common structure of convergence proofs for these mappings and explain how proof theory allows us to not only extract quantitative information from these proofs, but also unify and generalise them. This talk will not assume any background in either proof theory or functional analysis but will instead aim to provide a high-level illustration of some of the core ideas that are relevant to applied proof theory in general.

Let $T$ be an infinite perfect tree. The principle $TT^1$ states that every coloring of $T$ with finitely many colors has an isomorphic homogeneous subtree $U$ , i.e. where all the nodes have the same color. In this talk we discuss the first-order strength of this principle over the base system $RCA_0$ and those of its generalisations.

We investigate the strength of three principles between weak Konigs lemma ($WKL$: Every infinite binary tree has a path) and weak weak Konigs lemma ($WWKL$: Every positive measure binary tree has a path) on the basis of computable second order arithmetic ($RCA$): P+: Every positive measure tree has a positive measure perfect subtree； P: Every positive measure tree has a perfect subtree； P?: Every positive measure tree has an infinite countable family of paths. Under recursive comprehension with one-quantifier induction: $WKL$ implies P+ implies P implies P? implies $WWKL$. We show that these implications are strict, except possibly for "P implies P?" which we leave open. The separations are obtained by the construction of suitable omega models, some generated by random reals and some by generics. These constructions are largely a mix of measure and category methods, and involve concepts from the theory of random closed sets and Poisson point processes. Corollaries include the following facts, which are of independent interest: (a) an algorithmically random real computes a pathwise-random tree with infinitely many paths if and only if it computes the halting problem; it follows that the class of pathwise-random trees with unbounded width is null, with respect to any computable measure; (b) there exists a positive-measure pathwise-random tree which does not compute any complete extension of Peano arithmetic; (c) there exists a perfect pathwise-random tree which does not compute any positive pathwise-random tree. This is a joint work with Wei Wang. Our paper is available at: http://arxiv.org/abs/2104.12066

Functional interpretations of semi-intuitionistic and classical finite-type theories based on Goedel's work rely, at their root, on the accumulation into finite sets of possible witnesses of certain existential claims, of which at least one is an actual witness. Bounded interpretations, on the other hand, rely on the accumulation of witnesses below a certain bound. The latter interpretations enjoy some extra features. For instance, they interpret principles like weak Koenig's lemma or, in the case of semi-intuitionism, the FAN principle. However, when one restricts the analyses to second-order theories, accumulation into finite sets is also able to interpret these extra principles. We discuss these matters and compare the two kinds of interpretations.

I provide an overview of my joint project with Dag Normann on the Reverse Mathematics and computability theory of the uncountable ([2-7]). In particular, we have shown that the following theorems are hard to prove relative to the usual scale of (higher-order) comprehension axioms, while the objects claimed to exist by these theorems are similarly hard to compute, in the sense of Kleene's S1-S9 schemes ([1]). 1. There is no injection from R to N (Cantor 1874). 2. Arzela's convergence theorem for the Riemann integral (1885). 3. A Riemann integrable function is not everywhere discontinuous (Hankel, 1870). 4. Jordan's decomposition theorem. 5. A function of bounded variation on the unit interval has a point of continuity. 6. A lower semi-continuous function on the unit interval attains its minimum. 7. The Bolzano-Weierstrass theorem for countable sets (injections/bijections to N) We show that the nal item gives rise to many robust equivalences, which in turn yields the `Big Six' and `Big Seven' system of Kohlenbach's higher-order Reverse Mathematics. We discuss how comprehension is unsuitable as a measure of logical and computational strength in this context; we also provide an alternative, namely a (classically valid) continuity axiom from Brouwer's intuitionistic mathematics. In turn, this yields a framework that marries the `best of both worlds' of the Turing and Kleene approach to computability theory. Finally, our study shows that coding practise common in e.g. Reverse Mathematics and Weihrauch reducibility can significantly change the logical and computational strength of basic theorems pertaining to functions of bounded variation and other "close to full continuity" notions. REFERENCES: [1] John Longley and Dag Normann, Higher-order Computability, Theory and Applications of Computability, Springer, 2015. [2] Dag Normann and Sam Sanders, On the mathematical and foundational signicance of the uncountable, Journal of Mathematical Logic, https://doi.org/10.1142/S0219061319500016 (2018). [3] , Open sets in Reverse Mathematics and Computability Theory, To appear in Journal of Logic and Computability, arXiv: https://arxiv.org/abs/1910.02489 (2020). [4] , Pincherle's theorem in Reverse Mathematics and computability theory, Annals of Pure and Applied Logic, doi: 10.1016/j.apal.2020.102788 (2020). [5] , On the uncountability of R, Submitted, arxiv: https://arxiv.org/abs/2007.07560 (2020), pp. 37. [6] , The Axiom of Choice in Computability Theory and Reverse Mathematics, Journal of Logic and Computation 31 (2021), no. 1, 297-325. [7] , On robust theorems due to Bolzano, Weierstrass, and Cantor in Reverse Mathematics, See https://arxiv.org/abs/2102.04787 (2021), pp. 30.

Timothy Carlson's patterns of resemblance provide an astonishingly simple way to describe large computable ordinals. In particular, Gunnar Wilken has establish connections with collapsing functions and hence (amongst others) with the Bachmann-Howard ordinal. The present talk explores a more abstract version of this connection, where both patterns and collapsing functions are relativized to dilators. Our more abstract setting has two advantages: First, it allows us to capture the elegant mathematical ideas behind ordinal notation systems, without considering syntactic details. Indeed, the talk will aim to present these ideas without prerequisites from ordinal analysis. Secondly, we can investigate connections with other abstract principles, such as the set existence axioms from reverse mathematics. Specifically, we will obtain an equivalence between $\Pi^1_1$-comprehension and a statement about patterns of resemblance, which proves a conjecture from Antonio Montalban's list of `Open Questions in Reverse Mathematics' (BSL 17(3)2011). A preprint with full details is available as arXiv:2012.10292.

The $\Pi^1_2$-norm $|T|$ associated to a theory $T$ is a functor on the category Ord which captures the strength of the $\Pi^1_2$ consequences of $T$. It is always defined for $\Pi^1_2$-sound extensions of $ACA_0$. Attempts to extend the definition to theories which are not $\Pi^1_2$-sound lead to the notion of the $\Pi^1_2$ ordinal $o(T)$ of a theory. $o(T)$ is a measure of how close T is to being $\Pi^1_2$-sound. In this talk, we give more detailed definitions of these concepts and give a characterization of the admissible ordinals which are of the form $o(T)$ for some recursively enumerable extension of $ACA_0$. This is joint work with Fedor Pakhomov.

This talk presents a joint work with Juan Pablo Aguilera. Dilators are certain kind of well-behaving operators on well-orders that were introduced by Girard. There are several known results about the dilators connected to $ACA_0$, most well-known of which is the result Girard's result that $ACA_0$ is equivalent to the assertion that $X↦ω^X$ is a dilator. There is a well-studied notion of embeddings of dilators. We give a characterization of provable dilators of $ACA_0$ in terms of embeddability. Let $ε^+$ be the naturally defined dilator mapping a well-order X to the smallest $ε$-number strictly greater than the order type of X. We prove that $ε^+$ is the embeddability least dilator F such that for each recursive dilator D, if $ACA_0$-proves that D is a dilator, then D is embeddable into F. This result constitute the first to our knowledge characterization of provable dilators of any formal system in terms of embeddability. This proof required to develop new technical machinery, which will be discussed in this talk.

In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders.

This talk will consist of two parts. In Part I, l'll briefly introduce dependent/modern type theories, as studied by Martin-Loef and others [5,2,3], their meta-theoretic studies, and their applications such as those supported by proof assistants. Then, in Part II, l'll focus on one of the applications, giving an overview of Formal Semantics in Modern Type Theories (MTT-semantics) [7,4]. MTT-semantics is a semantic framework for natural language and, thanks to its recent development [1], it has become not only a full-blown alternative to Montague's semantics [6], but also an attractive framework with a promising future for formal semantics. References. [1] S. Chatzikyriakidis and Z. Luo. Formal Semantics in Modern Type Theories. Wiley/ISTE, 2020. [2] Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2/3),1988. [3] Z. Luo.Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994. [4] Z. Luo. Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6). 2012. [5] P. Martin-Lof. Intuitionistic Type Theory. Bibliopolis, 1984. [6] R. Montague. Formal Philosophy. Yale University Press, 1974. [7] A. Ranta.Type-Theoretical Grammar. Oxford University Press, 1994

In this talk we discuss a discrete pursuit-evasion game based on Rado's lion and man problem. We analyze geometric conditions of the domain where the game is played that ensure the success of the lion and, using ideas stemming from proof-mining, we extract a rate of convergence for the successive distances between the lion and the man. This talk is mainly based on the work [U. Kohlenbach, G. Lopez-Acedo, A. Nicolae, A uniform betweenness property in metric spaces and its role in the quantitative analysis of the "Lion-Man" game, Pacific J. Math. 310 (2021), 181-212].

The well-known proximal point algorithm (PPA) is a powerful and successful tool to approximate zeros of maximally monotone operators in Hilbert spaces. By the work of Rockafellar, we know that (PPA) is weakly convergent. However, a counter example by Gueler showed that, in general, one cannot guarantee strong convergence for this iteration. This prompted the study of several variants of the proximalpoint algorithm in an attempt to obtain strong convergence. In this talk, we discuss some of these variants and look at recent quantitative results obtained through the application of proof-theoretical techniques in the context of the proof mining program. References: [1] B. Martinet, Regularisation d???in equations variationnelles par approximations successives, Revue francaise d???informatique et de recherche operationnelle 4:154-158(1970). [2] R.T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization14(5):877???898 (1976). [3] O. Gueler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29(2):403-419 (1991). [4] U. Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg (2008). [5] P. Pinto, A rate of metastability for the Halpern type Proximal Point Algorithm, Numerical Functional Analysis and Optimization, 42(3):320-343, (2021). [6] L. Leustean and P. Pinto, Quantitative results on the Halpern type proximal point algorithm, Computational Optimization and Applications,79(1):101-125, (2021). [7] B. Dinis and P. Pinto, Quantitative results on the multi-parameters proximal point algorithm, Journal of Convex Analysis,28(3), 23 pp, (2021). [8] B. Dinis and P. Pinto, Effective metastability for a method of alternating resolvents,Submitted (2021) arXiv:2101.12675

It is well-known that classical arithmetic PA is $\Pi_2$-conservative over intuitionistic arithmetic HA. Using a generalized negative translation, we generalize this result with respect to theories of semi-classical arithmetic, which lie in-between PA and HA. In particular, it follows that PA is $\Pi_{k+2}$-conservative over HA + $\Sigma_k$-LEM where $\Sigma_k$-LEM is the low-of-excluded-middle scheme for formulas of $\Sigma_k$ form. In addition, we show that this conservation theorem is optimal in the sense that for any semi-classical arithmetic T, if PA is $\Pi_{k+2}$-conservative over T , then T proves $\Sigma_k$-LEM. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles. This is a joint work with Taishi Kurahashi.

Epistemic logic is used to formalize reasoning about knowledge, belief and related notions. However, such reasoning is done by an agent, that agent does not live alone. Her social communication with others, her social relation with others would have impact on her epistemic state. Enriching the traditional epistemic logic with a consideration of those social aspects is a project that my team has been working in the last few years. In this talk, I will introduce a few new logics that we have developed.

In this paper we develop sequent systems for classical tenselogic K.t [1] and Intuitionistic tense logic IK.t [2], which admit cut elimination and subformula property. Such results are extended to K.tand IK.t enriched with sp-axioms [3] including T,D,4,B,5, and so on. Moreover we develop proof search algorithms for some classical and intuitionistic tense logics based on these sequent systems. This is a joint work with Yu Peng and Xue Ge. References: 1. Burgess, J.P.: Basic Tense Logic, pp. 89-133. Springer Netherlands, Dordrecht(1984). 2. Ewald, W.: Intuitionistic tense and modal logic. Jounal of Symbolic Logic 51(1),166-179 (1986). 3. Kikot, Stanislav, Kurucz, Agi, Tanaka, Yoshihito, Wolter, Frank and Zakharyaschev, Michael: KRIPKE COMPLETENESS OF STRICTLY POSITIVE MODAL LOGICS OVER MEET-SEMILATTICES WITH OPERATORS. JOURNAL OF SYMBOLIC LOGIC, 84 (2). 533-588, (2019).

In the 1990s, Wilf and Zeilberger developed an algorithmic proof theory for combinatorial identities, which is called the Wilf-Zeilberger theory. This theory has become the bridge between symbolic computation and other research fields, such as combinatoric, special-function theory, number theory and mathematical physics etc. In this talk, I will first give a brief introduction to this theory by recalling some fundamental algorithms, and then present some intriguing applications in combinatorics.

Let X be a sequent calculus, and (R) be a rule in X that principally introduces positive occurrences of a key-note operator (like a modality). The diagonal extension of X is defined as a calculus gained via replacing rule (R) from X by rule (d.R), where (d.R) is just like (R), but has an extra negative copy of positive principals (from its conclusion) at each of its premises. The circular extension of X enjoys exact the same set of axioms and rules of X, but employs instead a generalized notion of proof, called circular proof. In a circular proof (tree), each leaf can either be a given axiom, or has a same sequent as another node on the unique path from that leaf to the root. [Shamkanov 2014] verified that the diagonal extension and the circular extension of a calculus for modal logic K4 coincide in terms of sequent provability (both are calculi for Goedel-Loeb provability logic). In this talk, we will sketch our finding that this can also be achieved purely in terms of proof transformation, which also allows us to prove a parallel result for [Visser 1981]'s BPL (sequent calculus from [Ishii et.al. 2011]), where both extensions are calculi for his FPL. This is a joint work with Yinqiu Zhu and Xinxian Chen.

The proximal point algorithm is a fundamental tool of convex optimization, traditionally attributed to Martinet [1], Rockafellar [2] (who named it) and Brezis and Lions [3]. In its many variants, it usually operates by iterating on a starting point a sequence of mappings dubbed "resolvents", whose fixed points coincide with the solutions of the optimization problem that one is aiming at. It has been observed by Eckstein [4] that the arguments used to prove the convergence of this algorithm "hinge primarily on the firmly nonexpansive properties of the resolvents". Inspired by this remark, the speaker, together with L. Leustean and A. Nicolae, has introduced in [5] the notion of jointly firmly nonexpansive family of mappings, which allows for a highly abstract proof of the proximal point algorithm's convergence, encompassing virtually all known variants in the literature. We have recently revisited [6] the concept, providing a conceptual characterization of it and showing how it may be used to prove other kinds of results usually associated with resolvent-type mappings. This all ties into the applied subfield of logic known as proof mining, which aims to proof-theoretically analyze proofs in concrete mathematics in order to extract additional information from them. In this talk, we shall report on all these findings and point towards works in progress and future developments, including an abstract version of the Halpern-style proximal point algorithm [7]. References: [1] B. Martinet, Regularisation d'inequations variationnelles par approximations successives [www.esaim-m2an.org]. Rev. Fran??aise Informat. Recherche Operationnelle 4, 154-158, 1970. [2] R. T. Rockafellar, Monotone operators and the proximal point algorithm [www.ceremade.dauphine.fr]. SIAM J. Control Optim. 14, 877-898, 1976. [3] H. Brezis, P. L. Lions, Produits infinis de resolvantes [link.springer.com]. Israel J. Math. 29, 329-345, 1978. [4] J. Eckstein, The Lions-Mercier Splitting Algorithm and the Alternating Direction Method are Instances of the Proximal Point Algorithm [citeseerx.ist.psu.edu]. Report LIDS-P-1769, Laboratory for Information and Decision Sciences, MIT, 1989. [5] L. Leustean, A. Nicolae, A. Sipos, An abstract proximal point algorithm [arxiv.org]. Journal of Global Optimization, Volume 72, Issue 3, 553?577, 2018. [6] A. Sipos, Revisiting jointly firmly nonexpansive families of mappings [arxiv.org]. arXiv:2006.02167 [math.OC], 2020. To appear in: Optimization. [7] A. Sipos, Abstract strongly convergent variants of the proximal point algorithm. In preparation.

We apply the methods of proof mining to a recent algorithm for approximating zeros of differences of maximal monotone operators due to Moudafi and provide rates of metastability and even, under suitable additional metric regularity assumptions, rates of convergence for the generated sequence. This logical analysis even suggests similar results under the incorporation of additional error terms into the algorithm. We carry out this extension and provide similar rates of metastability and convergence.

It is natural to represent real numbers in [-1,1] by streams of signed digits -1,0,1. Algorithms operating on such streams can be extracted from formal proofs involving a unary coinductive predicate CoI on (standard) real numbers x: a realizer of CoI(x) is a stream representing x. We address the question how to obtain bounds for the lookahead of such algorithms: how far do we have to look into the input streams to compute the first n digits of the output stream? We present a proof-theoretic method how this can be done. The idea is to replace the coinductive predicate CoI(x) by an inductive predicate I(x,n) with the intended meaning that we know the first n digits of a stream representing x. Then from a formal proof of I(x,n+1) ->I(y,n+1) -> I(1/2(x+y),n) we can extract an algorithm for the average function whose lookahead is n+1 for both arguments. -- This is joint work with Nils Koepp.

A survey of Wang’s philosophical works, which were as extensive, or perhaps more extensive, than his mathematical and logical works. I will focus on his later writings on Goedel and Wittgenstein, but it is important to see how generally important history and philosophy of logic were to Wang. In fact, I believe philosophy was regarded by him as the most important part of his work. I will build on a paper I wrote on Wang and Wittgenstein for the volume edited by Charles Parsons and Montgomery link, Hao Wang, Logician and Philosopher (College Publications, 2011).