Penn Graduate Logic Seminar (GLoS)

Upcoming Talks

• Fibrational framework for classical substructural and modal logics

  Speaker: Oualid Merzouga

  Date: May 14, 2026

  Abstract: Substructural and modal logics describe resource management, modalities of truth, and computational mechanisms. In my first talk, I motivated the existing fibrational approach of Licata, Shulman, and Riley, which gives an account of intuitionistic systems by organizing modes, structural rules, and connectives through two layers of type theories. In this talk, I will expose ongoing work attempting to extend this perspective to classical and multi-conclusion systems.
  
  The central idea is to replace ordinary intuitionistic proof trees with a richer notion of descriptor: a combinatorial object that records not only which variables are available, but also how inputs, internal computations, and outputs are connected together. These descriptors behave like directed acyclic graphs with input, internal, and output nodes. They make it possible to represent morphisms between contexts of multiple inputs and outputs (polymorphisms), rather than only morphisms with a single output (multimorphisms), and therefore provide a possible syntax for classical sequents.
  
  I will explain how descriptors can be composed by a cut operation, how they encode substructural behavior such as contraction, weakening, and exchange on the input and output sides, and how they suggest a path toward a bifibrational semantics of polycategories. The ultimate goal is to obtain a unifying framework in which modes describe logical or computational resources, descriptors describe the shape of proofs and programs, and classical connectives arise from the specifications of descriptors.
  
  Reading the abstract of Licata, Shulman, and Riley's paper on "A fibrational framework for substructural and modal logic" is encouraged. Knowledge of some fibrational notions of category theory will make the talk feel whole, although it is not required to appreciate it. Some familiarity with the sequent calculus is expected.

• 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