Fudan Logic Seminar 2024
June 7
Location: HGW2403
Speaker: Daisuke IKEGAMI (池上 大祐)
Time: 13:30 - 15:00
Speaker: Liping TANG (唐丽萍)
Time: 15:15 - 16:45
May 14
Speaker: Thomas Scanlon
Time: 13:30 - 15:30. Location: HGW2301.
(Un)decidability in function fields
Starting with J. Robinson's 1949 proof of the undecidability of the first-order theory of the field of rational numbers through a reduction to Gödel's first incompleteness theorem, various other theories of fields have been shown to be undecidable. On the other hand, A. Tarski's 1929 theorem on the decidability of Euclidean geometry is really a theorem on the decidability of the first-order theory of the field of real numbers. Theories of various other fields, including $p$-adic fields, fields of formal power series over decidable fields of characteristic zero, and pseudofinite fields, amongst others, have been shown to be decidable. It is a long standing open problem, appearing in print in 1963, whether the theory of the field $\mathbb{C}(t)$ of rational functions in one variable over the complex numbers is decidable.
In this lecture, I will describe some attempts to resolve this problem. In particular, I will discuss some methods using the theory of elliptic curves to define complicated structures in this field, but then also why those structures are likely decidable in their own right. I will also discuss other approaches to the decidability problem based on the theories of algebraic curves and more precisely an attempt to encode finite sets using families of hyperelliptic curves. Finally, I will speculate about the connections between this problem and the theory of rational curves on algebraic varieties.
April 30
Location: HGW2403.
Speaker: Bokai YAO (姚博凯)
Time: 13:30 - 15:30
什么是无素集合论？
在传统的集合论框架中，一切皆为集合。所谓“无素”（urelements）是指那些非集合的元素。若在集合论宇宙中引入无素，其对集合论公理系统会产生何种影响？这些公理与无素的数量是否存在某种联系？选择公理在其中扮演怎样的角色？最后，一个涵盖所有存在的集合论宇宙背后的哲学图景又是什么？本报告将通过介绍无素集合论的基本概念及方法，对这些问题进行探讨。handout
Speaker: Pierre-Louis Curien
Time: 15:30 - 17:30
Combinatorics and geometry of opetopes
Opetopes were introduced by Baez and Dolan at the end of the last millenium as a foundational tool for higher-dimensional algebra. They are shapes featuring associativity, coherence of asscoiativity, coherence of coherence of associativity, etc., in an unbiased setting. Here, unbiased refers to a product of varying arity, as opposed to a biased, binary one. While opetopes can be defined in a compact way by means of categorical abstractions (e.g. via polynomial functors as introduced by Joyal and Gambino), they are difficult to grasp and characterise combinatorially or syntactically. I shall report on work of Louise Leclerc (some of which joint with me) on proving equivalences of different definitions of opetopes. I shall also sketch how opetopes may label a suitable triangular subdivision of the family of associahedra, that refines the historically important Boardman-Vogt cubical subdivision (work in progress).
April 26
Location: HGW2403. Tencent Meeting: 711-524-519, code: 666666
Speaker: Jason CHEN (陈泽晟)
Time: 13:30 - 15:30
Metamathematical methods in descriptive set theory: a case study in the taxonomy of proofs
This project has a two-fold goal: on the practical side, to provide a rough collection and classification of the various types of proofs in descriptive set theory that can be characterized by their use of metamathematical methods. In doing so, I also aim to track the degree of involvement of metamathematical tools in these proofs, and hope to demonstrate that there is a sui generis methodology, in full analogy with, say, "algebraic methods". And on the philosophical side, the goal is to probe perhaps more general questions about the nature proofs and methods, particularly regarding what it means to characterize a proof by the method used, and what a method imports in a proof.
To do this, I will first motivate this project a little by relating it to a broader philosophical project born out of Dawson's monograph "Why Prove it Again? Alternative Proofs in Mathematical Practice" about the values of having multiple proofs. Next, I will consider an obvious non-example of metamathematical proof (that makes use of metamathematical methods), which will allow me to sketch a list of putative objections to calling such proofs metamathematical. These putative objections will shed light on the practice of organizing mathematical proofs by their methodology. Following that, I will present a series theorems and proofs that involve increasingly substantial use of metamathematical methods. At each turn, I will analyze how the proof in question addresses the earlier objections, honing in on the issue of whether the metamathematical methods can be translated away without loss of insight. This sort of dialectics will hopefully shed light on our practical taxonomy of proofs by their methodology, as well as on the specific question of whether a proof can be said to make substantial use of metamathematical methods. Slides
April 24
Location: HGW2501. Tencent Meeting: 459-205-619, code: 666666
Speaker: Jason CHEN (陈泽晟)
Time: 15:30 - 17:30
The emergence of invariant descriptive set theory
The common story of the history of descriptive set theory tells of Cantor's ingenious venture into the transfinite, how his work found palpable expression with the French analysts, the ill-fated program of the Moscow school to understand the projective hierarchy, and its marvellous revival in the west with large cardinals and determinacy. Nevertheless, a cursory glance at some of the recent publications in generalist mathematics journal such as the Annals of Mathematics and Inventiones Mathematicae reveals that the field has been making remarkable contributions to a wide range of mathematical areas, including ergodic theory, functional analysis, measure theory, and graph combinatorics, with techniques and concerns that have little motivation in ways of classical concerns such as the continuum hypothesis or large cardinals.
The present project is a partial attempt to fill this obvious gap in the literature, aiming to trace the pre-history of the rich theory, developed in the past 30 years, of invariant descriptive set theory (better known as the theory of Borel or definable equivalence relations). My goal is to shed light on a host of questions that naturally arise, for example: is there a clear historical narrative of the development of the field? What was in the air mathematically from the Moschow school's study of the projective sets to the rise of definable equivalence relations? When did descriptive set theorists turn to abstract structures among classification problems, rather than working on the concrete classification problems themselves? What technical tools were available when this turn took place, and where did they originate?
One pleasant finding is that the field of Borel equivalence relations is undergirded by two separate threads of development: on the one hand, the development of abstract techniques establishing non-reductions, motivated by Luzin and his complexity-regularity program, as well as Sierpinski's effort to ratify the axiom of choice into mathematical canon; on the other hand, the development of the actual reductions, motivated by non-set-theoretic concerns such as ergodic theory and the theory of Polish groups. As an interlude, we will also briefly touch upon the role that the infamous Luzin Affair played in this history. Slides
April 23
Location: HGW2403
Speaker: Baptiste Mélès
Time: 13:30 - 15:30
The rationale of axioms: Peano's arithmetic in Coq's standard library
In logic and mathematics, axioms provide the rationale for theorems, but they obviously do not need to have a rationale themselves. However, some logicians and mathematicians attempted to justify each axiom on the basis of the global properties of the logic or the theory they intended to construct. Starting with Gentzen and the requirement for cut-elimination, I will show that this requirement is now the basis of the Coq proof assistant. Due to global properties of Coq's logic, the number of Peano's axioms can be reduced from 5 to 2. As a result, some axiomatics are governed by a more demanding structure than a simple "aggregate" of axioms.
April 2
Location: HGW2403
Speaker: Yuan LI (李元)
Time: 13:30 - 15:30
On the Minimum Depth of Circuits with Linear Number of Wires Encoding Good Codes
Let $S_d(n)$ denote the minimum number of wires of a depth-$d$ (unbounded fan-in) circuit encoding an error-correcting code $C:\{0, 1\}^n \to \{0, 1\}^{32n}$ with distance at least $4n$. Gál, Hansen, Koucký, Pudlák, and Viola [IEEE Trans. Inform. Theory 59(10), 2013] proved that $S_d(n) = \Theta_d(\lambda_d(n)\cdot n)$ for any fixed $d \ge 3$. By improving their construction and analysis, we prove $S_d(n)= O(\lambda_d(n)\cdot n)$. Letting $d = \alpha(n)$, a version of the inverse Ackermann function, we obtain circuits of linear size. This depth $\alpha(n)$ is the minimum possible to within an additive constant 2; we credit the nearly-matching depth lower bound to Gál et al., since it directly follows their method (although not explicitly claimed or fully verified in that work), and is obtained by making some constants explicit in a graph-theoretic lemma of Pudlák [Combinatorica, 14(2), 1994], extending it to super-constant depths.
We also study a subclass of MDS codes $C: \mathbb{F}^n \to \mathbb{F}^m$ characterized by the Hamming-distance relation $\textrm{dist}(C(x), C(y)) \ge m - \textrm{dist}(x, y) + 1$ for any distinct $x, y \in \mathbb{F}^n$. (For linear codes this is equivalent to the generator matrix being totally invertible.) We call these superconcentrator-induced codes, and we show their tight connection with superconcentrators. Specifically, we observe that any linear or nonlinear circuit encoding a superconcentrator-induced code must be a superconcentrator graph, and any superconcentrator graph can be converted to a linear circuit, over a sufficiently large field (exponential in the size of the graph), encoding a superconcentrator-induced code.
This is a joint work with Andrew Drucker.