# What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

I am in possession of a book, which, inspired by Russell's Principia Mathematica (PM) and logical positivism, attempts to formalize a specific domain by determining axioms and deducing theorems from them. In short, it attempts to do for its domain what PM attempted to do for mathematics. Like PM, it was written before automated theorem proving (ATP) was possible.

I am trying to represent these axioms in a modern ATP system, and attempt to deduce theorems, initially those deduced by the author (by hand). I have not used an ATP system before, and given the plethora of options (HOL, Coq, Isabelle, and many more), each with their strengths, weaknesses, and intended applications, it is proving difficult to decide which is appropriate for my specific purpose.

The formalism of the author closely mirrors PM. There are classes (sets?), classes of classes, and so on up to 6 levels of hierarchy. There is first order, and possibly higher order logic. Given the connection to PM, I initially investigated Metamath, since several theorems of PM have been proved in MetaMath by other people. However, Metamath is of course a proof verifier and not an ATP system.

Going through descriptions of various ATP systems, I see several characteristics, such as implementations of Church's type theory, constructive type theories, intuitionistic type theories, typed / untyped set theory, natural deduction, types of lambda calculi, polymorphism, recursive function theory, and the existence of equality (or not). In short, each system seems to implement a very different language, and must be appropriate for formalizing different things. I assume that existing libraries for formalizing mathematics are not relevant to my purpose.

Any advice regarding the characteristics I should seek in choosing an ATP, or any other advice you may have after reading this question, would be much appreciated. For reference, here is a sample page from the book. Unfortunately, like PM, it is in Peano-Russell notation. The book -

"The Axiomatic Method in Biology" (1937), J.H. Woodger, A. Tarski, W.F. Floyd

1.1.2 $$x$$ is the sum of $$\alpha$$ if $$\alpha$$ is contained in the parts of $$x$$, and if when $$y$$ is any part of $$x$$ there is always a $$z$$ belonging to $$\alpha$$ having parts in common with the parts of $$y$$:

$$S{ = }_{ Df }\hat { x } \hat { \alpha } \{ \alpha \subset \vec { { P }^{ ‘ } } x:.(y):yPx.\supset .(\exists z).z\in \alpha .\vec { { P }^{ ‘ } } y\cap \vec { { P }^{ ‘ } } z\neq \Lambda \}$$

Again, note that this is Peano-Russell notation (the notation of Principia).

Later axioms have biological content, such as,

7.4.2 When gametes of two members of a Mendelian class unite in pairs to form zygotes, the probability of any given pair uniting is equal to that of the other pair.

This, from what I understand, was a postulate of Mendelian genetics.

I omit the notation for this because it is three lines long, and builds upon previously defined content.

Example of a theorem - This apparently carries a meaningful interpretation in Mendelian genetics, which, not being a historian of biology, I do not understand. In the book, it was deduced by hand.

Thanks!

• Is there historic interest in exactly following the book, or could you just extract the gist of it (the basic setup and the axioms) and formalize the theory in an available modern system? Jul 3 '14 at 14:49
• @andrej: Yes, extracting and formalizing the gist in a modern system is my aim. It would not be necessary to deduce every theorem deduced by hand in the book. Rather, it would be cool to deduce theorems not in the book, from the axioms in the book. Jul 3 '14 at 15:05
• In that case you should understand the text and then do it in whatever proof assistant and/or theorem prover seems to best fit your purpose. Jul 3 '14 at 15:08

Principia Mathematica was a largely response to the various paradoxes discovered in mathematical logic at the turn of the 20th century. However the work itself, which has often been obliquely praised as an 'unreadable masterpiece' is somewhat clumsy and more modern foundations have been crafted. To describe most of mathematics, you have several choices: category theory is one, type theory has been popular in some projects as an extension of the lambda calculus, but the best understood and most foundational is probably set theory.

Set theory has several different formulations; Zermelo Frankel set theory with the axiom of choice is the most orthodox, lovingly refered to as $\sf ZFC$ by set theory enthusiasts. Tarski-Grothendiek set theory is another that is largely similar to $\sf\ ZFC$ that includes Tarski's axiom for reasoning about large categories. These are interesting for verification, but somewhat more difficult for automated theorem proving because the axiom schema of replacement admits an infinite number of axioms that represent a challenge for implementation. While these foundations are perfectly reasonable for proof verification systems like Mizar for Tarski-Grothendiek set theory and Metamath for $\sf ZFC$, for an actual theorem proving system, it would be nice to have finite axiomatization.

The foundation that is probably most appropriate for that is Von Neumann–Bernays–Gödel set theory, or $\sf NBG$, which admits finite axiomatization by being a two sorted theory that has an ontology of proper classes as well as sets. Further, it's been proven that $\sf NBG$ is a conservative extension of $\sf ZFC$, so that any theorem of $\sf NBG$ is a theorem of $\sf ZFC$. The reason that this theory is the most appropriate for automated reasoning in my opinion is its expressible in first order logic, which admits an effective, sound and complete proof calculus, and finite axiomatization means it can be used with first order resolution which gives us the tidy result: If a statement is decidable, a proof will eventually be found.

Propositional logic isn't expressive enough, and higher order logic, while much more expressive, doesn't admit a effective, sound and complete proof calculus. First order logic with set theory allows you to represent and map higher order logical theories, so for foundations that's the sweet spot... except for the possibility of undecidable statements (thanks to Gödel.) which is why first order theories of sufficient quantifier rank are often described as semi-decidable.

Art Quaife did some work on this in: Automated Development of Fundamental Mathematical Theories, where he implemented $\sf NBG$ in first order logic in clausal form so that it could be used by a resolution based theorem prover (Otter) and an exellent reference for tackling the foundations for this sort of work is Elliott Mendelson's Introduction to Mathematical Logic.

Now modern proof assistants are often less concerned with foundations from the paradigm of Principia Mathematia and are more useful for theorem proving for everyday work, and so they have some support for fragments of higher order logic, SAT/SMT solving, type theories, and other more informal and less foundational approaches. But if you're trying do do something like Principia Mathematica a first order resolution theorem prover with a finitely axiomatizable first order set theory is ideal.

For some examples of how automated theorem provers attack problems from these foundations, the Thousands of Problems for Theorem Provers (TPTP) site has a nice number of problems, and you'll note that many of the foundational problems in number theory are founded in $\sf NBG$ set theory. If you have the time, check out NUM006-1.p on their site: the Goldbach conjecture. You can try running it, and if its decidable, a proof will eventually be found.

The theorems in your book will almost certainly be theorems of $\sf NBG$ given that they are written in the language of set theory. The axioms of genetics in that book will almost certainly be represented as definitions on set theoretical predicates, much the way that Peano arithmetic is represented in $\sf NBG$ as definitions of predicates. From there you follow the resolution procedure in any ATP. Pick a statement you want to prove, negate it, convert to Skolem normal form, then to clausal form, and follow the resolution. When you find the empty clause, you have found a contradiction, proving the statement.

The task you have at hand if you want to attempt to define the theory in terms of set theory, is finding the relational predicate definitions that are separate from set theory, that will allow you to make the predicates in terms of set theory. Again, an example of this is how we define Peano arithmetic in set theory, which by itself has no definitions of numbers, addition, multiplication, or even equality. As an example of a set theoretical definition of a relation like equality, we can define it in terms of membership as such:

$\forall$xy($\forall$z(z $\in$ x $\leftrightarrow$ z $\in$ y) $\leftrightarrow$ x = y)

A fair bit of warning: the learning curve for this is indeed very steep. If you are intent on pursuing this, you may find yourself several years in before grasping the full problem, as was my experience. You may want to examine the theory from a less foundational approach before taking on the enormous task of embedding it in a foundational language for everything. You don't, after all, necessarily need to reason about uncountable sets of genes mixing.

• Many thanks for this detailed and elucidating answer! A few questions: 1. Wikipedia states that 'The axiom schema of replacement is not necessary for the proofs of most theorems of ordinary mathematics.', and that it was not one of Z's original axioms (it was added by F). Is it possible that my theorems could be provable without it, hence negating the need for NBG? Of course, I suppose no automated theorem prover would allow use of {ZFC - axiom schema of replacement}, if that were even possible? Jul 10 '14 at 15:54
• 2. Given that first order logic + set theory is best for foundations, I assume that HOL/Isabelle/PVS/etc (all higher-order) are all overkill for my purpose? Also, everything based on type theory (Coq et al.) are not appropriate? Accordingly, the likes of Prover9/Vampire/SNARK would be appropriate? I have some prior experience with SNARK. It can handle many-sorted first order logic with equality, by resolution, but I'm not sure how to represent set theory in it. Jul 10 '14 at 16:17
• Automated theorem provers can use axiom schemas, but it makes implementation difficult. Prover9 doesn't support them. HOL, Isabelle, Coq all support first order set theory as far as I can remember, and are probably perfectly fine for your project. Even though you can embed other theories in NBG, it isn't absolutely necessary. We don't have to embed Peano arithmetic in NBG to prove things about numbers... but it does help to learn and understand logical structure. Jul 10 '14 at 17:35
• You can always embed your theory into set theory afterwards, by defining the predicates of the theory in terms of the membership predicate. I wouldn't worry about making your project absolutely foundational right away. It can be snapped in later. Jul 10 '14 at 17:38
• It appears then, that virtually any prover - even ones as different as Coq, HOL and Prover9 - may be used for my project. In such cases, what would be a smart decision strategy? I am unfamiliar with all but SNARK. The 'ideal' is discovery of new theorems in the axiom system provided. Jul 10 '14 at 17:40

Several points:

1. As far as I know, Principia Mathematica uses essentially a formalization of set theory using a typed first order logic. It would therefore be tempting to use a first-order automated theorem prover like Prover 9 or possibly ACL2 to formalize your statements. However, I am seeing several set-theoretic constructions (like $\in$, $\cap, \subset$) in there, which usually don't play very well with first order ATP.

2. Any modern interactive proof assistant will surely have the expressiveness to formalize and prove your statements, as Andrej has suggested. In fact, since there seem to be some statements including arithmetic, it would be wise to use a system like Isabelle, Coq or HOL which already have extensive theories to treat statements of arithmetic. My emphasis on modern is not a coincidence: great strides in usability have been made since Automath, and I honestly think you would be doing yourself a disservice by using anything that hasn't been actively developed since the 90's (if you could even get one to work!)

3. Finally, ITP and ATP have rather challenging learning curves, and you shouldn't expect to be able to enter these theorems into such a system as if you were writing a $\LaTeX$ proof. Expect severe frustration and lost time, especially in the first months (yes, months). You definitely need to work through some tutorials at first before getting to the main formalization.

• Thanks! This is the kind of general advice I was looking for. Marking this answer as accepted. I will probably have more specific / technical questions as I progress. Jul 8 '14 at 0:13
• Set theory is made for first order logic. You can reduce all of mathematics to a first order theory with just one predicate: membership. From there you can construct definitions of union, intersection, subset, proper subset, and other relations. Prover9 is entirely appropriate. Jul 9 '14 at 19:11
• In theory? Yes. In practice? If you define say, the natural numbers using set theory, a system like Prover9 wouldn't be able to prove the most basic statements like total ordering of $\mathbb{N}$. By nature, systems like set theory require a number of specific heuristics to be handled efficiently by ATP systems.
– cody
Jul 10 '14 at 16:09
• Prover9 uses set theoretical constructions of the natural numbers often. Check the number theory problems and number theory axioms in TPTP. They define number theory as definitions on set theory. The heuristics required by ATP for resolution theorem provers are just which clause to pick for the usable list when searching for the empty clause, and set theory isn't any special exception to that. Other theories are defined in set theory by relational predicates. Jul 10 '14 at 17:32