Diophantine Modeling of Provability in Algebraic Logic

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.