Divulgação de material sobre Categorical Proof Theory, Proof Complexity e Topos Theory
Vitor Greati
Oi, pessoal,
Passando aqui para divulgar, a pedido de Amir Tabatabai, alguns materiais introdutórios que ele produziu recentemente sobre Categorical Proof Theory, Proof Complexity e Topos Theory. Segue abaixo o email que recebi dele, contendo detalhes.
[…]
As discussed, I have recently written two chapters on "Categorical Proof Theory" and "Proof Complexity", for upcoming books:
https://arxiv.org/abs/2408.09488
https://arxiv.org/abs/2505.03002
In addition, I taught a course on topos theory and its applications to proving independence results in set theory and arithmetic:
https://www.youtube.com/playlist?list=PLN71BuiwBivAtJG2ELAVuDP1OdL7wqihY
All three are intended for PhD students and postdoctoral researchers with little or no prior background in the respective areas. I would be grateful if you could share this material with interested students. Below is a brief description of the content for those who may be curious:
- Categorical Proof Theory
The survey explores various applications of categorical methods in proof theory. It is designed to be accessible with no prior familiarity with category theory. The necessary categorical background is introduced gradually, with an emphasis on the philosophical and informal aspects of proof. The only prerequisites are a basic understanding of logic, computability theory, topology, and ordered structures.
- Proof Complexity
The chapter serves as a survey of the basics of propositional proof complexity, both classical and non-classical, with a particular emphasis on the use of feasible interpolation to establish hardness results. To make the material accessible to a broader audience, it is presented with the assumption of only a basic familiarity with propositional, modal, and first-order logic, as well as a basic understanding of key concepts in computational complexity, such as the classes NP and PSPACE. Any additional concepts are introduced and explained as needed.
- Topos Theory
A topos is a category with some basic structure admitting a wide range of interesting interpretations. It can be a set-theoretical universe where the alternative types of mathematics take place, a generalized notion of space that lifts geometrical intuition far beyond the usual topological spaces or a syntax-free presentation of a first-order theory of some sort. In this course on topos theory, we mainly focus on its first interpretation and its role in model construction, unifying techniques from forcing and Heyting-valued models to different types of realizability. We start with a very short and gentle introduction to category theory. Then, we introduce elementary toposes and as their concrete examples, we present the categories of sheaves and Heyting-valued sets, on the one hand, and the effective topos, on the other. Then, we move to the connection between topoi and logic to present a topos-theoretical version of some independence results including the independence of the continuum hypothesis and the axiom of choice. We also use toposes to realize some exotic, yet coherent possibilities including the so-called computable (resp. Brouwerian) universe in which all the functions on natural numbers (resp. real line) are computable (resp. continuous). These models are used to prove the consistency of Church-Turing thesis (resp. Brouwer's theorem on continuity of all functions on the reals) from intuitionistic arithmetic (resp. analysis). Despite what it may appear at the first glance, the course only assumes familiarity with some basic concepts in first-order logic, algebra and topology and hence it must be accessible to all mathematics and computer science students. The rest, including the preliminaries on category theory, will be built during the course, whenever it’s needed.
Abraços,
Vitor