This thesis explores the relationship between linear logic and algebraic geometry, particularly focusing on how proofs in linear logic can be interpreted as polynomials in atomic formulas. These polynomials correspond to closed subschemes of projective space. The thesis connects these concepts to computational aspects, drawing on the Geometry of Interaction program to understand the dynamics of proof rewrites, such as cut-elimination.
The primary contribution of the thesis is the development of a model for shallow multiplicative exponential linear logic proofs using Hilbert schemes, extending previous work that interpreted proofs as ideals in polynomial rings. This new model provides a geometric interpretation of the exponential fragment of linear logic, where proofs are patterns of equality between linear formulas. The thesis also discusses various models of linear logic, including those related to error-correcting codes and matrix factorizations, highlighting the relationships between these models and the process of cut-elimination.
The work ties algebraic geometry with proof theory, offering new insights into how linear logic can be represented geometrically, particularly in the context of projective schemes and Hilbert schemes. The thesis includes several secondary contributions, such as reinterpreting the dynamics of proof systems and exploring connections to functional programming languages.
A connection between multiplicative proof nets in linear logic and quantum error-correcting codes is defined. They propose associating a quantum code with each proof net, with cut-elimination in logic corresponding to quantum error correction.
A Hilbert space and stabilizer quantum code is associated to each proof net, where logical operations are represented by quantum system interactions. The cut-elimination process is modeled as a cooling procedure that reduces the system's energy to its ground state, which reflects the logical content of the proof net. Each reduction in a proof net corresponds to a quantum cooling operation, linking logical transformations to physical processes in quantum systems.
The paper also introduces examples, such as Majorana chains, and defines a category of stabilizer codes to formalize these relationships, bridging logic, algebra, and quantum information.
Part of the content of a proof net is the identification of different occurrences of the same formula in a proof. Taking this seriously, we define a ring \( R_{\pi} \) associated with a proof net, which is the quotient of a polynomial ring \( P_{\pi} \). The indeterminates of \( P_{\pi} \) are derived from the (atomic propositions of the) formulas in \( \pi \), and the kernel \( I_{\pi} \) of the quotient map \( P_{\pi} \longrightarrow R_{\pi} \) is determined by the links of \( \pi \).
If there exists a multi-step reduction of a proof \( \gamma: \pi \longrightarrow \pi' \) to a normal form \( \pi' \), then the generators of the ideals \( I_{\pi} \) and \( I_{\pi'} \) are related to one another via the Buchberger Algorithm, a pre-existing algorithm used to calculate Gröbner bases from generating sets. In cases where \( \pi' \) is not normal, the reduction can still be related to the Buchberger Algorithm, but with a small adaptation. This modified version of the Buchberger Algorithm is more naturally expressed as a new algorithm, which we introduce in this paper: the so-called Falling Roofs algorithm.
Topoi are often described as “generalized theories of sets,” but are they? This description is frequently attributed to topoi due to the similarities between their internal logic and ZF set theory. However, there are important differences that extend beyond the fact that the internal language of a topos is intuitionistic logic, while ZF set theory is classical. Even in Boolean topoi, where the law of excluded middle holds, there remains a critical distinction between the theories: the existence of the union of an arbitrary collection of sets is an axiom in ZF, and the product is intrinsically defined. However, in the internal language of a topos, this relationship is reversed; there is a product type constructor, while the union of two subobjects only makes sense in the context of a common parent object.
This difference is not apparent in ZF set theory during typical mathematical discourse, but it becomes significant when importing the usual set-theoretic definitions of mathematical objects into the internal language of a topos. The way these challenges arise and how they are addressed is the subject of this document.
A duality consists of two distinct perspectives on the same underlying object. The greater the disparity between these perspectives, the more informative the duality that relates them. Such correspondences are significant because two independent discoveries of the same structure strongly suggest that the structure is natural.
This document explores the duality between the simply typed λ-calculus (without product types) and the intuitionistic sequent calculus. This duality is particularly interesting because sequent calculus proofs and lambda terms are not inherently identical: for instance, the cut-elimination relations in sequent calculus are fundamentally local, while the β-equivalence relation in λ-calculus is inherently global (see Section 4.3). In this sense, the sequent calculus and λ-calculus offer, respectively, local and global perspectives on a shared logico-computational mathematical structure.
This paper examines two approaches to modeling Linear Logic: one focusing on models with syntax as a support, and the other on syntax with models in a supporting role. Categorical models fall into the first category, often requiring constraints like the exponential modality (!) to be a comonad. Our focus is on "models of cut-elimination," which emphasize the syntactic perspective, often overlooked.
We simplify Girard’s complex "normal functors" model, removing the need for normal functors and focusing on simpler normal functions. This leads to a new model distinct from existing ones like coherence spaces. We also reconsider Girard's use of "analytic functors," showing that λ-calculus interpretation only requires that functions are determined by their restrictions to smaller domains, not by power series. Our work challenges the necessity of categorical models, highlighting that the key feature of Linear Logic is its inherent linearity.
The λ-calculus is a syntactic system designed with Girard's linear logic in mind. The concept is straightforward: since the Curry-Howard correspondence connects intuitionistic natural deduction with the simply typed λ-calculus, and the intuitionistic sequent calculus embeds into the linear logic sequent calculus, one might conjecture the existence of a "linear λ-calculus." Such a system has been constructed, and the content of this document describes a parser that takes a term in the linear λ-calculus as input and generates HTML code displaying the (necessarily unique) term-constructing tree corresponding to the term.
For instance, the term
\( \lambda q \lambda p.\, \texttt{copy } q \texttt{ as } r, s \texttt{ in } \lambda z.\, \texttt{derelict}(p)(\texttt{derelict}(s)(\texttt{derelict}(r)z)) \)
has the following diagram associated with it.
Notes
Algebra/geometry
Elementary commutative algebra: Linear algebra, rings and modules, polynomial rings, fields, field extensions, integral extensions and Jacobson rings, dimension theory, discrete valuation rings, completions.
Secondary algebra: Graded rings/modules/algebras, (quasi-)regular sequences, Clifford algebras.
Introduction to varieties: Affine varieties, projective varieties (Gröbner bases), morphisms, singularities.
Some of the following seminars took place at metauni, a virtual and free-to-access campus. Come and join us on discord
Cambridge seminar
Computation in logic as the splitting of idempotents in algebraic geometry; two models of multiplicative linear logic (repeat of ChoCoLa talk, slides are different)
Trends in Linear Logic and Applications
Normal functors[ions], [the irrelevance of] power series, and [a new model of] λ-calculus
CHoCoLa (2023)
Computation in logic as the splitting of idempotents in algebraic geometry; two models of multiplicative linear logic slides
First order logic video Models of first order theories video Gödel's First Incompleteness Theorem Part 1 (proof sketch) video Gödel's First Incompleteness Theorem Part 2 (general recursive functions) video Gödel's First Incompleteness Theorem Part 3 (Chinese Remainder Theorem and the β-function trick) video Gödel's First Incompleteness Theorem Part 4 (properties of general recursive functions) video Gödel's First Incompleteness Theorem Part 5 (general recursive functions are representable 1) video Gödel's First Incompleteness Theorem Part 6 (general recursive functions are representable 2) video Ax–Grothendieck Theorem part 1 (proof sketch) video Ax–Grothendieck Theorem part 2 (the geometric part) video Ax–Grothendieck Theorem part 3 (Skolemisation) video Ax–Grothendieck Theorem part 4 (Lower Lownehiem-Skolem Theorem) video Ax-Grothendieck Theorem part 5 (Finishing the proof) video
Group de travail catégories (2022) (all the videos can be found here by scrolling down)
Introduction to Category Theory
Topoi and logic 1
Topoi and logic 2
Elimination and cut-elimination
Institut de Mathématiques de Marseille, Logic and Interactions (2022)
The Church-Rosser Theorem, notes, improved notes Introduction to Lambda-Calculus, notes System F in the real world: Haskell and functional programming, notes, the referenced talk by Rich Hickey is Simple made easy
Tips for presenting mathematics
Have a point
Some people struggle with social anxiety and this causes them to socialise in many ways which are not due to their conscious decisions but instead are due to fear. For instance, it is fine to be quiet in social situations, but only if you have decided to be quiet, rather than because you feel pushed into it due to fear of how you will be received. Explicitly, most people are quiet in social situations because they feel like they can't be loud. This means that they have been quiet out of necessity, and not out of choice. Therein lies the problem.
Presenting mathematics exhibits many similar circumstances. A classic and also very visible example is the tendency to say "um", or "like" incessantly (spelling). This person has clearly not made the choice to put "like" in between every second word, so what has compelled them to do it? The answer is fear, and our aim is to remove this fear.
In fact, this is our intermediate aim, our ultimate aim is to give a conscious presentation. That is, to have a vision of how your presentation will go, to realise this vision, and to realise this vision with intention.
Anxiety
I have written about anxiety more generally in my Obdurate posts, but to summarise I will briefly say here that the key method for overcoming anxiety is not to convince oneself that the thing they are terrified of is not going to happen, but instead is to build up strength in self so that one can manage the scary thing even if it does occur. Do not convince yourself that you will not be rejected by your crush, but instead learn that life continues even if you are, etc...
Here is an anecdote: one time I gave a presentation where the goal was to state and prove a difficult result. A few days before the presentation, I was in the office of a particular mathematician who took some time to explain a point to me which I wasn't entirely sure I understood by the time I left their office. During the lecture, I made a statement which was blatantly false (but which I thought was true) and the error was precisely that which the mathematician had explained to me just a few days prior. They were in the audience, so they spoke up and corrected me, but I still didn't understand entirely, though in that moment I realised with resounding clarity that indeed the argument I had prepared was erroneous. This was all within the first few minutes of the lecture.
I pressed on with the talk, and tried to give as good of a lecture as I could, but ultimately what I presented was wrong and needed the fix which had already been explained to me and which I was yet to understand. After a grueling hour the talk was over and I approached the mathematician. I told them that I still did not understand that solution to the problem in my proof and they responded by saying “yes, clearly” and then laughed, a few others heard them and laughed too.
Needless to say, I died of embarrassment. I then went out for coffee with a few members from the audience and I spent the entire time mentally lashing myself.
Anyway, time passed and a year or so later that same mathematician and myself were having a conversation and they mentioned the stress of presenting a lecture to an undergraduate audience where they're meant to be the authority figure yet still it's possible to become confused. I brought up the lecture I had given a year prior to them, and how I was able to relate to such a moment of embarrassment... The mathematician, who themselves had corrected me on that particular day, did not even remember the moment! I was surprised they did not, but eventually they did, to which they said "oh don't waste time thinking about that, it wasn't a big deal at all".
The point is that life continues, even if the most "terrifying" thing possible happens. In hindsight, I cannot believe I was even embarrassed by this story. Nowadays, if somebody were to laugh at me during a public presentation, it would not affect me the same way at all. This means I am not scared of such things which in turn leads to me giving better presentations because I can focus on more important things. A friend of mine said it best, "those who are cringe are free", and a mind willing to be laughed at is more capable of creating pioneering thoughts, so embrace that which terrifies you, it will maximise your chances of speaking well, and if you fail, then fail proudly and move on.
One last point on anxiety. When I took acting classes as a child, they taught me "the person on stage is the least important person in the room". It's a bit over the top but I like the sentiment. You're not presenting mathematics for yourself, but rather for the audience. If you are really struggling with anxiety, try to take the focus off yourself and put it onto the audience. You're there to enlighten them, not to prove yourself. It's similar to social anxiety, if you're really struggling then focus more on making the other people feel good, rather than focusing on making yourself look good. You will feel relief to have the attention taken off you, and that will be a good starting point.
Technical points
Write big,
Underline the word you're defining in your definitions,
Do not say "um",
Do not say "like" unless it's as a proper word,
If you do have this tendency, then combat it by physically slowing yourself down whilst speaking, take deep breaths, and try to talk less.
Allow your presentation to be boring. We're mathematicians, not entertainers. You should focus on making only true statements. One great way to make this easier for yourself is to speak less (silence is only deafening to the anxious presenter; long patches of silence whilst you think through the next argument you're presenting, or whilst you're writing up something long, are completely unnoticed by the audience).
Have a goal. What should the audience leave with that they didn't come with?
Tips for improving
Record your lectures and watch them back. This might be excruciating to begin with, but if you are putting yourself out there as a presenter, and you do not have a good idea of what that physically looks like from the perspective of an audience member, then you are missing a crucial aspect of self-awareness. This lack of self-awareness will create many blind spots. The removal of these blind spots is the goal, because then you can be conscious of how you conduct your presentation.
Get feedback. Ask people what they thought and how you could improve, people love to tell you what you did wrong... so let them!
Art
Taming the frame (2021), a mathematical commentary on an artwork created by Nobby Seymour
Nobby's statement:
Nature (in the form of gravity and as a commanding higher voice) has had its say; now for a more rigorous formal approach.
Using the integer 1 and the first four prime numbers, 2, 3, 5 and 7, I constructed a Cartesian grid centred on x and y = 0. I plotted all possible positive and negative values of the x and y coordinates (48 in all) and these formed the vertices of a square grid. Then I selected the 24 outmost coordinates and these served as the centrepoint of circles whose circumference passed through the midpoint of the previously established grid squares. This formed an interlocking path of arc quadrants which form the (blue) trajectory above, reminiscent of patterns in in early Chinese and Islamic Design. The central void also appealed to me, for reasons at this stage unfathomable.
I was pleased to see the frame as a trajectory, emerging from the geometric matrix that shapes much of our world.
There is a famous optical illusion2 in which some people see a duck, others a rabbit. My friend Will Troiani, who has tutored me over the years in mathematics I have required for various projects, turns up at the studio, looks at my Trajectory and sees a beautiful algorithm lurking there.
Before we reach the concluding work, Taming the Frame, I am delighted by any confluence of visual theory and science, Take it away Will.
