Elimination and cut-elimination. 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 to a proof net which is the quotient of a polynomial ring \( P_{\pi} \). The indeterminants of \( P_{\pi} \) come from the (atomic axioms of the) formulas in \( \pi \), and the kernel \( I_{\pi} \) of the quotient map \( P_{\pi} \longrightarrow R_{\pi} \) comes from 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}, 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 the case where \( \pi' \) is not normal, the reduction can still be related to the Buchberger Algorithm, but with a small adaptation made. In fact, this altered version of the Buchberger Algorithm is more naturally expressed as a new algorithm which we present in this paper, the so called Falling Roofs algorithm.
The internal logic and topoi. Topoi are often described as “generalised theories of sets”, but are they? This description is often given to topoi due to the similarities of the internal logic with ZF set theory. However, there are important differences, which extend further than just the fact that the internal language of a topos is an intuitionistic logic (and ZF classical). Even in Boolean topoi, where the law of exluded middle holds, still there is the following difference between the theories: the existence of the union of an arbitrary collection of sets is an axiom of ZF, and the product is intrinsically defined, but in the internal language this is reverseed; there is a product type constructor, and the union of two subobjects only makes sense in the context of a common parent object. This difference is not visible in ZF set theory during usual mathematical discorse, but when importing the usual set theoretic definitions of mathematical objects into the internal language, this distinction becomes significant. How these hurdles arrise and how they are solved is the content of this document.
2020:Gentzen-Mints-Zucker Duality. A duality consists of two different points of view on the same object. The greater the difference between the two points of view, the more informative is the duality which relates them. Such correspondences are important because two independent discoveries of the same structure is strong evidence that the structure is natural. The duality between the simply typed λ-calculus (without product types) and the intuitionistic sequent calculus is the content of this document, and is interesting precisely because sequent calculus proofs and lambda terms are not tautologically the same thing: for example the cut-elimination relations are fundamentally local
while the β-equivalence relation is global (see Section 4.3). In this sense sequent calculus and λ-calculus are respectively local and global points of view on a common logicocomputational mathematical structure.
2017: A proof tree constructor for the Linear Lambda Calculus. The λ-lambda calculus is a syntactic system designed with Girard's linear logic in sight. The idea is simple: since the Curry-Howard correspondence holds between intuitionistic natural deduction and the simply typed λ-calculus, and since the intuitionistic sequent calculus embeds into the linear logic sequent calculus, one may conjecture the existence of a "linear λ-calculus". Such a system has been designed, and the content of this document is a passer which takes as input a term in the linear λ-calculus and provides html code which displays the (necessarily unique) term-constructing tree corresponding to this term. For example, 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 to 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 (one off invitation)
Computation in logic as the splitting of idempotents in algebraic geometry; two models of multiplicative linear logic (repeat of ChoCoLa talk, slides are different) slides
Trends in Linear Logic and Applications
Normal functors[ions], [the irrelevance of] power series, and [a new model of] λ-calculus slides
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
How to present mathematics
2023-09-20
Have a point
Some people struggle with social anxiety and this causes them to socialise in many ways which are not due to their concious decisions but instead are due to fear. For instance, it is fine to be quiet in social situations, but only if you are 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" inbetween 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 concious 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 hindsite, I cannot believe I was even embarrassed by this story. Nowdays, if somebody were to laugh at me during a public presentation, it would not effect 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 focussing 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
In dotpoints:
- 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 which they came without?
Tips for improving
Record your lectures and watch them back. This might be excrutiating 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 concious 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.
