Graduate Logic Seminar: Difference between revisions

From UW-Math Wiki
Jump to navigation Jump to search
No edit summary
(107 intermediate revisions by 7 users not shown)
Line 1: Line 1:
The Graduate Logic Seminar is an informal space where graduate students and professors present topics related to logic which are not necessarily original or completed work. This is a space focused principally on practicing presentation skills or learning materials that are not usually presented in a class.
The Graduate Logic Seminar is an informal space where graduate students and professors present topics related to logic which are not necessarily original or completed work. This is a space focused principally on practicing presentation skills or learning materials that are not usually presented in a class.


* '''When:''' TBA
* '''When:''' Mondays 3:30-4:30 PM
* '''Where:''' on line (ask for code).
* '''Where:''' Van Vleck B223
* '''Organizers:''' [https://www.math.wisc.edu/~jgoh/ Jun Le Goh]
* '''Organizers:''' [https://uriandrews.netlify.app/ Uri Andrews] and [https://sites.google.com/view/hongyu-zhu/ Hongyu Zhu]


The talk schedule is arranged at the beginning of each semester. If you would like to participate, please contact one of the organizers.
The talk schedule is arranged at the beginning of each semester. If you would like to participate, please contact one of the organizers.


Sign up for the graduate logic seminar mailing list:  join-grad-logic-sem@lists.wisc.edu
Sign up for the graduate logic seminar mailing list:  [mailto:join-grad-logic-sem@lists.wisc.edu join-grad-logic-sem@lists.wisc.edu]


== Fall 2021 - Tentative schedule ==
== Fall 2023 ==


To see what's happening in the Logic qual preparation sessions click [[Logic Qual Prep|here]].
The seminar will be run as a 1-credit seminar Math 975 in Fall 2023. If you are not enrolled but would like to audit it, please contact [mailto:andrews@math.wisc.edu Uri Andrews] and [mailto:hongyu@math.wisc.edu Hongyu Zhu].


== Spring 2021 - Tentative schedule ==
While you are welcome (and encouraged) to present on a topic of your own choice, feel free to ask for help from faculties and/or other graduate students.


=== February 16 3:30PM - Short talk by Sarah Reitzes (University of Chicago) ===
Presentation Schedule: https://docs.google.com/spreadsheets/d/15Qd4EzrrKpn1Ct5tur1P_FDc2czsdAVnUf_pfp65Lb4/edit?usp=sharing


Title: Reduction games over $\mathrm{RCA}_0$
Zoom link for remote attendance: https://uwmadison.zoom.us/j/96168027763?pwd=bGdvL3lpOGl6QndQcG5RTFUzY3JXQT09 (Meeting ID: 961 6802 7763, Password: 975f23)


Abstract: In this talk, I will discuss joint work with Damir D. Dzhafarov and Denis R. Hirschfeldt. Our work centers on the characterization of problems P and Q such that P $\leq_{\omega}$ Q, as well as problems P and Q such that $\mathrm{RCA}_0 \vdash$ Q $\to$ P, in terms of winning strategies in certain games. These characterizations were originally introduced by Hirschfeldt and Jockusch. I will discuss extensions and generalizations of these characterizations, including a certain notion of compactness that allows us, for strategies satisfying particular conditions, to bound the number of moves it takes to win. This bound is independent of the instance of the problem P being considered. This allows us to develop the idea of Weihrauch and generalized Weihrauch reduction over some base theory. Here, we will focus on the base theory $\mathrm{RCA}_0$. In this talk, I will explore these notions of reduction among various principles, including bounding and induction principles.
Possible readings:
* (Elementary) Proof Theory: Chapters 4-7 of <i>[https://projecteuclid.org/ebooks/lecture-notes-in-logic/Aspects-of-Incompleteness/toc/lnl/1235416274 Aspects of Incompleteness]</i> by Per Lindström.
* An invitation to model-theoretic Galois theory.  <i>[https://arxiv.org/abs/0909.4340 On arxiv here.]</i>
* Variations on the Feferman-Vaught Theorem <i>[https://arxiv.org/abs/1812.02905 On arxiv here.]</i>
* Any of several papers on "Turing Computable Embeddings"
* Computability/Model/Set Theory: Consult faculties/students for recommended texts on specific areas.


=== March 23 4:15PM - Steffen Lempp ===
=== September 11 - Organizational Meeting ===


Title: Degree structures and their finite substructures
We will meet to assign speakers to dates.


Abstract: Many problems in mathematics can be viewed as being coded by sets of natural numbers (as indices).
=== '''September 18 - Taeyoung Em''' ===
One can then define the relative computability of sets of natural numbers in various ways, each leading to a precise notion of “degree” of a problem (or set).
'''Title:''' Explicit construction of non-quasidetermined game on <math>\mathcal P(2^{\mathbb N})</math> without using A.C. ([https://wiki.math.wisc.edu/images/Gale-Stewart_implies_A.C..pdf Supplement])
In each case, these degrees form partial orders, which can be studied as algebraic structures.
The study of their finite substructures leads to a better understanding of the partial order as a whole.


=== March 30 4PM - Alice Vidrine ===
'''Abstract:''' We will go over briefly some basic information about trees and infinite games. Then we prove the Gale-Stewart Theorem. The proof of the theorem motivates definition of quasistrategy. Then we will briefly introduce Borel determinacy. We will go over how the usage of A.C. makes convenient for us to make a non-quasidetermined or undertermined game. We will give an explicit construction of a non-quasidetermined game on <math>\mathcal P(2^{\mathbb N})</math> without using A.C.


Title: Categorical logic for realizability, part I: Categories and the Yoneda Lemma
=== '''September 25 - Karthik Ravishankar''' ===
'''Title:''' Spectra of structures


Abstract: An interesting strand of modern research on realizability--a semantics for non-classical logic based on a notion of computation--uses the language of toposes and Grothendieck fibrations to study mathematical universes whose internal notion of truth is similarly structured by computation. The purpose of this talk is to establish the basic notions of category theory required to understand the tools of categorical logic developed in the sequel, with the end goal of understanding the realizability toposes developed by Hyland, Johnstone, and Pitts. The talk will cover the definitions of category, functor, natural transformation, adjunctions, and limits/colimits, with a heavy emphasis on the ubiquitous notion of representability.
'''Abstract:''' One way to measure the complexity of a structure is via its spectrum - the set of Turing degrees of its copies. In this talk, we'll look at the definition and first properties of the spectrum followed by some examples. In particular, we'll show that the non-computable degrees and the hyperimmune degrees form a spectrum while the DNC degrees do not.


[https://hilbert.math.wisc.edu/wiki/images/Cat-slides-1.pdf Link to slides]
=== '''October 2 - Hongyu Zhu''' ===
'''Title:''' Continuum Hypothesis: On Platonism and Pluralism ([https://wiki.math.wisc.edu/images/CH.pdf Slides] and [https://uwmadison.zoom.us/rec/share/lSe2BL28988PGmmthWKA6FM7bWOJ0eR6vxP4laS7O6ImNN2gQ5skPJ6-C8KlbGcm.G48mQQ0qlW-lo3gr Recording]; Passcode: .iXJs?1t)


=== April 27 4PM - Alice Vidrine ===
'''Abstract:''' Despite its independence from ZFC, the continuum hypothesis continues to be of interest to logicians. In this talk, we will see arguments for settling the truth of CH in one way or another (or yet another). We will see how mathematical arguments (the inner model program) are intertwined with philosophical beliefs (mathematical Platonism and pluralism) about the set-theoretic universe(s).


Title: Categorical logic for realizability, part II
=== '''October 9 - Hannah Ashbach ''' ===
'''Title:''' An Introduction to Constructive Mathematics ([https://wiki.math.wisc.edu/images/An_Introduction_to_Constructive_Mathematics.pdf Slides] and [https://uwmadison.zoom.us/rec/share/UIxI2m2WWMnitZTd1oQxYxl6vpashJdvf_2UtN6erlFXN9yNgm7q0mhXw1min0-L.cz3b7tsbBPlsgxD6 Recording]; Passcode: 5.$c5L+2)


Abstract: Realizability is an approach to semantics for non-classical logic that interprets propositions by sets of abstract computational data. One modern approach to realizability makes heavy use of the notion of a topos, a type of category that behaves like a universe of non-standard sets. In preparation for introducing realizability toposes, the present talk will be a brisk introduction to the notion of a topos, with an emphasis on their logical aspects. In particular, we will look at the notion of a subobject classifier and the internal logic to which it gives rise.
'''Abstract:''' Have you ever written a mathematical proof and felt dissatisfied after writing QED? Perhaps you had proven the existence of a particularly complicated mathematical object, but you have no clue how that object may actually look or be constructed. Or perhaps you are ready to denounce the Axiom of Choice after reading about its far-reaching consequences. Constructive logic is a formal logic system that seeks to clear up these concerns for mathematicians, though not all mathematicians agree with the power it holds-- or takes away.


==Previous Years==
=== '''October 16 - Rune Chen ''' ===
'''Title:''' An Introduction to Model-Theoretic Galois Theory
 
'''Abstract:''' Given an arbitrary first-order theory with elimination of imaginaries, the standard Galois theory can be translated into a model-theoretic version, which can be further generalized and thus be useful in other algebraic settings. In this talk, we will give a brief introduction to model-theoretic Galois theory and then look at a simple case of model-theoretic Galois correspondence. We will skip the detailed discussion of elimination of imaginaries by choosing our theory T to be a first-order theory coding finite sets and working in a large enough saturated model M of T.
 
=== '''October 23 - John Spoerl ''' ===
'''Title:''' The Computational Content of Forcing
 
'''Abstract:''' Given information about a ground model, how much can you know about it’s forcing extensions? Given a forcing extension, how much can you know about its ground model? This talk will be a primer on forcing and a review of the main results of Hamkins, Miller and Williams’ 2020 paper: “Forcing as a Computational Process”.
 
=== '''October 30 - Chiara Travesset ''' ===
'''Title:''' Mission-time LTL (MLTL) Formula Validation Via Regular Expressions
 
'''Abstract:''' Mission-time Linear Temporal Logic (mLTL) is an extension of propositional logic that includes temporal operators over finite intervals of time. A computation is a (finite) sequence consisting of a truth assignment for each propositional variable at each time step. This presentation will describe how we can use regular expressions to describe the structure of the computations that make a given mLTL formula true. We prove soundness and completeness, and also give an implemented algorithm (the WEST program) and analyze its complexity both theoretically and experimentally. We generate a test suite using control flow diagrams to robustly test the code. Finally, we present the REST theorem, which significantly simplifies certain sets of computations. This talk only requires basic familiarity with propositional logic and computer science.
 
=== '''November 6 - Antonio Nakid Cordero ''' ===
'''Title:''' Martin's Conjecture in the Turing degrees and the Enumeration Degrees
 
'''Abstract:''' Martin's Conjecture is an attempt to formalize the empirical phenomenon that "naturally occurring" Turing degrees are well-ordered. In this talk, I'll go over how one can make that into a precise mathematical statement, a uniform version of the conjecture that has been fully resolved, and some of the complications of trying to propose a similar conjecture in the enumeration degrees. If time allows, I'll report on my ongoing project in this direction.
 
=== '''November 13 - Alice Vidrine ''' ===
'''Title:''' Enumeration Weihrauch degrees and closed choice problems ([https://wiki.math.wisc.edu/images/EWdeg_Grad_seminar_Fall_23.pdf Slides] and [https://uwmadison.zoom.us/rec/share/F_pDYkWhHGiMTy7Rkqrb_PpeJnjxBCo0ZIMOEHV4CP-XfJodbV-P8igStgVwiXq4.A7ONs9u5Em6-3Gvp Recording] Passcode: C89k#5&0)
 
'''Abstract:''' In the Weihrauch degrees, we think of elements of Baire space as names for elements of mathematical objects. In the enumeration Weihrauch (eW) degrees we follow a similar idea, but our names may only carry positive information. It turns out that this coding by positive information separates several choice problems that are equivalent in the Weihrauch degrees, and in this talk we look at some of the more striking examples and their proofs. We close with some discussion of various directions for further research.
 
=== '''November 20 - Logan Heath ''' ===
'''Title:''' A Proof Theorist's Guide to First Aid: CUT-Elimination and Other Results of Classical Proof Theory ([https://wiki.math.wisc.edu/images/A_Proof_Theorist%27s_Guide_to_First_Aid.pdf Slides])
 
'''Abstract:''' When are correct proofs also "bad" proofs, how can we avoid them, and should we even try? In this talk we examine some early results of classical proof theory regarding the consistency of the sequent calculus for FOL and '''PA'''. In both cases our approach will be to avoid proofs which are technically correct, but also defective in some sense.
 
=== November 27 - Thanksgiving Break ===
=== '''December 4 - Mei Rose Connor ''' ===
'''Title:''' When ‘And’ is Too Much and ‘Or’ is Not Enough
 
'''Abstract:''' This work was motivated by the seven–valued predication system of the Jaina religion, which states that no statement exists as an absolute. This system, known as ''Saptabhangivada'' in Sanskrit, has 7 truth values that are the non-empty subsets of the set {asti, nāsti, avaktavyah}. These words translate to: ''it is'', ''it is not'', and ''it is unassertible'', respectively. This talk will explore how these seven truth values relate to each other, the problems encountered when trying to formalise this system, and the author’s current resolution of said problems using lattice theory and introducing an eighth truth value.
 
=== '''December 11 - Ang Li ''' ===
'''Title:''' TBA
 
'''Abstract:''' TBA
 
<!-- Template
 
=== '''September 18 - Karthik Ravishankar''' ===
'''Title:''' Lowness for Isomorphism ([https://wiki.math.wisc.edu/images/Karthik_talk.pdf Slides])
 
'''Abstract:''' A Turing degree is said to be low for isomorphism if it can only compute an isomorphism between computable structures only when a computable isomorphism already exists. In this talk, we show that the measure of the class of low for isomorphism sets in Cantor space is 0 and that no Martin Lof random is low for isomorphism.
 
-->
 
== Previous Years ==


The schedule of talks from past semesters can be found [[Graduate Logic Seminar, previous semesters|here]].
The schedule of talks from past semesters can be found [[Graduate Logic Seminar, previous semesters|here]].

Revision as of 03:18, 27 November 2023

The Graduate Logic Seminar is an informal space where graduate students and professors present topics related to logic which are not necessarily original or completed work. This is a space focused principally on practicing presentation skills or learning materials that are not usually presented in a class.

The talk schedule is arranged at the beginning of each semester. If you would like to participate, please contact one of the organizers.

Sign up for the graduate logic seminar mailing list: join-grad-logic-sem@lists.wisc.edu

Fall 2023

The seminar will be run as a 1-credit seminar Math 975 in Fall 2023. If you are not enrolled but would like to audit it, please contact Uri Andrews and Hongyu Zhu.

While you are welcome (and encouraged) to present on a topic of your own choice, feel free to ask for help from faculties and/or other graduate students.

Presentation Schedule: https://docs.google.com/spreadsheets/d/15Qd4EzrrKpn1Ct5tur1P_FDc2czsdAVnUf_pfp65Lb4/edit?usp=sharing

Zoom link for remote attendance: https://uwmadison.zoom.us/j/96168027763?pwd=bGdvL3lpOGl6QndQcG5RTFUzY3JXQT09 (Meeting ID: 961 6802 7763, Password: 975f23)

Possible readings:

  • (Elementary) Proof Theory: Chapters 4-7 of Aspects of Incompleteness by Per Lindström.
  • An invitation to model-theoretic Galois theory. On arxiv here.
  • Variations on the Feferman-Vaught Theorem On arxiv here.
  • Any of several papers on "Turing Computable Embeddings"
  • Computability/Model/Set Theory: Consult faculties/students for recommended texts on specific areas.

September 11 - Organizational Meeting

We will meet to assign speakers to dates.

September 18 - Taeyoung Em

Title: Explicit construction of non-quasidetermined game on [math]\displaystyle{ \mathcal P(2^{\mathbb N}) }[/math] without using A.C. (Supplement)

Abstract: We will go over briefly some basic information about trees and infinite games. Then we prove the Gale-Stewart Theorem. The proof of the theorem motivates definition of quasistrategy. Then we will briefly introduce Borel determinacy. We will go over how the usage of A.C. makes convenient for us to make a non-quasidetermined or undertermined game. We will give an explicit construction of a non-quasidetermined game on [math]\displaystyle{ \mathcal P(2^{\mathbb N}) }[/math] without using A.C.

September 25 - Karthik Ravishankar

Title: Spectra of structures

Abstract: One way to measure the complexity of a structure is via its spectrum - the set of Turing degrees of its copies. In this talk, we'll look at the definition and first properties of the spectrum followed by some examples. In particular, we'll show that the non-computable degrees and the hyperimmune degrees form a spectrum while the DNC degrees do not.

October 2 - Hongyu Zhu

Title: Continuum Hypothesis: On Platonism and Pluralism (Slides and Recording; Passcode: .iXJs?1t)

Abstract: Despite its independence from ZFC, the continuum hypothesis continues to be of interest to logicians. In this talk, we will see arguments for settling the truth of CH in one way or another (or yet another). We will see how mathematical arguments (the inner model program) are intertwined with philosophical beliefs (mathematical Platonism and pluralism) about the set-theoretic universe(s).

October 9 - Hannah Ashbach

Title: An Introduction to Constructive Mathematics (Slides and Recording; Passcode: 5.$c5L+2)

Abstract: Have you ever written a mathematical proof and felt dissatisfied after writing QED? Perhaps you had proven the existence of a particularly complicated mathematical object, but you have no clue how that object may actually look or be constructed. Or perhaps you are ready to denounce the Axiom of Choice after reading about its far-reaching consequences. Constructive logic is a formal logic system that seeks to clear up these concerns for mathematicians, though not all mathematicians agree with the power it holds-- or takes away.

October 16 - Rune Chen

Title: An Introduction to Model-Theoretic Galois Theory

Abstract: Given an arbitrary first-order theory with elimination of imaginaries, the standard Galois theory can be translated into a model-theoretic version, which can be further generalized and thus be useful in other algebraic settings. In this talk, we will give a brief introduction to model-theoretic Galois theory and then look at a simple case of model-theoretic Galois correspondence. We will skip the detailed discussion of elimination of imaginaries by choosing our theory T to be a first-order theory coding finite sets and working in a large enough saturated model M of T.

October 23 - John Spoerl

Title: The Computational Content of Forcing

Abstract: Given information about a ground model, how much can you know about it’s forcing extensions? Given a forcing extension, how much can you know about its ground model? This talk will be a primer on forcing and a review of the main results of Hamkins, Miller and Williams’ 2020 paper: “Forcing as a Computational Process”.

October 30 - Chiara Travesset

Title: Mission-time LTL (MLTL) Formula Validation Via Regular Expressions

Abstract: Mission-time Linear Temporal Logic (mLTL) is an extension of propositional logic that includes temporal operators over finite intervals of time. A computation is a (finite) sequence consisting of a truth assignment for each propositional variable at each time step. This presentation will describe how we can use regular expressions to describe the structure of the computations that make a given mLTL formula true. We prove soundness and completeness, and also give an implemented algorithm (the WEST program) and analyze its complexity both theoretically and experimentally. We generate a test suite using control flow diagrams to robustly test the code. Finally, we present the REST theorem, which significantly simplifies certain sets of computations. This talk only requires basic familiarity with propositional logic and computer science.

November 6 - Antonio Nakid Cordero

Title: Martin's Conjecture in the Turing degrees and the Enumeration Degrees

Abstract: Martin's Conjecture is an attempt to formalize the empirical phenomenon that "naturally occurring" Turing degrees are well-ordered. In this talk, I'll go over how one can make that into a precise mathematical statement, a uniform version of the conjecture that has been fully resolved, and some of the complications of trying to propose a similar conjecture in the enumeration degrees. If time allows, I'll report on my ongoing project in this direction.

November 13 - Alice Vidrine

Title: Enumeration Weihrauch degrees and closed choice problems (Slides and Recording Passcode: C89k#5&0)

Abstract: In the Weihrauch degrees, we think of elements of Baire space as names for elements of mathematical objects. In the enumeration Weihrauch (eW) degrees we follow a similar idea, but our names may only carry positive information. It turns out that this coding by positive information separates several choice problems that are equivalent in the Weihrauch degrees, and in this talk we look at some of the more striking examples and their proofs. We close with some discussion of various directions for further research.

November 20 - Logan Heath

Title: A Proof Theorist's Guide to First Aid: CUT-Elimination and Other Results of Classical Proof Theory (Slides)

Abstract: When are correct proofs also "bad" proofs, how can we avoid them, and should we even try? In this talk we examine some early results of classical proof theory regarding the consistency of the sequent calculus for FOL and PA. In both cases our approach will be to avoid proofs which are technically correct, but also defective in some sense.

November 27 - Thanksgiving Break

December 4 - Mei Rose Connor

Title: When ‘And’ is Too Much and ‘Or’ is Not Enough

Abstract: This work was motivated by the seven–valued predication system of the Jaina religion, which states that no statement exists as an absolute. This system, known as Saptabhangivada in Sanskrit, has 7 truth values that are the non-empty subsets of the set {asti, nāsti, avaktavyah}. These words translate to: it is, it is not, and it is unassertible, respectively. This talk will explore how these seven truth values relate to each other, the problems encountered when trying to formalise this system, and the author’s current resolution of said problems using lattice theory and introducing an eighth truth value.

December 11 - Ang Li

Title: TBA

Abstract: TBA


Previous Years

The schedule of talks from past semesters can be found here.