A note on syntactic symmetry and the manipulation of formal systems by machine

Abstract

In the past few years, digital computer programs that depart from the traditional numerical computation and data processing for which these machines were conceived have become increasingly commonplace. In many of these programs, the computer is called upon to manipulate a complex formal logistic system as a tool to implement the solution of a problem. This paper is concerned with the problem of efficient machine manipulation of formal systems in which the predicates display a high degree of symmetry. The solution to the problem, embodied in a theorem and a rule of syntactic symmetry is specified in Section I. The theorem is in fact a metatheorem concerning formal systems, and is used in the synthesis of proofs. On the other hand, the rule is an invaluable aid in the search for a proof by the so-called analytic method. In Section II, the set of all syntactic symmetries for a given set of formulas is constructed and displayed in a form conducive to minimum effort programming for a computer. © 1959 Academic Press Inc.