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 -
&quot;The Axiomatic Method in Biology&quot; (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!
Several points:


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