These web pages are a supplement to the following paper.
Computer and Human Reasoning:
Single Implicative Axioms for Groups
and for Abelian Groups
The paper appears in
American Mathematical Monthly 103(10):888-892 (December 1996).
Here is a
preprint.
Abstract
The paper presents single implicative axioms for abelian groups
in terms of addition and inverse
and in terms of subtraction,
and implicative single axioms for (ordinary) groups
in terms of product and inverse
and in terms of division.
Two of the axioms were found by a human, and the other two by
computer.
The proofs in the paper are adapted from proofs found by the
automated deduction system
Otter.
Theorems in the Paper
-
Theorem 1. x+y = z+u -> (y´+z)+u = x
is a single axiom, in terms of addition and inverse, for abelian groups.
-
Theorem 2. x-y = z-u -> u-(z-x) = y
is a single axiom, in terms of subtraction, for abelian groups.
-
Theorem 3. (x·y)·z = (x·u)·w -> u·(w·z´) = y
is a single axiom, in terms of product and inverse, for group theory.
-
Theorem 4. x/y=z/u -> y/(((z/z)/z)/((x/x)/x))=u
is a single axiom, in terms division, for group theory.