key: cord-0046591-mh2hyd82
authors: Lampert, Timm; Nakano, Anderson
title: Deciding Simple Infinity Axiom Sets with One Binary Relation by Means of Superpostulates
date: 2020-05-30
journal: Automated Reasoning
DOI: 10.1007/978-3-030-51074-9_12
sha: fa68bbb2fead22a8d4944a60d32657150b263ebd
doc_id: 46591
cord_uid: mh2hyd82

Modern logic engines widely fail to decide axiom sets that are satisfiable only in an infinite domain. This paper specifies an algorithm that automatically generates a database of independent infinity axiom sets with fewer than 1000 characters. It starts with complete theories of pure first-order logic with only one binary relation (FOL[Formula: see text]) and generates further infinity axiom sets S of FOL[Formula: see text] with fewer than 1000 characters such that no other infinity axiom set with fewer than 1000 characters exists in the database that implies S. We call the generated infinity axiom sets S “superpostulates”. Any formula that is derivable from (satisfiable) superpostulates is also satisfiable. Thus far, we have generated a database with 2346 infinity superpostulates by running our algorithm. This paper ends by identifying three practical uses of the algorithmic generation of such a database: (i) for systematic investigations of infinity axiom sets, (ii) for deciding infinity axiom sets and (iii) for the development of saturation algorithms.

Modern logic engines for first-order formulas (FOL), such as Vampire, CVC4, Spass or i-Prover, are very powerful in proving theorems (or refutations) or in deciding formulas with finite models (counter-models). For formulas that have only infinite models, however, these engines widely fail. 1 One exception is 1 Exceptions include infinity axiom sets that can be decided by saturation, such as the theory of immediate successors as stated in FOL with identity (cf. (14) on p. 15). However, in regard to FOL without identity, infinity axiom sets are only rarely solved, and only a few of them are included in the Thousands of Problems for Theorem Provers (TPTP) library, namely, problems SYO635+1 to SYO638+1. Among these problems, only SYO638+1 can be solved by SPASS due to chaining rules, which directly apply to the transitivity axioms. Furthermore, Infinox decides the finite unsatisfiability of SY0638+1 only by virtue of the plain properties of the relation involved.

Infinox, which decides the finite unsatisfiability of some relevant TPTP problems due to specific model-theoretic principles (cf. [3] ). 2 In contrast to Infinox, we investigate how to generate hitherto unknown and intricate infinity axiom sets (superpostulates) of FOL R to make it possible to decide an infinite number of infinity axiom sets related to these superpostulates. No engine is currently able to solve most of the superpostulates we generate.

In this paper, we refer only to FOL R , i.e., FOL without function symbols, without identity and with only one binary relation. Based on Herbrand's reduction of FOL to dyadic FOL, Kalmar has proven that FOL R is a reduction class (cf. [7] ). Boolos, Jeffrey and Burgess have defined and proven the algorithm for reducing FOL to FOL R in modern terms (cf. [2] , Sect. 21.3). Börger, Grädel and Gurevich have specified prenex normal forms of FOL R -formulas with prenexes of the form ∀∃∀ (= [∀∃∀, (0, 1)]-class) or of the form ∀∀∀∃ (= [∀ 3 ∃, (0, 1)]-class) as the two minimal classes of FOL R with infinity axioms (cf. Theorem 6.5.4, p. 309) and have presented the following two examples for the two classes (cf. [1] , p. 307):

They also specify another formula with the prenex ∀∃∀ (cf. [1] , p. 33):

(1) and (3) are both derivable from (2) . Thus, to decide that the latter is satisfiable, it is sufficient to decide that the former are likewise satisfiable. This method of deciding infinity axioms can be extended by specifying infinity axioms that imply other infinity axioms.

However, prenex normal forms do not provide a syntax that is suitable for this task. Different prenex normal forms can be converted into each other by equivalence transformation. For example, formula (2) , which is a member of the minimal class [∀ 3 ∃, (0, 1)], can easily be converted into a member of the minimal class [∀∃∀, (0, 1)], as shown in Table 1 . 

(ii) ∀x¬Rxx ∧ ∀x∃uRxu ∧ ∀x∀y(¬Rxy ∨ ∀z(¬Ryz ∨ Rxz)) Miniscoping Rx3x5) )) Prenexing 2 A further exception with respect to the engines on the TPTP site is Decider. This engine is able to identify infinity axiom sets of pure FOL without identity due to the implementation of a strong saturation algorithm that is not based on resolution. However, the complexity of the implemented algorithm is exponential, and the Decider engine is not optimized for rapid decision making. Thus, it fails to decide complex formulas within reasonable time and memory limits.

Likewise, it may well be that a formula of the minimal class [∀∃∀, (0, 1)] can be converted into a formula of a decidable class, e.g., with prenexes starting with existential quantifiers followed by universal quantifiers (=∃ * ∀ * , (0, 1)]-class). Similarly, the distribution of bound variables in the matrix is not standardized in prenex normal forms. Thus, many equivalent variations are possible. Therefore, the syntax of prenex normal forms is not well suited for investigating the internal properties and relations of infinity axioms. This is why we do not refer to infinity axioms (and, thus, to prenex normal forms) in the following. Instead, we refer to the opposite of prenex normal forms, namely, anti-prenex normal forms, in which the scopes of quantifiers are minimized. We refer to infinity axiom sets in terms of sets of anti-prenex normal forms. To do so, we define primary formulas via negation normal forms (NNFs) as follows: Thus, lines (ii) and (iii) of Table 1 are conjunctions of three primary formulas, while lines (i) and (iv) do not contain primary formulas. Any first-order formula can be converted into a disjunction of conjunctions of primary formulas (=FOLDNF); cf. [8] for an algorithm for doing so. Since the satisfiability of a disjunction can be decided by deciding the satisfiability of each disjunct, we consider only conjunctions of primary formulas or, analogously, (finite) sets of axioms (= theories) in anti-prenex form.

An axiom set is a finite set of primary formulas.

From here on, we will express all axiom sets of FOL R in standardized notation. Example 1. In standardized notation, formula (2) is converted into the following infinity axiom set:

This axiom set was the example used by Hilbert and Bernays to motivate proof theory by showing that the consistency of (4) cannot be proven by finite interpretations ("Methode der Aufweisung"; cf. [6] , p. 10). The third axiom expresses transitivity.

Formula (3) is equivalent to the following infinity axiom set from [11] , p. 183:

Like (1), (3) and (5) are derivable from (4). The following infinity axiom set (6) is taken from [2] , p. 138:

Like (2) , this infinity axiom set is equivalent to (4) .

The formulas mentioned up to this point are examples of infinity axiom sets of FOL R given in the standard literature. They are all satisfiable by interpreting Rxy as x < y over Q. Thus, they are all derivable from the complete dense linear order (DLO) axiom set without endpoints. In the following sections, we will generate a system of DLO variants without identity, to which all of the mentioned standard examples belong. We use the term "system of formulas" to refer to a recursive set of formulas generated by rules that can be implemented by a computer program. Our investigation may serve as a case study for investigating systems of infinity axiom sets of FOL R .

Our goal is the automated generation of a system of consistent infinity axiom sets S of a limited length L such that no other infinity axiom sets S2 of length ≤L exist such that S2 implies S. We call these infinity axiom sets S "superpostulates". Superpostulates enable the reduction of a large number of infinity axiom sets to a small number of infinity axiom sets of limited length. The term and the general idea of studying systems of superpostulates originated in the work of Sheffer (cf. [12] ). Sheffer, however, neither published his work nor developed his logic project to a full extent. His student Langford made use of Sheffer's idea in [9] . Langford intended to prove that the axiom set for linear orderings is a complete superpostulate. Urquhart (cf. [14] , p. 44), however, objected to the correctness of his proof and showed how to correct it. Langford proved similar results for the theories of betweenness and cyclic order. All of his examples are equivalent to formulas of decidable classes without existential quantifiers and with identity, which have the finite model property (cf. [1] , Theorem 6.5.1, p. 307). To our knowledge, neither Langford nor Sheffer studied superpostulates in terms of infinity axiom sets.

The following sections investigate infinity axiom sets related to the complete DLO axiom set without endpoints. Section 2 introduces further terminology and specifies a superpostulate DLO R for FOL R , which is a DLO variant without identity and without endpoints from which all of the mentioned infinity axiom sets follow. After having specified a complete infinity axiom set, Sect. 3 specifies an infinite sequence of infinity axiom sets, each strictly implying the next and all implied by (5) . Section 4 then specifies a system of superpostulates based on DLO R ; Sect. 5 refers to a system THS R based on the complete theory of immediate successors without identity. Finally, we conclude by identifying several practical uses of our method of algorithmic generation of systems of superpostulates in Sect. 6.

We first introduce some terminology as a basis for defining the term superpostulate.

Remark 1. Throughout this paper, we consider FOL R . This means that an axiom set A is complete iff no FOL R -formula B is independent of A.

We measure the length of an axiom set by the number of characters it contains in standardized notation.

A of length ≤ L is L-complete in FOL R if for any FOL R -formula B of length ≤ L, either B or ¬B follows from A. Remark 2. Definition 7 implies that no formula B of length ≤ L exists such that A of length ≤ L is strictly implied by B if A is L-complete.

It is desirable to define superpostulates as complete (and not merely L-complete) theories. However, we abstain from doing so because we intend to define a practical algorithm for generating infinity axiom sets. The standard of preserving completeness, however, faces both practical and theoretical problems, as we will show in Sect. 4. Thus, we merely presume that the generation of a system of superpostulates is based on complete theories and aims for completeness relative to a length L of up to 1000 characters (cf. p. 11).

Any semi-decider is able to prove that a formula is implied by or inconsistent with another formula or finite axiom set. Since these are the only two options in the case of complete superpostulates, it is decidable whether a given formula is implied by a complete superpostulate. Furthermore, all (finite) infinity axiom sets that are implied by a set of infinity superpostulates are decidable.

From the following axiom set DLO R , all infinity axiom sets of the standard literature mentioned in Sect. 1 follow:

Axiom 1 (irreflexivity), Axioms 2 and 3 (no right endpoint and no left endpoint), Axiom 4 (transitivity) and Axiom 6 (density) are identical to axioms of DLO without endpoints. However, DLO also contains trichotomy, i.e., the axiom ∀x∀y(Rxy ∨Ryx∨x = y), which involves identity. The trichotomy axiom of DLO is replaced by Axiom 5 (transitivity of ¬R) in DLO R . Formula (7) contains all of the axioms of the infinity axiom set given in formula (4) . Additionally, Axioms 3, 5 and 6 are added to those in (4). These axioms are not essential for satisfiability in an infinite domain.

A is no longer an infinity axiom.

The set of the essential axioms plus the negation of an inessential axiom is also an infinity axiom set, but it is not necessarily a complete one.

In the following, we prove that (7) is a complete superpostulate by proving the relevant properties.

Proof. If (7) is satisfiable, then it is satisfiable only in an infinite domain; this is because it implies (4), which is known to be an infinity axiom set. Thus, it remains to be shown that (7) is satisfiable. This is done by providing the following model over Q for (7):

It can be proven that this interpretation is indeed a model by paraphrasing each axiom. We use the common forms of the transitivity axioms (Axiom 4 and Axiom 5) and the density axiom (Axiom 6) for convenience: Axiom 1 ∀x¬Rxx (Axiom 1) All rational numbers (r.n.) are no less than (<) themselves (irreflexivity of <) Axiom 2 ∀x 1 ∃y 1 Rx 1 y 1 (Axiom 2) For all r.n. x 1 , some r.n. y 1 exists such that x 1 < y 1 (no right endpoint) Axiom 3 ∀x 1 ∃y 1 Ry 1 x 1 (Axiom 3) For all r.n. x 1 , some r.n. y 1 exists such that y 1 < x 1 (no left endpoint)

(Axiom 6) For all r.n. x 1 and x 2 , if x 1 < x 2 , then there exists an r.n. y 1 such that x 1 < y 1 and y 1 < x 2 (density) Therefore, (7) is satisfiable; this is so only in an infinite domain, which means that (7) is an infinity axiom set.

Proof. This is ensured by systematically producing the following:

1. all possible axiom sets A from (7) with one axiom eliminated (case 1a) or with the conjunct in Axiom 6 eliminated (case 1b), 2. all possible axiom sets A with one disjunct in Axioms 4 to 6 eliminated (case 2), and 3. all possible axiom sets A obtained by (α) reducing the universal quantifiers in Axioms 4 to 6 and (β) replacing Axiom 2 and Axiom 3 with ∀x 1 Rx 1 x 1 or ∃y 1 Ry 1 y 1 (case 3).

In case 2 and case 3 (β), the resulting sets A and A have been proven to be inconsistent by Vampire in any arbitrary case; in case 3 (α), the resulting axioms in A have been proven to be redundant by Vampire. In case 1a, the results of eliminating Axiom 1 or Axiom 4 have been proven to be finite axiom sets by Vampire. Therefore, the resulting axiom sets are not equivalent. Axioms 2, 3, 5 and 6 are not redundant (and, thus, cannot be eliminated) because they can be proven to be independent axioms by replacing them with their negations, which, in turn, results in infinity axiom sets. This can be seen by referring to the following interpretations:

Axiom 1 Axiom 2 Axiom 3 Axiom 4 Axiom 5 Axiom 6

The conjunct in Axiom 6 is not redundant because eliminating it results in a redundant axiom, whereas Axiom 6 itself is not redundant.

Proof. We extend (7) by the following defining axiom of x 1 = x 2 :

The union of (7) and (8) is equivalent to DLO without endpoints (as proven by Vampire). Thus, DLO without endpoints is a conservative extension of (7) and, by conservativeness, (7) is complete if DLO is complete. 3 Since DLO without endpoints is known to be complete, (7) is also complete. We say that an infinity axiom set B is weaker than A if B is strictly implied by A, that is, A B, but B A does not hold. Before we consider how to generate further superpostulates, let us first consider the opposite: infinity axiom sets that are as weak as possible.

The set given in formula (5) is the weakest infinity axiom set mentioned in the standard literature. The following infinite axiom sets, however, strictly follow from (5):

Formula (9) strictly follows from (5), and (10), in turn, strictly follows from (9). We first prove that (10) is an infinity axiom. We then show that it can still be systematically weakened without losing the property of being an infinity axiom set.

Proof. We first show that there exists a denumerable model of (10) and then show that (10) has no finite model.

We assume the natural numbers as the domain and interpret Rxy as x < y. Then, it is true that for all natural numbers x 1 , there exists a number y 1 such that x 1 < y 1 and y 1 ≮ x 1 , and that for all x 2 , if x 2 < x 1 , then x 2 < y 1 . Thus, a denumerable model of (10) exists.

We prove that (10) has no finite model by contradiction. Suppose that there is a finite model M of (10), where the elements of its domain are listed as m 1 , . . . , m k . Let n 1 = m 1 . In the following, we consider how to satisfy the three conjuncts in the scope of ∀x 1 ∃y 1 . By the first conjunct, there must be some n in the domain such that (n 1 , n) is in (R). Let n 2 be the first element for which this is true. Thus, we have (n 1 , n 2 ) ∈ (R). By the second conjunct, we have that (n 2 , n 1 ) / ∈ (R). It follows that n 1 = n 2 is in (R). Again, by the first conjunct, there must be some n such that (n 2 , n). Let n 3 be the first element for which this is the case; thus, we have (n 2 , n 3 ) ∈ (R) and, by the second conjunct, (n 3 , n 2 ) / ∈ (R), and therefore, n 2 = n 3 . By the third conjunct, we have either (n 1 , n 2 ) / ∈ (R) or (n 1 , n 3 ) ∈ (R). Since we already have (n 1 , n 2 ) ∈ (R), the second of these statements, i.e., (n 1 , n 3 ) ∈ (R), must be true. Then, by the second conjunct, we have (n 3 , n 1 ) / ∈ (R). Thus, we also have n 1 = n 3 (in addition to n 2 = n 3 ) since we have (n 3 , n 1 ) / ∈ (R) and (n 1 , n 3 ) ∈ (R). Continuing in this manner, we obtain n 4 , which is different from all of n 1 , n 2 , and n 3 ; then, we obtain n 5 , which is different from n 1 to n 4 ; and so on. However, by the time we reach n k+1 , we will have exceeded the number of elements of the domain. Thus, our supposition that the domain of M is finite leads to a contradiction. Therefore, (10) has no finite model.

Formula (10) is a simple and weak infinity axiom that no TPTP engine is able to decide. 4

Proof. We consider the iterative derivation of strictly weaker axioms from (10) by applying the rule A B ∨ A (∨I), as shown in Table 2 . Table 2 . Infinity axioms implied by (10) No. Axiom Rule

Lines (ii), (iii), etc., follow from (10) with the application of nothing but ∨I, which is a valid derivation rule. Each result is, in turn, a primary formula. To verify that iteratively applying ∨I generates a sequence of weaker infinity axiom sets, one must determine how the proof of Theorem 4 still applies. Formula (10) allows one to directly conclude that n 1 = n 3 once n 1 = n 2 and n 2 = n 3 are established. Applying ∨I once (cf. line (ii)), however, allows one to conclude only that either (n 1 , n 3 ) ∈ (R) or (n 4 , n 2 ) / ∈ (R) (where n 4 is the element introduced by ∀x 3 , which cannot be presumed to be either identical to or different from n 1 , n 2 , or n 3 ). Due to the first two conjuncts, n 1 = n 3 follows from (n 1 , n 3 ) ∈ (R), and n 2 = n 4 follows from (n 4 , n 2 ) / ∈ (R). Considering further objects of the domain introduces further objects that must be different from all objects in one of the established alternative sets of objects. With each further application of ∨I, further alternative sets arise. Thus, each axiom resulting from ∨I establishes a wider range of objects that cannot be identical. Therefore, each application allows for less powerful inferences concerning the non-identity of the elements in pairs satisfying (R), and thus, each resulting axiom is strictly weaker. Nevertheless, the resulting axioms still necessitate that at least one of the newly considered objects (e.g., n 3 and n 4 in step 2 of the argument after n 1 = n 2 is established in step 1) in each step of the argument must be different from at least one of the already considered objects (e.g., n 1 and n 2 in step 1). Therefore, the resulting axioms still cannot be satisfied under the assumption of only a finite number of objects. Consequently, we generate an endless sequence of increasingly weaker infinity axioms.

There are many further infinite sequences of non-equivalent infinity axiom sets that are implied by (7) . They all can be proven to be satisfiable by proving that they follow from (7).

We are searching for a system of infinity superpostulates that is automatically generated by transformation rules from a complete theory such as (7) . The rules specified in this section are a starting point for the general project of generating systems of infinity superpostulates from a given complete axiom set. We do not claim that our third rule preserves completeness.

The following two rules yield structurally similar infinity axiom sets of FOL R . They trivially preserve the property of being a complete infinity axiom set in the case of FOL R : These rules do not necessarily yield new (non-equivalent) infinity axiom sets. Rule 1, for example, converts Axiom 4 of superpostulate (7) into Axiom 5 and vice versa. Rule 2 does not change Axiom 1, does convert Axiom 2 into Axiom 3 and vice versa, and yields equivalent axioms in the cases of Axioms 4 and 5.

In fact, applying these rules to our superpostulate (7) results in only one further complete superpostulate:

The crucial problem in considering systems of superpostulates is specifying rules beyond Rules 1 and 2. Replacing Axiom 2 or Axiom 3 with its negation results in a complete variant of DLO R with endpoints. 5 Thus, one might consider a rule that replaces axioms with their negations. However, the case in which completeness is preserved by simply replacing an axiom with its negation is an exceptional one. This is true only if one cannot replace an axiom A of a complete theory S with a strictly weaker axiom that is still independent of S without A. For example, there is no primary formula X that is strictly implied by ∀x 1 ∃y 1 Rx 1 y 1 (=Axiom 2) and is not implied by Axiom 1 and Axioms 3-6 of (7). The same does not hold, e.g., for Axiom 1. Therefore, simply replacing Axiom 1 of (7) with its negation does not preserve completeness since ∃y 1 ¬Ry 1 y 1 could be added as an independent axiom.

To preserve completeness when replacing an axiom A of an axiom set S with its negation, one must generate an axiom set S that is minimally weaker than S and does not imply A.

An axiom set S2 is minimally weaker than an axiom set S1 if S2 is strictly weaker than S1 and no intermediate axiom set S3 exists such that S3 is strictly weaker than S1 and S2 is strictly weaker than S3.

Only adding the negation of an axiom A of S to S , which is minimally weaker than S, preserves completeness. However, the generation of a minimally weaker axiom set S from a given axiom set S gives rise to intricate practical and theoretical problems. We cannot even prove whether a minimal weaker axiom set S exists for any axiom set S. The main theoretical and practical problem is that one must specify some upper bound for an axiom set that preserves completeness if one axiom is replaced with its negation. We leave it as an open question whether this problem is solvable and, if so, how it can be solved. Instead, we confine our DLO R -system to superpostulates of a certain length.

To do so, we adopt the following two restrictions:

We set an upper bound for any considered axiom set with a length L of 1000 characters. Restriction 2: We make use of an incomplete calculus that does not significantly increase the length of formulas when generating implied formulas.

These restrictions are justified by the practical aim of generating a system of infinity superpostulates.

Due to our restrictions, the considered superpostulates are simple enough to make use of the following assumption: Assumption 1. If one of the following cases holds, this is proven by the standard casc-mode of Vampire within a time limit of 300 s:

1. a considered part of a considered axiom set is redundant, 2. a considered minimal axiom set is inconsistent, or 3. the considered axiom set is implied by another considered axiom set or implies either (10) or (12) .

In fact, Vampire is able to almost immediately identify these cases for the simple axiom sets that we consider here in nearly all cases. By Assumption 1, we assume that Vampire can solve the semi-decidable problems 1 to 3 for axiom sets with fewer than 1000 characters to obtain a positive result within 300 s. In other words, our algorithm runs Vampire with a time limit of 300 s, and if the problem is not solved within this time limit, then we assume a negative solution. The reliability of Assumption 1 is based on extensive experience. To generate strictly weaker axioms A from an axiom A by applying an inference rule, we make use of an incomplete calculus that does not include rules for the introduction of disjuncts (∨I) and conjuncts (∧I), which would increase the length of axioms. For this reason, we cannot ensure the generation of minimally weaker axiom sets and, thus, do not necessarily preserve completeness. Instead, we consider only rules concerning quantifiers: one rule for changing the order of quantifiers (QEx), two for universal quantifier elimination (∀E1 and ∀E2) and two for existential quantifier introduction (∃I1 and ∃I2); cf. Table 3 . The abbreviated notations for the rules specify only the relevant syntactic changes. For example, ∃μ∀ν ∀ν∃μ means that the order of two quantifiers is changed in a primary formula. We tacitly presume that a sequence of universal (existential) quantifiers is orderless; each of the quantifiers of such a sequence can be considered as either the leftmost or rightmost quantifier of the sequence. μ/ν means that μ is replaced with ν. In the case of ∀E1, ν may also be replaced with the variable of a new existential quantifier preceding the resulting axiom. ∀νϕ(ν, ν) indicates that ν occurs more than once in the scope of ∀ν. ϕ(μ/ν, μ) means that at least one occurrence of μ is replaced with ν. We tacitly presume that new variables are used if a new quantifier is introduced. We establish the following rules for the application of the quantifier rules. ∀E1 can be applied such that ∃μ is taken from an axiom that differs from A after having variables renamed and PN laws applied to the effect that ∀ν is directly to the right of ∃μ. Before ∀E1 can be applied to quantifiers of one and the same axiom, PN laws must be applied to the effect that existential quantifiers that are separated by ∧ from other existential quantifiers are pulled outwards. The same holds for universal quantifiers that are separated by ∨ from other universal quantifiers. Thus, the numbers of quantifiers in a sequence of existential quantifiers and a sequence of universal quantifiers from which ∃μ and ∀ν are to be chosen are increased. ∀E2 and QEx can also be applied to universal quantifiers that are separated by ∨; QEx additionally can be applied to existential quantifiers that are separated by ∧ from the universal quantifier. In these cases, PN laws are applied to exchange the order of the universal quantifiers and ∧ or ∨. The results of the application of these rules are converted into a minimized FOLDNF in standardized notation (cf. p. 3). One application of a quantifier rule results in conversion from a set of primary formulas to a set of primary formulas. Thus, each application comprises the application of equivalence rules to prepare for the application of QEx, ∀E1 or ∀E2 and to convert the result into an FOLDNF. In the case in which the resulting FOLDNF is, in fact, a disjunction, we consider only disjuncts as axiom sets that are strictly implied by the axiom set prior to the application of a quantifier rule. Furthermore, we consider each conjunct of a disjunct of an FOLDNF as a separate axiom.

Given an axiom set S that includes axiom A, we consider the totality of all possible applications of the 5 quantifier rules to A. In the case of ∀E1, this may involve different orders of the prior application of PN laws in addition to the elimination of the universal quantified variable by variables bound by different existential quantifiers. QEx can be applied to all ∃μ and all ∀ν such that ∃μ occurs in a sequence of existential quantifiers directly to the left of a sequence of universal quantifiers containing ∀ν. ∃I1 and ∃I2 may replace variables in different positions. The totality of possible applications of QEx, ∀E1, ∀E2, ∃I1, and ∃I2 to A realizes all different applications of the five rules.

Our method of generating a DLO R -system is based on all possible nonredundant applications of the quantifier rules starting from (7).

Definition 15. An application of a quantifier rule to an axiom A of an axiom set S is non-redundant if it results in a strictly weaker axiom set S and the axiom A that replaces A in S is not implied by S without A .

If, however, S implies S or if A is not independent in S , then the application of a quantifier rule is redundant. Based on Algorithm 1, we generate a DLO R -system by means of the following rule:

Rule 3: Starting from (7), generate infinity superpostulates by iteratively applying Algorithm 1 to all axioms of all generated superpostulates until no further superpostulates are generated. Restriction: Delete superpostulates if they are implied by previously generated superpostulates.

The restriction ensures that no other infinity axiom set of S T strictly implies S; this is the best we can do to generate L-complete infinity axiom sets up to a length of 1000 characters. Furthermore, the restriction avoids repetitions and loops (cf. the application of Algorithm 1 to Axiom 1 of (13) in Example 2).

With our implementation of Rule 3, we have generated 732 superpostulates in approximately 1000 h of run time. We have generated a database of 2196 infinity superpostulates in TPTP format by applying Rules 1 to 3 starting with DLO R . None of these superpostulates can be currently solved by any of the TPTP-engines. Additionally, we have generated a database of 60 weak infinity DLO R -variants. 8 of them can be solved by SPASS within 60 s.

A prominent alternative complete theory to start with is the theory of immediate successors (THS), which can be defined as follows in familiar notation:

The following reduction THS R of THS to FOL R can be proven to be complete by adding the defining axiom ∀x∀y(x = y ↔ ∀z(Rxz ↔ Ryz)∧∀z(Rzx ↔ Rzy)) and proving the equivalence to (14) :

Vampire is able to solve (14) by saturation in 300 s, but it cannot solve (15) or variants thereof. Axioms 1, 2, and 3 of THS R are part of DLO R with a left endpoint, and Axiom 6 follows from Axiom 5 of DLO R . Axioms 4 and 5 of THS R contradict Axioms 1, 2, and 6 of DLO R . Axioms 4, 5, and 6 of DLO R contradict Axioms 1, 2, and 4 of THS R .

Remark 5. Our algorithm has generated a database of 156 superpostulates from (15) and terminated after approximately 200 h of run time. 32 of them are solved by CVC4. None of the 156 superpostulates implies any of the superpostulates of the DLO R -system or any of the weak DLO R -variants.

From a theoretical point of view, it would be desirable to generate a database of complete infinity axiom sets. However, this would involve the problem of generating minimally weaker infinity axiom sets that may be of arbitrary length. Here, our intent is to provide a pragmatic algorithm that, in fact, generates significant infinity axiom sets. Thus, we restrict the generated infinity axiom sets to a certain length. This restriction does not imply that the generated sets are not complete theories; rather, it means only that we are unable to guarantee that they are. Our algorithm starts with a complete theory of FOL R , such as DLO R or THS R , and automatically generates further infinity axiom sets S with fewer than 1000 characters such that, roughly speaking, no other infinity axiom sets with fewer than 1000 characters exist that strictly imply infinity axiom sets S. We say "roughly speaking" here because in addition to limiting the set length, we use an incomplete calculus without inference rules that would significantly increase complexity, and we test the restriction only on the basis of already generated entries in our database. We believe that the theoretical question concerning an (unrestricted) algorithm that does, in fact, preserve completeness is an important one, but we do not aim to answer it in this paper. Instead, our final objective is a practical algorithm, and we maintain that we have achieved this aim. Thus far, we have generated more than 2250 superpostulates in 10 weeks of run time. All of these superpostulates are hard problems.

Note that it is not trivial to automatically generate infinity axiom sets. Infinity axiom sets (not to say systems of infinity axiom sets) (i) are rarely encountered, (ii) can seldom be solved by logic engines, (iii) are hard problems even when they are short in length, and (iv) have not been systematically studied; moreover, (v) only a few of them exist in the TPTP library, and no systematic archive of infinity axiom sets is available. Therefore, we believe that our database is of practical importance for (i) systematically studying infinity axiom sets, (ii) deciding the satisfiability of additional infinity axiom sets that follow from our database, and (iii) improving saturation algorithms by enabling the decidability of infinity axiom sets. In regard to (i), we are investigating the question of whether starting our algorithm with different complete FOL R theories will yield identical superpostulates. MacPherson conjectured that any ω-categorical axiom set has the strict order property (cf. [10] and [4] for detailed discussions). Proofs of the property of being ω-categorical widely depend on identity. In light of MacPherson's conjecture, it would be interesting to study the limits of the DLO R -system. We have also reduced Goldbach's conjecture to FOL R and intend to study its internal relations with other infinity axiom sets in our still-growing database. In regard to (ii), we have proven in Sect. 3 that an infinite number of additional infinity axiom sets follow from our superpostulates. A database of superpostulates will make it possible to decide the satisfiability of infinity axiom sets that are implied by one of the entries of the database. In regard to (iii), we are currently working on saturation algorithms that can cope with infinity axiom sets. We know from our work how important it is to test such algorithms on a variety of intricate examples during development.

The classical decision problem

Automated inference of finite unsatisfiability

On first-order sentences without finite models

The Decision Problem. Solvable Classes of Quantificational Formulas

Grundlagen der Mathematik

Zurückfürung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, binären Funktions variablen

Minimizing disjunctive normal forms of pure first-order logic

Analytic completeness of sets of postulates

Finite axiomatizability and theories with trivial algebraic closure

Methods of Logic

The general theory of notational relativity. Typewritten manuscript of 61 pp

Mathematical Logic

Henry M. Sheffer and notational relativity

We thank the three anonymous referees for their comments and Geoff Suttcliffe for checking our database with CVC4, E, Infinox, SPASS and Vampire.

To ensure that all superpostulates are, in fact, infinity axiom sets, we consider only superpostulates that imply the very weak infinity axiom set given in (10) or its counterpart given in (12) , as generated by Rule 2:DLO R without endpoints, with a left endpoint, and with a right endpoint all imply either (10) or (12) . By Assumption 1 and our quantifier rules, it is possible to apply the following algorithm to generate a set S * of further superpostulates from a superpostulate S. Algorithm 1. Generate S * from S, which includes A, as follows: Example 2. Applying Algorithm 1 to Axiom 1 of (7) results in a set S * with the following superpostulate as its only member: Ry 1 y 1 , ∀x 1 ∃y 1 ¬Rx 1 y 1 , ∀x 1 ∃y 1 ¬Ry 1 x 1 , ∀x 1 ∃y 1 (Rx 1 y 1 ∧ ¬Ry 1 y 1 ), ∀x 1 ∃y 1 (Ry 1 x 1 ∧ ¬Ry 1 y 1 ),Axioms 4, 5, and 6 of (7)Note that the application of ∀E1 to replace x 1 in Axiom 1 of (7) with y 1 in Axiom 6 is redundant. Set (13) can, in turn, serve as a starting point for the application of Algorithm 1. Applying Algorithm 1 to Axiom 1 of (13) results in (7) once again (consider the implied minimization strategies!).Let us use S * * to denote the result of applying Algorithm 1 to all of the axioms of S; S * * is the union of all results S * . Furthermore, let us use S T to denote the totality of the generated superpostulates. Finally, we use S * * * to denote the subset of S * * that contains only superpostulates that are not implied