If you are interested in giving a talk (in person or over Zoom), then please contact Alvaro (apintado $$ sas $$ upenn $$ edu).
Upcoming Talks
-
Bifibrations for Classical Logic
Speaker: Oualid Merzouga
Date: May 14, 2026
Abstract: We present ongoing work extending A Fibrational Framework for Substructural and Modal Logics of Licata, Riley, and Shulman to classical logics.
-
Proof Mining and Elimination of Ultraproducts
Speaker: Jin Wei
Date: May 19, 2026
Abstract: Positive bounded logic, or equivalently continuous logic, extends first-order logic to accommodate normed or metric structures. It retains a number of desirable model-theoretic properties, most notably the availability of ultraproduct construction. However, arguments based on ultraproducts are typically nonconstructive and obscure quantitative information in the proof.
Proof mining of ultraproducts in positive bounded logic was treated by Günzel and Kohlenbach, who introduced a formal system interpreting positive bounded logic based on monotone functional interpretation. Within this framework, a uniform boundedness principle(UB) substitutes ultraproducts in many applications. Moreover, a corresponding metatheorem guarantees the elimination of UB, yielding quantitative results. A different approach to the elimination of ultraproducts in first-order logic was also developed by Henry Towsner using infinitary logic.
In recent joint work with Neri and Kohlenbach, we revise and extend the framework of Günzel and Kohlenbach and establish an equivalence between the saturation principle and UB. This allows the treatment of a substantially broader class of model-theoretic arguments. We will also present two case studies, one from stability theory of groups and another from the metastable dominated convergence theorem.
Past Talks