Por Clarence Protin (Universidade Aberta).
In this short talk we describe the Pylog software project and its application to Kelley-Morse set theory. Pylog is a minimalistic Python command-line based proof assistant and proof checker based on linearised natural deduction for first-order logic with equality and a comprehension operator.
First-order logic is extended with formula-variables to deal with propositional validities. Axiom schemes are implemented as additional rules.
The main feature of Pylog is that both the interface and the source-code are simple and transparent and easily understandable by the logician and formally-minded mathematician with only the most basic knowledge of Python. This is also useful to the programer who wishes to modify or develop Pylog or incorporate it into more advanced projects.
Pylog is based on the philosophy that (exhaustively) detailed natural deductions proofs (where the classical negation rule is added to the core intuitionistic rules and is used as desired or needed) are at least a step in the right direction for capturing how mathematicians go about writing proofs. The next step is to achieve a kind of micro-automatisation and condensation of the proof in the direction of greater conciseness and readibility, perhaps employing techniques similar to the "tactics" of Coq.
We describe our project of formalising Kelley-Morse set theory as found in the famous appendix of Kelley's General Topology (1955).
At present there is over ten thousand lines of proof covering over eighty theorems. We illustrate the Pylog command-line environment by proving a simple consequence of the axiom of regularity. We then give a description of the next stages of the PyLog project.
Finally we end with some short remarks on mainstream formal mathematics projects and the foundations of mathematics.
Zoom | Meeting ID: 837 8989 1971
