Authors: Paulo Firmino and Laurentiu Leuştean

This talk presents an application of proof mining to the viscosity approximation method (VAM) for accretive operators in Banach spaces, studied recently by Xu et al. [5]. Proof mining is a research program concerned with the extraction, by using proof-theoretic techniques, of new quantitative and qualitative information from mathematical proofs. We refer to Kohlenbach’s textbook [2] for details on proof mining.

Let \(X\) be a normed space and \(A:X\to 2^X\) be an accretive operator with a nonempty set of zeros. The VAMe iteration, a generalization of VAM obtained by adding error terms, is defined as follows:

\(\text{VAMe} \qquad x_0=x\in X, \quad x_{n+1}=\alpha_n f(x_n) +(1-\alpha_n)J_{\lambda_n}^Ax_n + e_n,\) where \(f:X\to X\) is an \(\alpha\)-contraction for \(\alpha\in[0,1)\), \((\alpha_n)_{n\in\mathbb{N}}\) is a sequence in \([0,1]\), \((\lambda_n)_{n\in\mathbb{N}}\) is a sequence in \((0,\infty)\), \((e_n)_{n\in\mathbb{N}}\) is a sequence in \(X\), and, for every \(n\in\mathbb{N}\), \(J_{\lambda_n}^A\) is the resolvent of order \(\lambda_n\) of \(A\).

In [1] we apply proof mining methods to obtain quantitative asymptotic regularity results for the VAMe iteration, providing uniform rates of asymptotic regularity, \(\left(J_{\lambda_n}^A\right)\)-asymptotic regularity and, for all \(m\in\mathbb{N}\), \(J_{\lambda_m}^A\)-asymptotic regularity of VAMe. For concrete instances of the parameter sequences, linear rates are computed by applying \cite[Lemma 2.8]{LeuPin23}, a slight variation of a lemma due to Sabach and Shtern [4].

Bibliography

1. P. Firmino, L. Leuştean, Quantitative asymptotic regularity of the VAM iteration with error terms for accretive operators in Banach spaces, arXiv:2402.17947 [math.OC], 2024.
2. U. Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics, Springer, 2008.
3. L. Leuştean, P. Pinto Rates of asymptotic regularity for the alternating Halpern-Mann iteration, Optimization Letters, https://doi.org/10.1007/s11590-023-02002-y, 2023.
4. S. Sabach, S. Shtern, A first order method for solving convex bilevel optimization problems, SIAM Journal on Optimization,vol. 27 (2017), no. 2, pp. 640–660.
5. H.-K. Xu, N. Altwaijry, I. Alughaibi, S. Chebbi, The viscosity approximation method for accretive operators in Banach spaces, Journal of Nonlinear and Variational Analysis, vol. 6 (2022), no. 1, pp. 37–50.

Authors: Piotr Błaszczyk and Anna Petiurenko

We present a new model of a non-Euclidean plane, in which angles in a triangle sum up to \(\pi\). It is a subspace of the Cartesian plane over the field of hyperreal numbers \(\mathbb{R}^*\), adheres to Hilbert’s axioms of absolute geometry, deviates from the parallel and Archimedean axioms, and is not hyperbolic. The model enables one to represent the negation of equivalent versions of the parallel axiom, such as the existence of the circumcircle of a triangle, and Wallis’ or Lagendre’s axioms, as well as the difference between non-Euclidean and hyperbolic planes. In our model, we present counterexamples to various versions of the parallel axiom, including those found in Euclid’s Elements, such as the circumcircle proposition. Additionally, we demonstrate the failure of the Wallis axiom and Legender’s axiom, showing discrepancies between their predictions and our model’s outcomes, thus challenging the equivalence of these axioms to the parallel axiom. We emphasize that besides the well-known non-Archimedean Pythagorean fields, there exist non-Archimedean Euclidean fields as well. The model has unique educational advantages because, unlike standard models of non-Euclidean planes involving non-Euclidean representations of straight lines (Poincaré) or angles (Klein), the key idea of our model requires only the basics of Cartesian geometry and non-Archimedean fields.

Bibliography

1. Max Dehn,Legendre’schen Sätze über die Winkelsumme im Dreieck,Mathematische Annalen,vol. 53 (1900), no. 3, pp. 404–439.
2. Piotr Bł,aszczyk, Anna Petiurenko,New model of non-Euclidean plane,arXiv:2302.12768 [math.HO],2023.
3. Piotr Bł,aszczyk, Anna Petiurenko,New model of non-Euclidean plane,arXiv:2302.12768 [math.HO],2023.

Matthias Baaz and George Metcalfe [1] provided a hypersequent calculus for infinite Łukasiewicz logic which is sound and complete with respect to \([0,1]\)-truth valued semantics and admits cut elimination. This result is further extended to first-order Łukasiewicz logic [2]. However, the cut elimination proof passes through semantics and the constructive information is missing. In particular, a proof with cut does not lead directly to a cut-free proof other than guarantees the existence of one.

The core ingredient of their proof is an approximate version of Herbrand’s theorem for first-order Łukasiewicz logic where a compactness argument is being used. Since Herbrand’s theorem is essentially a \(\Pi_2\)-statement, proof mining technique should be applicable here, provide a quantitative version of the theorem, and give an explicit upper bound for term witnesses of existence quantifiers. In this talk, I will describe my current progress in finding a constructive version of approximate Herbrand’s theorem for first-order Łukasiewicz logic. It will also be mentioned how this will contribute to a ultimate syntactic cut elimination proof, as well as some potential applications to continuous model theory.

Bibliography

1. Matthias Baaz, George Metcalfe,Herbrand’s theorem, skolemization and proof systems for first-Order Łukasiewicz logic,Journal of Logic and Computation,vol. 20 (2010), no. 1, pp. 35–54.
2. George Metcalfe, Nicola Olivetti, Dov Gabbay,Sequent and hypersequent calculi for abelian and Łukasiewicz logics,ACM Transactions on Computational Logic,vol. 6 (2005), no. 3, pp. 578–613.
3. Petr Hájek,Metamathematics of Fuzzy Logic,Kluwer,1998.
4. Ulrich Kohlenbach, Paulo Oliva,Proof mining: a systematic way of analysing proofs in mathematics,Proceedings of the Steklov Institute of Mathematics,vol. 9 (2002), no. 31.

Authors: Horatiu Cheval, David Nowak and Vlad Rusu

While partial recursive functions are ubiquitous in programming, proving results about their behavior using dependently typed proof assistants like Coq or Lean is not straightforward, as they typically require the totality of all functions. In this talk, we present a new approach for defining and reasoning about potentially non-terminating functions in such systems, and a work-in-progress formalization of these methods in the Lean theorem prover. Our framework, which is based on domain theory, allows one to embed such partial functions and constructs like while loops into proof assistants, maintaining one’s ability to write proofs about them.

At the same time, we introduce a domain-theoretical representation of coinductive types and partial corecursive functions. This, together with convenient automations, provides an extension to Lean, whose native theory does not include such notions. Furthermore, our representation allows one to also write corecursive functions that would normally not be accepted even in systems with built-in coinductives, like Coq, as they would violate a required guardedness condition (like the mirror function on infinitely deep trees), or they would need to be partial (like the filter function on streams).

Bibliography

1. Horac{t}iu Cheval, David Nowak, Vlad Rusu, Formal Definitions and Proofs for Partial (Co)Recursive Functions, https://inria.hal.science/hal-04360660 (2023).

If you know what a supercompact cardinal is, there are many possibilities that come to mind for what the phrase “\(\Sigma_2\)-supercompact” could mean. Noting that \(\textrm{HOD}\) is \(\Sigma_2\)-definable, it is natural to throw \(\textrm{HOD}\)-supercompactness and supercompactness in \(\textrm{HOD}\) into this mix, particularly given the interest in large cardinals in \(\textrm{HOD}\) arising from Woodin’s \(\textrm{HOD}\) conjecture.
We report on joint work with Shoshana Friedman disentangling these various possibilities, in part building on work of Bea Adam-Day [1], with models separating examples of these variants that are inequivalent.

Bibliography

1. Beatrice Adam-Day,Indestructibility and \(C^{(n)}\)-Supercompact Cardinals,PhD Thesis, University of Leeds, 2024.