AxiomaticTheory
AxiomaticTheory["theory"]
gives an axiomatic representation of the specified axiomatic theory.
AxiomaticTheory[{"theory","op_{1}"s_{1},"op_{2}"s_{2},…}]
uses s_{i} to represent the operator op_{i} in the theory.
AxiomaticTheory[theory,"property"]
gives the specified property of an axiomatic theory.
Details
 AxiomaticTheory by default uses formal symbols such as a to represent free variables in axioms.
 AxiomaticTheory by default uses functions with predefined formatting but without predefined values to represent operators and constants in axioms. Examples are CircleTimes, CenterDot and OverTilde, formatted as ⊗, · and .
 AxiomaticTheory[] gives a list of supported axiomatic theories.
 AxiomaticTheory[theory] is equivalent to AxiomaticTheory[theory,"Axioms"].
 AxiomaticTheory supports the following properties:

"Axioms" list of axioms "Operators" operators in the theory and their representations "OperatorArities" arities of operators in the theory "NotableTheorems" notable named theorems in the theory "EquivalentTheories" names of theories equivalent to this one "Subtheories" names of theories that are contained by this one "Supertheories" names of theories that contain this one  "OperatorArities" gives a list suitable for use in Groupings.
 AxiomaticTheory supports the following theories for Boolean algebra:

"BooleanAxioms" six standard axioms (operators: "And", "Or" and "Not") "HillmanAxioms" Hillman's three axioms (operators: "Nand") "HuntingtonAxioms" Huntington's three axioms (operators: "Or" and "Not") "MeredithAxioms" Meredith's two axioms (operators: "Nand") "RobbinsAxioms" Robbins's three axioms (operators: "Or" and "Not") "ShefferAxioms" Sheffer's three axioms (operators: "Nand") "WolframAxioms" Wolfram's shortest possible axiom (operators: "Nand") "WolframAlternateAxioms" Wolfram's alternate shortest axiom (operators: "Nand") "WolframCommutativeAxioms" Wolfram's two axioms (operators: explicitly commutative "Nand")  AxiomaticTheory supports the following other algebraic theories:

"AbelianGroupAxioms" standard axioms for Abelian group theory "AbelianHigmanNeumannAxioms" Higman and Neumann single axiom for Abelian group theory "AbelianMcCuneAxioms" McCune's single axiom for Abelian group theory "GroupAxioms" standard axioms for group theory "HigmanNeumannAxioms" Higman and Neumann single axiom for group theory "McCuneAxioms" McCune's single axiom for group theory "MonoidAxioms" standard axioms for a monoid "RingAxioms" standard axioms for a ring with multiplicative identity "SemigroupAxioms" standard axiom for a semigroup  AxiomaticTheory[{"GroupAxioms",g,…},"Axioms"] returns the list of standard axioms for group theory as well as the group relations for the FiniteGroupData group g, as given by FiniteGroupData[g,"DefiningRelations"] but expressed using the operators and constants used in the axioms.
Examples
open allclose allBasic Examples (2)
Give a statement of the standard axioms for group theory:
Find supertheories of group theory:
This is Wolfram's shortest possible axiom for Boolean algebra:
By default, the axiom uses CenterDot to format the binary operator used:
Scope (6)
Give a list of currently supported axiomatic theories:
Give a list of currently supported properties about axiomatic theories:
Get the axioms of a theory, using default names for its operators:
AxiomaticTheory[theory] also gives the axioms of the theory:
These are the default operator names used by the group axioms in AxiomaticTheory:
Specify your own operator names using an association:
Specify only the name of the inversion operation:
Find the arities of the operators of an axiomatic theory:
Get the same arities for the same theory with your own specification of operator names:
Applications (2)
Take the axioms of Boolean logic in this form:
Get the arities of the operators of the theory:
Construct all formulas containing the same free variable twice:
Select which of those formulas is equivalent to the free variable itself:
Get the axioms of group theory and the generating relations for the quaternion group, generated by i, j:
Prove that the fourth power of both generators is the identity element:
Properties & Relations (3)
If theory_{1} is a subtheory of theory_{2}, then theory_{2} is a supertheory of theory_{1}:
Equivalent theories of theory are not considered subtheories nor supertheories of theory:
The axioms of a subtheory can be proven from those of a supertheory using the same operators:
However, not all theorems of the supertheory can be proven from those of the subtheory: