How to find axioms for finite domains: A computational exploration of mathematical discovery

AbstractAxioms are pervasive in mathematics and formulating the axioms for a particular discipline has often been an important step in the development of mathematics. One way mathematicians arrive at axioms is by characterizing a given domain that consists of objects (e.g., numbers or points and lines) and relations between them. We present a software system that, given a set of objects and relations as input, determines, first, a set of first-order formulas that are satisfied in that domain, and, second, a set of axioms from which all of these formulas can be derived. Several domains are used to illustrate our program. By comparing the axioms for different domains, analogies between these domains can be expressed, such as structural and invariance properties. From the complexities of the implementation and the discussion of various examples, conclusions are drawn about the process of axiomatization in mathematical practice.


Return to previous page