I have thought for a long time that it would be nice to have a high-level proof language with a prover that would compile that to an easy to verify and still readable low level language. A good candidate for the low-level part would be Metamath. I have recently found out about Russel – a high-level proof language created by Dmitri Yurievich Vlasov that compiles to (a simplified version of) Metamath. The Russell project on Sourceforge was last updated in February 2011, so it seems to be unused and abandoned. There is a paper (in Russian) that describes Russell. Unfortunately I don’t have access to the journal where it was published.

I downloaded the tar file and played a bit with the contents. The amount of work that went to the Russell project is staggering: almost 60000 lines of GPL licensed C++ code (very nicely written, btw) and 3800 lines of shell scripts. The scripts mostly do tests described on the Russell page. The compression test in particular is very interesting – it decompiles Metamath proofs to Russel and then tries to reduce them to the minimal number of steps from which the full Metamath proof can be restored with the prover. I run the compression test on the full Metamath database (included in the Russel’s distribution) with the recommended parameter N=300 (meaning that one in 300 proofs will be compressed). The results were not that amazing – out of 40 proofs for which the compression was attempted, only in two cases the prover managed to reduce the number of steps. In one case the length of the proof was reduced from 8 to 7 steps and in the other case from 12 to 4.

For the second case the original decompiled theorem looks like this:

theorem eqfnfvf2 (var x : set , var y : set , var A : class , var F : class , var G : class ) { hyp 1 : wff = |- ( ( y ∈ F ) → ∀ x ( y ∈ F ) ) ; hyp 2 : wff = |- ( ( y ∈ G ) → ∀ x ( y ∈ G ) ) ; ----------------- prop : wff = |- ( ( ( F 𝐅𝐧 A ) ∧ ( G 𝐅𝐧 A ) ) → ( ( F = G ) ↔ ∀ x ∈ A ( ( F ` x ) = ( G ` x ) ) ) ) ; } proof /* [22-Mar-2009] */ /* [29-Jan-2004] */ { var z : set ; step 1 : wff = theorem eqfnfv2 () |- ( ( ( F 𝐅𝐧 A ) ∧ ( G 𝐅𝐧 A ) ) → ( ( F = G ) ↔ ∀ z ∈ A ( ( F ` z ) = ( G ` z ) ) ) ) ; step 2 : wff = axiom ax-17 () |- ( ( y ∈ z ) → ∀ x ( y ∈ z ) ) ; step 3 : wff = theorem hbfv (hyp 1, step 2) |- ( ( y ∈ ( F ` z ) ) → ∀ x ( y ∈ ( F ` z ) ) ) ; step 4 : wff = axiom ax-17 () |- ( ( y ∈ z ) → ∀ x ( y ∈ z ) ) ; step 5 : wff = theorem hbfv (hyp 2, step 4) |- ( ( y ∈ ( G ` z ) ) → ∀ x ( y ∈ ( G ` z ) ) ) ; step 6 : wff = theorem hbeq (step 3, step 5) |- ( ( ( F ` z ) = ( G ` z ) ) → ∀ x ( ( F ` z ) = ( G ` z ) ) ) ; step 7 : wff = axiom ax-17 () |- ( ( ( F ` x ) = ( G ` x ) ) → ∀ z ( ( F ` x ) = ( G ` x ) ) ) ; step 8 : wff = theorem fveq2 () |- ( ( z = x ) → ( ( F ` z ) = ( F ` x ) ) ) ; step 9 : wff = theorem fveq2 () |- ( ( z = x ) → ( ( G ` z ) = ( G ` x ) ) ) ; step 10 : wff = theorem eqeq12d (step 8, step 9) |- ( ( z = x ) → ( ( ( F ` z ) = ( G ` z ) ) ↔ ( ( F ` x ) = ( G ` x ) ) ) ) ; step 11 : wff = theorem cbvral (step 6, step 7, step 10) |- ( ∀ z ∈ A ( ( F ` z ) = ( G ` z ) ) ↔ ∀ x ∈ A ( ( F ` x ) = ( G ` x ) ) ) ; step 12 : wff = theorem syl6bb (step 1, step 11) |- ( ( ( F 𝐅𝐧 A ) ∧ ( G 𝐅𝐧 A ) ) → ( ( F = G ) ↔ ∀ x ∈ A ( ( F ` x ) = ( G ` x ) ) ) ) ; qed prop = step 12 ; }

This gives some idea on the syntax of the Russell language. I would say it is very readable, although it is funny how it resembles C++. Unfortunately the distribution does not provide any sample of human-written Russel code or tutorial on the syntax of the language. The original proof syntax is somewhat similar to what one gets from the SHOW STATEMENT and SHOW PROOF command in Metamath.

MM> SHOW STATEMENT eqfnfvf2 $d x A $. $d y F $. $d y G $. $d x y $. 13784 eqfnfvf2.1 $e |- ( y e. F -> A. x y e. F ) $. 13785 eqfnfvf2.2 $e |- ( y e. G -> A. x y e. G ) $. 13786 eqfnfvf2 $p |- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) ) $= ... $. MM> SHOW PROOF eqfnfvf2 39 syl6bb.1=eqfnfv2 $p |- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. z e. A ( F ` z ) = ( G ` z ) ) ) 77 hbfv.1=eqfnfvf2.1 $e |- ( y e. F -> A. x y e. F ) 84 hbfv.2=ax-17 $a |- ( y e. z -> A. x y e. z ) 85 hbeq.1=hbfv $p |- ( y e. ( F ` z ) -> A. x y e. ( F ` z ) ) 91 hbfv.1=eqfnfvf2.2 $e |- ( y e. G -> A. x y e. G ) 98 hbfv.2=ax-17 $a |- ( y e. z -> A. x y e. z ) 99 hbeq.2=hbfv $p |- ( y e. ( G ` z ) -> A. x y e. ( G ` z ) ) 100 cbvral.1=hbeq $p |- ( ( F ` z ) = ( G ` z ) -> A. x ( F ` z ) = ( G ` z ) ) 111 cbvral.2=ax-17 $a |- ( ( F ` x ) = ( G ` x ) -> A. z ( F ` x ) = ( G ` x ) ) 138 eqeq12d.1=fveq2 $p |- ( z = x -> ( F ` z ) = ( F ` x ) ) 144 eqeq12d.2=fveq2 $p |- ( z = x -> ( G ` z ) = ( G ` x ) ) 145 cbvral.3=eqeq12d $p |- ( z = x -> ( ( F ` z ) = ( G ` z ) <-> ( F ` x ) = ( G ` x ) ) ) 146 syl6bb.2=cbvral $p |- ( A. z e. A ( F ` z ) = ( G ` z ) <-> A. x e. A ( F ` x ) = ( G ` x ) ) 147 eqfnfvf2=syl6bb $p |- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) )

After the compression the proof is as follows:

problem eqfnfvf2 (var x : set, var y : set, var A : class, var F : class, var G : class) { hyp 1 : wff = |- ( ( y ∈ F ) → ∀ x ( y ∈ F ) ) ; hyp 2 : wff = |- ( ( y ∈ G ) → ∀ x ( y ∈ G ) ) ; ----------------- prop : wff = |- ( ( ( F 𝐅𝐧 A ) ∧ ( G 𝐅𝐧 A ) ) → ( ( F = G ) ↔ ∀ x ∈ A ( ( F ` x ) = ( G ` x ) ) ) ) ; } proof /* [22-Mar-2009] */ /* [29-Jan-2004] */ { var z : set; step 1 : wff = ? |- ( ( z = x ) → ( ( F ` z ) = ( F ` x ) ) ) ; step 2 : wff = ? |- ( ( z = x ) → ( ( G ` z ) = ( G ` x ) ) ) ; step 3 : wff = ? |- ( ( z = x ) → ( ( ( F ` z ) = ( G ` z ) ) ↔ ( ( F ` x ) = ( G ` x ) ) ) ) ; step 4 : wff = ? |- ( ( ( F 𝐅𝐧 A ) ∧ ( G 𝐅𝐧 A ) ) → ( ( F = G ) ↔ ∀ x ∈ A ( ( F ` x ) = ( G ` x ) ) ) ) ; qed prop 1 = step 4 ; }

One can see two differences – the keyword “problem” is used instead of “theorem” and the lack of theorem references in the proof steps. My understanding is that the prover can find the correct references and reconstruct the complete 12 steps Metamath proof from just this sequence of four assertions. That’s very good, but in practice such approach seldom works well as evidenced by the compression statistics. In Isar this works (from the user perspective, I have no idea what happens internally) somewhat differently: there is a certain subset of theorems that are “added to the simplifier” and may be considered by user as common knowledge. To justify a step in a proof the user must reference only the theorems that are needed but are not in the simplifier. So for every step there is a different set of assertions that are used when searching for the proof. This set consists of the theorems in the simplifier, additional references provided by the proof author for this step and the hypotheses of the proof step, that must be either previously proven steps or come from the hypotheses of the theorem. Maybe defining such dynamic proof search space for each proof step is possible in Russell, I dont’ know.

Another feature that in my opinion is important for a formal proof language but seems to be missing in Russell is the structuring of proof. The structure of the Russel proof is linear without the possiblility of creating subproofs for intermediate results. Such feature is a good way to cope with overwhelming amount of detail that is typical for formal proofs and allows a reader to set the amount of detail she wants to be shown by the presentation layer. Again, maybe this is possible in Russel, but there is no example of such syntax in the automatically generated Russell code I looked at.

Judging from hits in search engines the Russell project is abandoned and unused. I think it deserves at least that more people know about it and maybe someone will base his idea or code on Russell.

Tags: formalized mathematics, Metamath, proof language, Russell

## Leave a Reply