Many real-life situations lead us to considering a mathematical problem dealing with finding all possible numbers \(x\) satisfying a certain formula. In most primitive cases, this formula is an equation involving basic arithmetic operations (like the one we considered in Lecture 1). As an example of a formula that does not fall in this category, consider the following one:
\(x<y^2\) for every value of \(y\) (Formula A)
In other words, the formula expresses the property that no matter what value of \(y\) we pick, we will always have \(x<y^2\). Let us write this purely symbolically as follows (so that it looks more like a formula!):
\(y\Rightarrow x<y^2\) (symbolic form of Formula A)
In general, the symbol "\(\Rightarrow\)" describes logical implication of statements. Here the implication is: if \(y\) has a specific value then \(x<y^2\). In the symbolic form above, the assumption that \(y\) has a specific value is expressed by just writing \(y\) on the LHS (left-hand-side) of the implication symbol "\(\Rightarrow\)". Since we are not giving any further detail as to which specific value does \(y\) have, the implication must not be dependent on such detail, and hence the RHS (right-hand-side), \(x<y^2\), must hold for all values of \(y\). Note however that this type of symbolic forms, where variables are allowed to be written on their own like in the LHS of the implication symbol above, is not a standard practice. We will nevertheless stick to it, as it makes understanding proofs easier.
So, what is the solution of Formula A? If \(x<y^2\) needs to hold for every value of \(y\), then in particular, it must hold for \(y=0\), giving us \(x<0^2=0\). This can be written out purely symbolically, as a proof:
In this blog-based lecture course we will learn how to build mathematical proofs.
Let us begin with something simple. You are most likely familiar with "solving an equation". You are given an "equation", say \[x+2=2x-3\] with an "unknown" number \(x\) and you need to find all possible values of \(x\), so that the equation holds true. You then follow a certain process of creating new equations from the given one until you reach the solution: \[2+3=2x-x\] \[5=x\] This computation is in fact an example of a proof. To be more precise, there are two proofs here: one for proving that
if \(x+2=2x-3\) then \(x=5\) (Proposition A),
and the other proving that
if \(x=5\) then \(x+2=2x-3\) (Proposition B).
The first proof is the same as the series of equations above. The second proof is still the same series, but in reverse direction. The two Propositions A and B together guarantee that not only \(x=5\) fulfills the original equation (Proposition B), but that there is no other value of \(x\) that would fulfill the same equation (Proposition A). It is because of the presence of these two proofs in our computation that we can be sure that \(x=5\) is indeed the solution of the equation \(x+2=2x-3\).
In general, a proof is a series of mathematical formulas, like the equations above. However, in addition to a "vertical" structure of a proof, where each line displays a formula that has been derived from one or more previous lines, there is also a "horizontal" structure, where each line of a proof has a certain horizontal offset. This is, at least, according to a certain proof calculus formulated by someone by the name of Fitch. There are other ways of defining/describing proofs; in fact, there is an entire subject of proof theory, which studies these other ways. We will care little about those other ways and stick to the one we started describing, as it is closest to how mathematicians actually compose proofs in their everyday job.
So where were we? We were talking about "vertical" and "horizontal" structure of a proof. Not to complicate things too much at once, let us first get a handle on the vertical structure of proofs, illustrating it on various example proofs that have most primitive possible horizontal structure. We will then, slowly, complexify the horizontal structure as well.
For Proposition A, the proof goes like this:
The numbers at the start of each line are just for our reference purposes, they do not form part of the proof. Line 2 is a logical conclusion of Line 1: if \(x+2=2x-3\) then it must be so that \(2+3=2x-x\), since we could add \(3\) to both sides of the equality and subtract \(x\) as well – a process under which the equality will remain true if it were true at the start.
Line 3 is (again) a logical conclusion of Line 2: since \(5=2+3\) and \(2x-x=x\), so if the equality in Line 2 were true then the equality in Line 3 must be true as well.
A series of lines of mathematical formulas where every next line is a logical conclusion of the previous one or more lines, is a mathematical proof with simplest possible horizontal structure. We will call such proofs "basic".
Proposition B also has a basic proof:
\(x=5\) and \(x+2=2x-3\),
\(x=5\) or \(x+2=2x-3\),
The goal of this project is to build a proof assistant based on the SOFiA proof system, where the capital letters in SOFiA stands for Synaptic First Order Assembler (the purpose of the lower-case "i" will be explained further below). The use of terms "synapsis" and "assembler" is a suggestion of Brandon Laing, who wrote an MSc Thesis, "Sketching SOFiA" (2020), where the notion of an assembler was introduced: an assembler is the monoid of words in a given alphabet, seen as a monoidal category. The main result of his MSc Thesis was a characterization of assemblers using intrinsic properties of a monoidal category. An assembler gives a robust theoretical framework which guides the syntactical structure of the SOFiA proof system. The latter has been refined through a series of discussions with Louise Beyers and Gregor Feierabend in 2021, after which the first computer implementation of the SOFiA proof system was produced, based on the Python programming language. You can learn about it here. In January 2021, Gregor Feierabend developed a self-contained Haskell implementation, with user interface and documentation, which can be accessed here.
These deduction rules do not include rules for disjunction or fallacy. The latter can be implemented as axiom schemes. So at its base, the SOFiA proof system embodies a bit less than intuitionistic logic. This is marked by the appearance of lower-case "i" in "SOFiA". Note however that because in the SOFiA syntax there is no distinction between "objects" and "statements about objects", the SOFiA proof system is not quite the same as the usual proof system of a first-order logic, although in a loose sense SOFiA does have the structure of a first-order language. One of the key differences with standard first-order languages is that in SOFiA one does not introduce additional relational or functional symbols. Instead, one may write any sequence of allowed characters in SOFiA which can be given the intended meaning of a relational or a functional symbol by means of axioms. Possibility for a sound and complete embedding of any first-order logic in SOFiA still needs to be proved and is currently one of the founding themes of PhD research by Brandon Laing.
The current version(s) of the SOFiA proof assistant have the following shortcomings, which are to be addressed in the near future:
The bracket notion for mathematical proofs is an adaptation of the Fitch notation for Gentzen's natural deduction proof system. It has led to the development of the SOFiA proof assistant. This post brings together some videos explaining the bracket notation and the first-order formal language for mathematics in the context of the bracket notation.
Here you will find the content for the Category Theory course given under the National Graduate Academy NGA-Coursework of the CoE-MaSS. The lectures are on Saturdays 9:00-11:00.
Register here to receive the Zoom link for joining the lectures
There is also a Discord channel for this course, which you can find on the Discord server of the NGA-Coursework project.
This is a video-based course aimed at post-graduate students and as well academics interested to learn about category theory, with live participation of the audience shaping the content of the course. For a reading course at the South African honors level, see:
This is the blog post of the 2022 August NITheCS Mini-School. Let us begin with some useful links:
This picture symbolizes a human state when one is working on a routine task, while one's mind looks into the bigger picture of things. While guitarists hands are busy playing on the guitar, his eyes are looking into the open space from a balcony. The fence of the balcony symbolizes the restrictions imposed on us by the necessity of a routine task.
This picture shows the back of a woman with yellow hair, in a stylish red dress, gazing at the white moon. The hair is blowing in a light wind. Mountains covered in snow are in the background. Her outfit is certainly not a match for the cold weather, but contemplation will keep her body warm. This picture symbolizes that deeper things in life can give us physical strength.
This freehand digital artwork represents the idea that significant change requires restructuring of foundations. The solid ground on the right middle side of the picture (the foundations) dissolves into an uproar of waves that illustrate the process of restructuring, which may appear to be chaotic. Going back from the left to the right side of the picture the waves subside into (new) foundations.
These are notes in progress for a talk given at the online user group conference of the advanced programme mathematics organized by ieb (19 February 2022)
