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.
Thanks!
EDIT :-
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!
Since no replies are forthcoming, I have posted this question on Theoretical Computer Science. I'm accepting this 'answer' to close the question here.