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
- 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.