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

Question

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

The axioms start with the mereological. For example,

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!

Answer 1

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.

Answer 2

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.