In this well-written but quite technical paper, the author considers the logical theory T of two commuting permutations, whose axioms are ( i = 1 , 2 )
A1i ∀ x ∃ y ∀ z ( R i ( x , z ) ↔ y = z )
A2i ∀ x ∃ y ∀ z ( R i ( z , x ) ↔ y = z )
A3 ∀ x ∀ y ∀ z ∀ u ( R 1 ( x , y ) ∧ R 2 ( x , z ) ∧ R 2 ( y , u ) ⟹ R 1 ( z , u ) )
The main result is that SAT( T ), the set of first-order formulas in the language of T (notice there are no function symbols or constants) that are true in some model of T, is a set decidable in nondeterministic time 2 c n 2 and space 2 c n, where n is the length of the formula to be decided. This is to be contrasted with the theory of two permutations (which do not necessarily commute), which is undecidable, and the theory of one permutation, which is decidable with the same upper bounds.
The method of proof is a detailed analysis of the models of this theory, which may be viewed as digraphs with edges labeled with {1,2}. Every model of T is a direct sum of its connected components, each of which may be characterized by a triple ( r , s , t ) ∈ ( N+ ∪ { &ohgr; } ) × ( N+ ∪ { &ohgr; } ) × (Z ∪ { &ohgr; } ). Distance in a connected model is defined as minimal path length. The author proves that if A and B are two connected models and their spheres of radius 2 n - 1 are isomorphic, then A ≡ n B ; that is, for any formula &phgr; of quantifier depth not more than n , A ⊧ &fgr; ↔ B ⊧ &fgr; . Decidability follows from the author’s further result that for every model A of T, there is a finite connected model A′ of cardinality < n 2 9n + 1 such that A ≡ n A′.
The algorithms for testing satisfiability are not deep but simply enumerate possible models; rather the significance of this paper lies in the analysis of models of T. As expected, there is a speedup if an alternating TM is used in place of a nondeterministic TM. The author does not consider lower bounds for the problem except to observe that the lower bound for the theory of one permutation is a lower bound for T.
