It has long been established that the set Th of theorems in an axiomatic formal theory is recursively enumerable
(r.e.). Building upon the Davis-Putnam-Robinson-Matiyasevich theorem, which states that every r.e. set is
Diophantine, this paper explores the complexity of representing Th through a Diophantine equation D = 0.
We contend that a good trade-off between two primary measures of the complexity of the representation,
which are the number of unknowns and the degree of the polynomial D, should aim at the transparency of
the representation. Our work builds on a previous construction, notably that of M. Carl and B.Z. Moroz, who
have provided a Diophantine representation of the sentences provable in the Gödel-Bernays class theory (NBG)
within first-order predicate calculus. In contrast, our Diophantine representation of NBG relies on a modernized
version of Schröder’s algebra of relations, specifically the L× equational calculus proposed by A. Tarski and S.
Givant. Additionally, we replace NBG’s traditional axioms with an alternative axiomatization by H. Friedmann.
These changes reduce the complexity of the Diophantine representation of NBG’s provability, while maintaining
equivalence to more classical formalizations. While we provide only preliminary insights into this novel equational
axiomatization, we report on initial experiments with these axioms using the Vampire theorem prover.
