Contributed Talks 3
Chair: Andrei Sipoș
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
16:30 
Laurentiu Leuştean, Proof mining and the viscosity approximation method 
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 prooftheoretic 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


16:55 
Piotr Błaszczyk, New model of nonEuclidean plane 
Authors: Piotr Błaszczyk and Anna Petiurenko We present a new model of a nonEuclidean 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 nonEuclidean 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 wellknown nonArchimedean Pythagorean fields, there exist nonArchimedean Euclidean fields as well. The model has unique educational advantages because, unlike standard models of nonEuclidean planes involving nonEuclidean representations of straight lines (Poincaré) or angles (Klein), the key idea of our model requires only the basics of Cartesian geometry and nonArchimedean fields. Bibliography


17:20 
Jin Wei, Constructive Version of Herbrand’s Theorem for FirstOrder Łukasiewicz Logic 
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 firstorder Ł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 cutfree proof other than guarantees the existence of one. The core ingredient of their proof is an approximate version of Herbrand’s theorem for firstorder Ł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 firstorder Ł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


17:45 
Horatiu Cheval, Defining and reasoning about partial (co)recursive functions in Lean 
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 nonterminating functions in such systems, and a workinprogress 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 At the same time, we introduce a domaintheoretical 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 builtin coinductives, like Coq,
as they would violate a required guardedness condition
(like the Bibliography


18:10 
Andrew BrookeTaylor, Disentangling Sigma_2 variants of supercompactness 
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. Bibliography
