The SOFiA Proof Assistant Project

Background

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.

Overview of the SOFiA Proof System

The SOFiA proof system is an adaptation of the Fitch notation for natural deduction. The main novelty of the SOFiA proof system is the use of variables as statements, which leads to reducing quantified statements to implications. This allows unification of deduction rules for implication with those for the universal and existential quantifiers. The basic deduction rules for the proof system then are:

• Making an assumption (no restrictions except that the assumption must be a valid SOFiA expression).
• Restating an already stated SOFiA expression.
• Recalling a theorem or an axiom, external to the proof.
• Equating a stated SOFiA expression with itself.
• Synapsis: stepping out of an assumption block (this allows to conclude quantified statements, as well as implications).
• Application a SOFiA expression (this allows to conclude from quantified statements as a generalization of the modus ponens rule).
• Substitution: substituting SOFiA expressions within each other based on already stated equalities.

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.

Developing the Proof Assistant

The current version(s) of the SOFiA proof assistant have the following shortcomings, which are to be addressed in the near future:

• The proofs can only be built line-by-line, it is currently not possible for the computer to fill the missing lines. This applies to both the Python and Haskell implementations. 
• The Python implementation source code is messy and there is currently no documentation.
• The Haskell implementation contains bugs.
• There Python implementation does not have a user interface. 
• Python and Haskell implementations come with modules for Boolean Logic and Peano Arithmetic, but they do not yet come with a module for Set Theory.

Read More

Python-Based Introduction to Mathematical Proofs

Scroll down for video lectures

1. What is a Mathematical Proof?  

Mathematical proof is a method of discourse which allows a human being to: 

• discover new mathematical knowledge,
• analyze existing mathematical knowledge,
• verify truthfulness of a piece of mathematical knowledge. 

The ability to construct a mathematical proof is part of human nature. It is closely related to the ability to form thoughts and reason.

Mathematical knowledge is knowledge of abstract principles about our universe. As such, it requires use of symbols to represent entities that are inherently abstract. For example, the symbol 2 may represent 2 apples or 2 pears. The number 2 is an abstract entity, since it is not confined to any of these concrete representations. 

Mathematics functions at different levels of abstraction too. For instance, we may write a symbol, such as n, to represent any number. In one case we could have n = 2, and in another case we could have n = 3. This is a second layer of abstraction compared to the layer of each specific number, such as number 2. Symbols representing abstract entities form basic ingredients of mathematical proof. The most complex parts of mathematical proofs deal with manipulations of these symbols, which sometimes may take an extremely long time. To optimize a proof, it is important to understand its most fundamental components. The aim of these lectures is to provide an exposition of these fundamental components. 

Activity. Get Python IDE, if you do not already have one: there are many available, Spyder is recommended (very easy to install). Then, get the file sofia.py, which can be obtained from https://github.com/ZurabJanelidze/sofia. Save sofia.py to the runtime directory of your Python IDE. To test that you have done it correctly, create a separate file named something.py, copy-paste the following code in that file, and run the file with your Python IDE:

import sofia

sofia.help()

Read More