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 = 0. We contend that a good trade-of between two primary measures of the complexity of the representation, which are the number of unknowns and the degree of the polynomial , 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 version of Schröder's algebra of relations, specifically the 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.
For a long time (see, e.g., [
How complex is such a set of theorems? Two complexity measures associated with a Diophantine
representation (†), as well as trade-ofs between the two, are discussed in [4, p. 153 f.]:
Rank of Th: The minimum possible value of , the number of unknowns in a representation (†).
Order of Th: The minimum possible degree of with respect to the unknowns in (†).
Taken alone, the order can always be kept below 5—at the price, however, of a significant increase in
the rank (see [4, pp. 3–4]). Taken alone, the rank can always be kept below 11—though at the cost of an
order exceeding 1044 (see [5, p. 552]); ways of balancing the two measures emerge, in fact, from the
study [
A criterion for best associating a polynomial with a theory Th is that the construction of should be transparent, in the sense that it closely mirrors the process of deriving a theorem from the axioms of Th in a specific formal system. This criterion may appear somewhat elusive, but it is well illustrated https://users.dimi.uniud.it/~andrea.formisano/ (A. Formisano); https://sites.units.it/eomodeo/index.html/ (E. G. Omodeo)
CEUR
ceur-ws.org
by the manner in which Merlin Carl and Boris Z. Moroz [
This paper presents an emulation, by the authors, of the work of Carl and Moroz. However, instead
of using first-order logic, the formalism underlying the axiomatization of NBG adopts a modernized
version of Ernst Schröder’s algebra of (dyadic) relations, specifically the equational logic ℒ× , extensively
discussed by Alfred Tarski and Steven Givant in [
While only a glimpse of the novel axiomatization of NBG based on ℒ× is ofered, the article reports on the initial stages of experimentation with these axioms, assisted by the theorem prover Vampire (cf. https://vprover.github.io/).
We begin by stating our goal in general terms. Our goal is to encode a formalized theory using Diophantine equations. The theory is based on a symbolic language and consists of the following components: 1. A finite number of logical axiom schemata. 2. A finite number of derivation rules, each applying to at most two premises.
Together with the language, the first two components define the underlying logical calculus, while the third specifies the theory itself.
Let F be the set of all statements of the formal language, and let Th ⊆ F be the set of provable theorems of the theory. We assume the availability of an efective bijection : F → N that assigns a unique natural number to each statement.
By the Davis-Putnam-Robinson-Matiyasevich theorem, every recursively enumerable set is Diophantine. Since Th is recursively enumerable, there exists a Diophantine polynomial := (; 1, . . . , ) such that the equation = 0 has solutions in the set N of natural numbers if and only if the parameter belongs to [Th]. Our objective is to explicitly construct such a polynomial .
Although general techniques exist for this purpose, our construction will provide deeper insight into the number-theoretic devices underlying the Diophantine representation of Th.
We proceed with the following subtasks:1 • Constructing a Diophantine polynomial ∈ Z[; ⃗1], where ⃗1 = (1, . . . , 1 ), that admits solutions in N1 if and only if is the number corresponding to one of the logical axioms. • Constructing a Diophantine polynomial ∈ Z[, , ; ⃗2], where ⃗2 = (1, . . . , 2 ), that admits solutions in N2 if and only if − 1() is obtainable from − 1() and − 1() by means of one of the derivation rules. • Constructing a Diophantine polynomial ∈ Z[; ⃗3], where ⃗3 = (1, . . . , 3 ), that admits solutions in N3 if and only if is the number corresponding to one of the adopted proper axioms. We will ensure that these three polynomials take only nonnegative integer values. This does not restrict generality, as the property or relation over N represented by a Diophantine parametric polynomial remains unchanged when the polynomial is squared. To smooth the presentation, we also impose that 1For clarity, when representing a polynomial, we sometimes separate variables using ‘;’ to distinguish those that act as parameters from those that are viewed (even if only implicitly) as existentially bounded variables. 1 = 2 = 3 , and denote this common value as : in fact, we can multiply any Diophantine polynomial not involving a variable by the monomial + 1, without afecting the relation it represents.
A proof is a nonempty list of statements each of which is either an axiom or is derived, thanks to a derivation rule, from statements which precede it in the list. We can hence say: ∈ Th ⇐⇒
(∃ ∈ N) (∃ 0, 1, . . . , ∈ F) such that • = and • for each ℎ ⩽ , one of the the following holds: – ℎ is a logical axiom, i.e., there exists ⃗ ∈ N such that ︀( (ℎ), ⃗︀) = 0; – there exist , < ℎ and ⃗ ∈ N such that ℎ is derivable in a single step from and , i.e., ︀( (ℎ), (), ( ), ⃗︀) = 0; – ℎ is a proper axiom, i.e., there exists ⃗ ∈ N such that ︀( (ℎ), ⃗︀) = 0.
Proposition 1. Define the demonstrative polynomial of the theory as: (, , ; ⃗) := (; ⃗) · (; ⃗) · (, , ; ⃗) .
[Th] = {︁ ∈ N ⃒⃒ (∃ , 0, 1, . . . , ∈ N) (∀ ℎ ⩽ ) (∃ , , ′, ′ ∈ N) (∃ ⃗ ∈ N) (︁ 0 = (ℎ, , , ⃗) + (ℎ + + ) · (︀ ( + ′ + 1 − ℎ)2 + ( + ′ + 1 − ℎ)2)︀ + ( − )2 )︁}︁ .
Each of the three polynomials composing represents an alternative condition: (, ⃗) = 0 implies that encodes a logical axiom; (, ⃗) = 0 implies that encodes a proper axiom; and (, , , ⃗) = 0 implies that () is directly obtainable from () and () via a derivation rule. Since we are interested in the locus of zeros, multiplying these polynomials together imposes that at least one of the conditions must hold. Similarly, we often sum squares of polynomials to enforce that multiple conditions are jointly satisfied. For example, ( + ′ + 1 − ℎ)2 + ( + ′ + 1 − ℎ)2 vanishes only when < ℎ and < ℎ; ℎ + + vanishes only if ℎ = 0, in which case we want = = 0; and ( − )2 vanishes precisely when the final statement coincides with the theorem we are checking for.
Remark 1. Note that when ℎ = = = 0, then ℎ = = . In this case, 0 is typically an axiom, since in most formal systems no derivation rule allows deriving a statement from itself. In the calculus ℒ× to be discussed later, this situation may arise but poses no problem: it leads to having 0 of the form = , which is a valid scheme. ⊣
We can encode a finite-length list of natural numbers using two numbers, ℓ and , via the Chinese
Remainder Theorem (see, e.g., [4, pp. 200–201]), as embedded in a technique due to [
mod 1 + · (ℎ + 1) and ℎ < 1 + · (ℎ + 1) , (∃ ∈ N)[ (ℓ − ℎ) = (1 + · (ℎ + 1)) · & ℎ ⩽ · (ℎ + 1) ] .
Accordingly, we can rewrite the specification of [Th] as follows: [Th] = {︁ ⃒⃒ ∃ , ℓ, ∀ ℎ ⩽ ∃ , , ′, ′∃1, 2, 3 ∃ ⃗ ∈ N ∃ 1, 2, 3, 4, 1, . . . , 4 ︁( 0 = (︀ (1 + 1 − (ℎ + 1))2 + (ℓ − 1 − 1((ℎ + 1) + 1))2 + (2 + 2 − ( + 1))2+ (ℓ − 2 − 2(( + 1) + 1))2 + (3 + 3 − ( + 1))2 + (ℓ − 3 − 3(( + 1) + 1))2+ ( + 4 − ( + 1))2 + (ℓ − − 4(( + 1) + 1))2+ (1, 2, 3, ⃗) + (ℎ + + )(( + ′ + 1 − ℎ)2 + ( + ′ + 1 − ℎ)2))︀ ︁)}︁ .
This can be considered a valid expression in any theory formulated in a formal language with an
arbitrary set of axioms and derivation rules involving at most two premises. To translate such an
expression into a purely Diophantine one, we can use various techniques of eliminating the bounded
universal quantifier. Here we follow the one from [
The number of variables used for the elimination is ( + 1)( + 1) + + 1, where • = + 15 is the number of existentially quantified variables after the bounded universal quantification (recall = max(1, 2, 3)), • is the number of variables present in the polynomial that expresses factorial, • is the number of variables present in the polynomial that expresses the product ∏︀ =1(1 + ).
The resulting polynomial has the maximum degree among the degree of Th and the degrees of the polynomials needed to perform the translation of factorial and the product ∏︀ =1(1 + ). All this is immediately deducible by looking at [12, pp. 153–154].
We do not make these constants explicit because they can always be improved through more refined Diophantine formulations. Here we follow the theorems in [12, pp. 144–149], from which = 55 and = 115.
The goal of this article is to find a polynomial that represents the class theory NBG. To do so, we will express the theory in algebraic (relational) form.
Our work follows the line of preceding work on the same theory, as formulated in first-order predicate
calculus by [
Operation Polynomial
Polynomial Polynomial
Polynomial
Value
Value Polynomial Th
[
Table 1 presents a brief summary of the diferences in expressive economy between our approach and
that of [
Let deg() denote the degree of a generic polynomial . Observe that deg() ⩽ deg( · · ). Here, the inequality hints that sometimes, as we will do in the following section, it is possible to combine these three polynomials in a less expensive way than by direct multiplication. This inequality suggests that, as we will demonstrate in the following section, it is sometimes possible to combine these three polynomials more eficiently than by direct multiplication.
We can now proceed to show how to encode logical axioms, proper axioms, and derivation rules.
We briefly recall the syntax of the relational language, which we denote by ℒ× . For further details, the
reader may consult the standard reference [
The alphabet is as follows: Definition 3.1.
The alphabet of ℒ× consists of: • Two identity symbols, one for relations, one for predicates {, =} • Two binary operators, union and composition {∪, ∘} • Two unary operators, reflection and complement {⌣, ¯} • The membership symbol { } • Parentheses {(, )} Semantically, is interpreted as a non-empty two-argument relation.
We define, inductively, the formation rules of predicates: Definition 3.2.
The set of predicates is formed as follows: • , are predicates, • If , are predicates, then ∪ , ∘ , ⌣, ¯ are predicates.
However, the ultimate objects of our relational calculus are not predicates but equalities. Definition 3.3. Let , ∈ . An equality is an expression of the form = . We denote by the set of such equalities.
Hence, for the language ℒ× , formulas F are equalities .
Since our work concerns exclusively syntactic aspects of the language (in particular, the notion of derivation), there is no need to define the semantic of ℒ× .
The logical axioms are reported in section 3.2 and the notion of proof in Section 3.4. The formulation of the proper axioms requires constructs that go beyond the scope of this article and will be presented in a diferent work.
We can proceed to number the formulas of the language. We take this idea from Julia Robinson [
First, we give the definition of Cantor’s bijection in Diophantine form: Definition 3.4.
c(, ) = :=
2 = ( + )( + + 1) + 2
The definition of proceeds in two steps, the first being inductive: Definition 3.5.
Define inductively a numbering ′ of the formulas 0, 1, . . . : • 0 = , i.e. ′( ) = 0, • 1 = , • 4(+1) = ∪ with = c(, ), • 4(+1)+1 = ∘ with = c(, ), • 4+2 = ¯, • 4+3 = ⌣.
The map : → N is defined as
( = ) = c(, ).
We emphasize that among the many possible bijections between and N, we have chosen one that allows us to immediately reconstruct the structure of the formula it represents from a given number. 3.2. Diophantine representation of axiomatic relational laws We present, without delay, the logical axioms: 1. ∪ = ∪
2. ∪ ( ∪ ) = ( ∪ ) ∪ 3. ∪ ∪ ¯ ∪ = 4. ∘ ( ∘ ) = ( ∘ ) ∘ 5. ( ∪ ) ∘ = ( ∘ ) ∪ ( ∘ ) 6. ∘ = 7. ⌣⌣ = 8. ( ∪ )⌣ = ⌣ ∪ ⌣ 9. ( ∘ )⌣ = ⌣ ∘ ⌣ 10. ( ⌣ ∘ ∘ ) ∪ =
(, , , 1, . . . , 5, 1, . . . , 9) = 2( − 1)2+ (21 − 2c(, ))2 + (22 − 2c(, ))2+ (23 − 2c(, ))2 + (24 − 2c(4(1 + 1) + , ))2+ (25 − 2c(, 4(3 + 1) + ))2 + +(21 − 2c(4 + 2, ))2+ (22 − 2c(4(1 + 1), ))2 + (23 − 2c(, ))2+ (24 − 2c(4(3 + 1) + 1, 4(3 + 1) + 1))2 + (25 − 2c(, 1))2+ (26 − 2c(4 + 3, 4(4(1 + 1) + 1) + 2))2 + (27 − c(4(6 + 1) + 1, 4 + 2))2+ (28 − 2c(16(2 + 1) + 2, 16(1 + 1) + 2))2 + (29 − 2c(4 + 3, 4 + 3))2 and we use these variables in the following polynomials: 1* = 2 − 2c(4(1 + 1), 4(2 + 1)) 2*,4 = 2 − 2c(4(4 + 1) + , 4(5 + 1) + ) 3* = 2 − 2c(48 + 2, ) 5* = 2 − 2c(4(2 + 1) + 1, 4(4 + 1)) 6* = 2 − 2c(4(5 + 1) + 1, ) 7* = 2 − 2c(4(4 + 3) + 3, ) 8*,9 = 2 − 2c(4(4(1 + 1) + ) + 3, 4(9 + 1) + ) 1*0 = 2 − 2c(4(7 + 1), 4 + 2) Call × * the product of these, and define × = + × * 2. We have deg(× * ) = 2 · 8 = 16, deg(× ) = (2 · 8) · 2 = 32.
We can now state the following: Proposition 2. Let (, ⃗1) = × , with ⃗1 = (, , , 1, . . . , 5, 1, . . . , 9, ). Then, if ∈ is in one of the logical-axioms schemata, there exists ⃗1 ∈ N18 such that ( ( ), ⃗1) = 0.
Let us elaborate on the first axiom as an example. 1 is the pairing of , via c, 2 the pairing of
, via c. The operation 4(1 + 1) is precisely that given in the definition of ′ for ∪. Therefore, the
operation c(4(1 + 1), 4(2 + 1)) is exactly the operation performed in the definition of to represent
the equality of two unions with identical operands in reversed order.
3.3. Diophantine representation of NBG’s proper axioms
We must now perform the same operation for the polynomials of the proper axioms of our class theory.
We have chosen to use the axioms as formulated in [
Since there are no axiom schemata, the multi-image of each axiom via will be a single number.
Hence, we may refrain from explicitly writing out the individual axioms and thus the polynomial: Lemma 2. Let : N × Z → Z be a polynomial, and ∈ . Then
[ ] = { ∈ N | ∃ ∈ Z s.t. (, ) = − = 0} with ∈ N. Furthermore, if we let = ∏︀ ∈AXp , then
[] = { ∈ N | ∃ ∈ Z s.t. (, ) = 0}.
Note that in this lemma, the presence of the variable is purely accessory.
According to our formulation of the proper axioms, || = 15. Again, we have chosen to remain faithful to a more transparent idea of proof rather than forcing the degree or the number of variables to be as low as possible. Using appropriate operations, we could indeed have created a single ‘macroaxiom’ to obtain a polynomial of degree 1 instead of one of degree 30.
Compared to the axiomatization proposed by [
∏︁ )︁ 2 ∈AXp [AX] = { ∈ N | ∃⃗1 ∈ N18 s.t. AX(, ⃗1) = 0} and we have deg( ) = (16 + 15) · 2 = 62.
The polynomial encodes the fact that a demonstration step is a logical or a proper axiom. In this section, we codify, in Diophantine form, the notion of derivability in the relational calculus, recalled here: Definition 3.6. A family Θ of equalities is called a theory if it possesses the following closure properties: 0. The logical axioms belong to Θ. 1. When two equalities = and = belong to Θ, then = also belongs to Θ. 2. When , , are predicates and = belongs to Θ, the equalities ∪ = ∪ , ∘ = ∘ , ¯ = ¯, and ⌣ = ⌣ also belong to Θ.
Lemma 3. Let = and = be equalities in .
Given ℎ1 ∈ Z[, ′, ′′, , , ], then the equality = is derived from = and = by inference rule 1 if and only if with
Let
∃, , | ℎ1( ( = ), ( = ), ( = ), , , ) = 0 ℎ1(, ′, ′′, , , ) = (2′ − 2c(, ))2 + (2′′ − 2c(, ))2 + (2 − c(, ))2.
ℎ ∈ Z[, ′, , , , , ], = 2, . . . , 5 and ℎ ∈ Z[, ′, , ], = 6, 7, then for each of the four inference schemata of point 2, the following holds:
An equality with code = ( ) is derived by the th schema from = if and only if ∃, , , , | ℎ(, ( = ), , , , , ) = 0, = 2, 3
or ℎ(, ( = ), , ) = 0, = 4, 5 with ℎ defined as follows: ∪ = ∪ ℎ2(, ′, , , , , ) = (2′ − 2c(, ))2+ ∘ = ∘ ℎ3(, ′, , , , , ) = (2′ − 2c(, ))2+ (2 − 2c(, ))2 + (2 − 2c(, ))2 + (2 − 2c(4 + 4, 4 + 4))2 ⌣ = ⌣ = (2 − 2c(, ))2 + (2 − 2c(, ))2 + (2 − 2c(4 + 5, 4 + 5))2 ℎ4(, ′, , ) = (2′ − 2c(, ))2 + (2 − 2c(4 + 3, 4 + 3))2 ℎ5(, ′, , ) = (2′ − 2c(, ))2 + (2 − 2c(4 + 2, 4 + 2))2 Proof. Immediate by the bijectivity of , ′.
Proposition 4. Let
Taking care to keep variables and degree under control, we can summarize:
(, ′, ′′, ⃗3) = (2′ − 2c(, ))2 + (2 − 2c(, ))2 + (2 − 2c(, ))2 + (2 − )2+ (( − ′′)2 + ( − )2) (2 − 2c(4 + 4 + , 4 + 4 + ))2·
· (2 − 2c(4 + 2 + , 4 + 2 + ))2 with ⃗3 = (, , , , , ). An equality with code = ( ) is derived from the equality = (and = ) by the derivation rules if and only if
∃⃗3 ∈ N6 | (, ( = ), ( = ), ⃗3) = 0 and also deg() = 2 + 2 · 2 · 2 = 10.
Since and are positive, we simply multiply them to obtain , which then has degree 10 + 62 = 72.
Because we are multiplying, with an appropriate renaming of variables, we can reuse those of the polynomial that has more of them (in our case ) in the definition of the other. Hence, we have a total of 18 variables in .
The availability of an equational reformulation of an axiomatic set theory within Tarski-Givant relational calculus ofers an interesting approach to the mechanization of reasoning in Set Theory. The approach consists of two steps. The first step requires building a prover for the equational calculus on top of an existing first-order theorem prover. Subsequently, this equational prover will be used to automate equational set-reasoning in the axiomatic theory.
The feasibility of this path has been explored in [
In this section, we outline a similar approach for the case of NBG based on the state-of-the-art theorem prover Vampire.
The key to enable a first-order theorem prover to perform deductions in ℒ× is to consider relational equalities (e.g., the logical axioms of Section 3.2) as universally closed first-order sentences, where the predicates (namely, , , ) play the role of first-order variables.
We implemented this idea by developing a hierarchy of layers on top of a core group of first-order sentences reflecting the logical axioms of ℒ× .
Each level extends the syntax of calculus by introducing new constructs derived from the constructs of the levels below. Then, Vampire is used to prove, starting from definitions and laws proved at lower levels, a set of laws that characterize the new constructs. For example, at the bottom level Vampire easily proved a rich collection of lemmas on the primitive operators, namely, union (∪), composition (∘ ), complementation (¯), and inversion (⌣). At the next level we introduced the relational constants Ø, 1l and the constructs of intersection ( ∩ := ∪ ), diference ( ∖ := ∪ ), and Peircean sum ( † := ∘ ). Vampire quickly proved several laws involving these new constructs.
We recall below only some examples of the constructs introduced, and laws demonstrated, in the subsequent levels of the hierarchy.
Inclusion. A possible definition for the notion of inclusion of relations is:
⊆ := ∪ = 1l.
Among the laws proved in this layer we mention, monotonicity and transitivity of inclusion, the
so-called cycle laws and Dedekind law [
Functionality. The main derived constructs in this layer are a selector of the functional part of a relation:
fncPart ( ) := ∖ ( ∘ ) and a shorthand for functionality condition:
Fnc( ) := ⌣ ∘ ⊆ .
Totality. This layer introduces and a shorthand for totality of relations: fncPart ( )⌣ ∘ fncPart ( ) ⊆ , Fnc( ) ∧ Fnc() → Fnc( ∘ ) , Fnc( ) → ∘ ( ∩ ) = (( ∘ ) ∩ ( ∘ )).
Total( ) := ∘ 1l = 1l.
Among the related laws Vampire easily proved the implications:
Total( ) ∧ Total() → Total( ∘ ) , Total( ∘ ) → Total( ) ,
Total( ) , ∩ ⌣ = Ø → Total(︀ )︀ .
By developing the entire hierarchy of levels, Vampire managed to prove several hundreds laws, in most cases taking fractions of a second and never going beyond a few minutes for the most dificult proofs. 4.2. Benchmarks for assisted reasoning in the equational formalization of NBG At the top of the hierarchy described earlier, after specifying the (equational rendering of the) proper axioms of the theory of interest, one can exploit Vampire to obtain proofs of theory-specific theorems.
As mentioned in the previous section, the proof framework we are developing has achieved good results in proving several theorems of relational calculus.
Extending the framework to support automated theorem-proving in NBG involves the addition of
layers that introduce set-theoretic notions and include equational re-formulations of the proper axioms
of NBG. While the relational translation of the axiomatic system proposed by Harvey Friedmann in [
The system was preliminarily tested by obtaining some apparently simple proofs. For example, Vampire quickly obtained a proof of the equivalence of diferent formulations of the Extensionality axiom, or that from the Infinity axiom the existence of a set immediately follows (namely, that 1l ∘ ∘ 1l = 1l holds).
As future work, we intend to validate the approach based on the equational formulation of NBG and powered by the theorem prover Vampire by tackling some harder problems of increasing dificulty. The goals that will be the first object of this activity include automated proofs of the following claims: • An empty class exists (our formulation of NBG does not explicitly include the emptyset axiom) • For any given set there exists a class whose sole element is • Any class that is a singleton is a set • Any class that has exactly two elements is a set • There exists a universal class