Spring Semester
-
An Introduction to Homotopy Type Theory
Speaker: Elan Roth
Date: May 05, 2025
Abstract: Equality is weird. Sometimes two things are the same, sometimes they're not, and sometimes we can’t decide (yes, that was a computability joke). Homotopy Type Theory (HoTT) doesn’t fix this, but by treating types as spaces and equalities as paths, HoTT offers a geometric reimagining of logic and truth. In this talk, I’ll introduce some of the strange and elegant ways HoTT lets us think about identity, structure, and equivalence.
-
Random Types
Speaker: Krishan Canzius
Date: April 28, 2025
Abstract: This talk focuses on a paper by Kyle Gannon and James Hanson, in which they define a probability measure on the space of types over the monster model. Their goal, broadly speaking, was to determine which properties should hold of almost all randomly sampled types. We will discuss model theoretic concepts such as Keisler measures, Morley products, and almost sure theories with the goal of understanding some of their results.
-
Axioms that Correspond to Structural Rules
Speaker: Jin Wei
Date: April 14, 2025
Abstract: When studying proof systems for various logics—particularly substructural or nonclassical ones, we are naturally led to the following natural question: Which axioms, when added to a base logic, preserve the cut-freeness of the proof system? Remarkably, this question has a precise algebraic counterpart: Which varieties of pointed residuated lattices are closed under MacNeille completions?
In this talk, we will explore this connection through the lens of algebraic proof theory. We will introduce the substructural hierarchy and demonstrate that the class N_2 precisely marks the expressive boundary for (intuitionistic) sequent-style calculi, while the class P_3 represents the limit for hypersequent-style. As we classify familiar axioms within the hierarchy, an open question naturally arises: what proof system corresponds to the class N_3, which includes many important axioms, such as distributivity and the Łukasiewicz axiom. -
Domain Theory and Denotational Semantics
Speaker: Tanner Duve
Date: April 07, 2025
Abstract: Domain theory was introduced by Dana Scott in the 1960s, motivated by the search for a denotational semantics of the lambda calculus. Denotational semantics is concerned with the mathematical meaning of programming languages, where programs are to be interpreted as morphisms in certain categories. This talk will introduce the basic theory of domains, viewed as both order-theoretic structures and topological spaces, and explore some of their friendly properties that make them uniquely suitable for modeling computer programs. We will explore the connections between computability and continuity, and discuss the role of domains in the semantics of programming languages - in particular interpreting recursive definitions as least fixpoints. Basic concepts in order theory, category theory, and topology will be used but no advanced understanding of these is required from the audience.
-
A General framework for mainstream logics
Speaker: Oualid Merzouga
Date: March 24, 2025
Abstract: Most of us learned in kindergarten that intuitionistic logic can be obtained from classical logic by giving up double negation elimination. A few months later, we learned that Linear logic is a pleasant system to work in as it makes the features of intuitionistic and classical logic apparent.
Widely used logics are arguably composed of three groups ; the identity , the structural and the logical groups. A large class of logics can then be defined by variation of those rules present in the structural and logical groups.
Proving interesting facts (cut elimination, normalization, invertibility,…) of those logics becomes redundant on an intuitive level and tedious to carry formally.
Wouldn’t it be great to construct a general framework such that all variations can be explained ? Proving interesting facts about them would only have to be done once and for all. An attempt at deriving such a framework has been published by D. Licata, M.Shulman, and M. Riley in 2017 in , what the speaker consider, a landmark paper.
In this talk, we will go over the main idea of the framework which relies on formalizing a concept of resource usage. Knowledge of category theory is helpful but not required. Knowledge of gentzen style sequent calculus is desired.
The only reference used in this talk is : “A Fibrational Framework for substructural and modal logics”, by the authors mentioned above. -
Twists and Termination: The Braid Group in Lean
Speaker: Hannah Fechtner (CMU)
Date: March 03, 2025
Abstract: Braids can be defined topologically (think: intertwined strings in space) or algebraically in terms of generators and relations. I will discuss the algebraic definition, and its formalization in Lean. The word problem in the braid group is decidable, and the larger, ongoing project is to implement a verified algorithm, following Dehornoy. I will discuss the formalization of the first major stage: defining the braid monoid and embedding it into the braid group. While formalizing the remaining portion, I noticed visual intuition sneaking into the termination/correctness proof for this algorithm. I will present a novel proof which can rescue the claim, and further include a bit of the history of the mathematics behind braids and its path to rigor. Lastly, I will briefly share a peek at a braid visualization widget-to-come, which will hopefully allow the user to generate Lean proofs by clicking and dragging strings!
-
An Introduction to Cubical Type Theory
Speaker: Carmine Ingram
Date: February 24, 2025
Abstract: Homotopy type theory has been a hot topic for a number of years now, of interest both as a synthetic setting for homotopy theory and for its convenient type-theoretic properties. Unfortunately, one of its central features --- the univalence axiom, which asserts that it is possible to transport equivalences between types into genuine equalities --- has long lacked a computational interpretation. This talk will summarize the fundamentals of cubical type theory, which replaces a number of primitives in homotopy type theory in order to create a type theory in which univalence is a theorem, not an axiom, and in which canonicity is restored.
-
Artin Gluing: A Semantic Approach to Logical Relations
Speaker: Riley Shahar
Date: February 10, 2025
Abstract: A standard approach to proving meta-theoretic properties of a proof system or type theory is to first define a stronger dependent predicate R---often called a logical relation---by induction on syntax, and prove the desired property by showing that every well-formed term satisfies this stronger property. In categorical semantics, this technique looks like an Artin gluing of the syntactic category along a hom-functor. This talk will introduce this technique, at least in the special case of so-called "sconing," and utilize it for a categorical proof of the existence property of intuitionistic logic.
-
Proof by Contradiction Can Be Constructive, If You Take This Simple Trick...
Speaker: Jin Wei
Date: January 27, 2025
Abstract: Since Brouwer, constructivism in mathematics has been closely associated with intuitionistic logic and the BHK interpretation. Intuitionistic logic is asymmetric as it prioritizes truth over falsity by treating ¬A as A→⊥. Another source of asymmetry comes from the contraction rule where we are allowed to use assumptions arbitrarily many times while only one conclusion is derived. These cause serious difficulties in the Dialectica interpretation when extracting constructive content from mathematical proofs. In this talk, we will talk about Michael Shulman’s antithesis interpretation with affine linear logic, obtained by demanding both proofs and refutations for formulas and removing the contraction rule. We will see how classical definitions and reasoning, including proof by contradiction, can be constructivized in this setting and why affine logic could plausibly replace intuitionisitic logic as the cornerstone of constructive reasoning.
-
Girard's Paradox for Set Theorists, via Hurkens
Speaker: Riley Shahar
Date: November 22, 2024
Abstract: Since Brouwer, constructivism in mathematics has been closely associated with intuitionistic logic and the BHK interpretation. Intuitionistic logic is asymmetric as it prioritizes truth over falsity by treating ¬A as A→⊥. Another source of asymmetry comes from the contraction rule where we are allowed to use assumptions arbitrarily many times while only one conclusion is derived. These cause serious difficulties in the Dialectica interpretation when extracting constructive content from mathematical proofs. In this talk, we will talk about Michael Shulman’s antithesis interpretation with affine linear logic, obtained by demanding both proofs and refutations for formulas and removing the contraction rule. We will see how classical definitions and reasoning, including proof by contradiction, can be constructivized in this setting and why affine logic could plausibly replace intuitionisitic logic as the cornerstone of constructive reasoning.
-
On the de Finetti--Hewitt--Savage--Theorem
Speaker: Irfan Alam
Date: October 18, 2024
Abstract: I wrote a long preprint titled "Generalizing the de Finetti--Hewitt--Savage Theorem" (arXiv:2008.08754v4) in 2020 (last updated in 2023), which used methods from nonstandard analysis to vastly generalize de Finetti's theorem from probability theory. Based on recommendations from the peer-review of this preprint, I recently had to create an updated shorter version consisting of the mathematical core of this work, titled "On the de Finetti--Hewitt--Savage Theorem" (accessible at this link). I am aiming to talk about this work in an accessible manner. In particular, I plan to spend almost equal amounts of time on the following topics:
- Introduction to nonstandard analysis.
- Review of requisite concepts from probability theory and topology; and nonstandard perspectives on those concepts.
-
Towards Linear Topoi
Speaker: Riley Shahar
Date: September 27, 2024
Abstract: Topos theory plays a central role in geometry and categorical logic. For instance, topoi yield a natural semantic theory of intuitionistic dependent type theories. One important step in this theory is the observation that topoi are Heyting categories, i.e. that propositions in the internal logic of a topos can be refined along intuitionistjc predicates. In this talk, I will attempt to give an accessible outline of this classical story and motivate the study of "linear topoi", categories which exhibit topos-like behavior with respect to a linear internal logic. I will conclude with a discussion of some progress towards an axiomatic presentation of these categories.
-
Completeness of GŁ∀
Speaker: Jin Wei
Date: September 20, 2024
Abstract: In this talk, I will share my most recent result on the completeness of hypersequent calculus for first-order Łukasiewicz logic. I will first provide necessary backgrounds and motivations, especially its connection to continuous model theory, and explain the story of earlier incomplete (picking my word carefully) attempts by others. Then I will present my proof in details. I will also point out three potential future research directions and share why I believe they are very exciting.
-
Induction and coInduction formalized
Speaker: Oualid Merzouga
Date: September 09, 2024
Abstract: Induction is a widely recognized proof technique in mathematics. From your five-years old past friend asking, “How do you know the numbers don’t stop?” to a thesis topic on “How to prove that Peano Arithmetic is consistent” this technique has become and continues to be one of the most trusted tools for mathematicians.
To investigate further this proof technique, we can formalize it within mathematics itself. We will employ category theory to find an appropriate formulation for what it means to prove something by induction.
This natural process will lead us to define inductive data structures and their dual, co-inductive structures. We will begin by building intuition behind these concepts through standard examples and conclude by embedding these ideas within category theory, enabling you to confidently respond to your past five-year-old friends:
“Of course, numbers don’t stop; they are merely the manifestation of the initial algebra for a specific endofunctor!”