gives an axiomatic representation of the specified axiomatic theory.


uses si to represent the operator opi in the theory.


gives the specified property of an axiomatic theory.


  • 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:
  • "AncillaryDefinitions"definitions for related operators
    "AncillaryOperators"related operators
    "Axioms"list of axioms
    "AxiomsAssociation"association of axioms with names as keys
    "Dataset"dataset of all property value pairs of the theory
    "Description"description of the theory
    "EquivalentTheories"names of theories equivalent to this one
    "FormulationDate"date of formulation of the theory
    "Formulators"authors of the theory
    "LogicType"type of logic used for the axioms of the theory
    "NotableTheorems"notable named theorems in the theory
    "Operators"operators in the theory and their representations
    "OperatorArities"arities of operators in the theory
    "Reference"bibliographical citation for the theory
    "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")
    "OrNotBooleanAxioms"Boolean logic with operators "Or" and "Not"
    "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")
  • Other logic-related theories include:
  • "EquivalentialCalculusAxioms"axioms for equivalential calculus
    "ImplicationalCalculusAxioms"axioms for implicational calculus
    "JunctionalCalculusAxioms"axioms for junctional calculus
  • AxiomaticTheory supports the following other algebraic theories:
  • "AbelianGroupAxioms"standard axioms for Abelian group theory
    "AbelianMcCuneAxioms"McCune's single axiom for Abelian group theory
    "AbelianTarskiAxioms"Tarski's single axiom for Abelian group theory
    "CentralGroupoidAxioms"standard axioms for central groupoids
    "CombinatorAxioms"axioms for the purely algebraic theory of combinators
    "CommutativeRingAxioms"standard axioms for a commutative ring without identity
    "CommutativeRingWithIdentityAxioms"standard axioms for a commutative ring with identity
    "FieldAxioms"standard axioms for field theory
    "GroupAxioms"standard axioms for group theory
    "HigmanNeumannAxioms"Higman and Neumann single axiom for group theory
    "LeftNearRingAxioms"standard axioms for a left near-ring
    "McCuneAxioms"McCune's single axiom for group theory
    "MeadowAxioms"standard axioms for meadow theory
    "MonoidAxioms"standard axioms for a monoid
    "RightNearRingAxioms"standard axioms for a right near-ring
    "RingAxioms"standard axioms for a general ring
    "RingWithIdentityAxioms"standard axioms for a ring with identity
    "SemigroupAxioms"standard axiom for a semigroup
    "SemiringAxioms"standard axioms for a semiring
    "SquagAxioms"standard axioms for squags (Steiner quasigroups)
  • 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.


open allclose all

Basic 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:

Return the axiom using your own named operator:

Prove commutativity of the operator:

Scope  (8)

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:

Get notable theorems of Boolean algebra:

Get a dataset of information about the following:

Show the named axioms:

List the authors of a theory:

Year of formulation:

Bibliographical citation:

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 theory1 is a subtheory of theory2, then theory2 is a supertheory of theory1:

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:

Wolfram Research (2019), AxiomaticTheory, Wolfram Language function, (updated 2021).


Wolfram Research (2019), AxiomaticTheory, Wolfram Language function, (updated 2021).


Wolfram Language. 2019. "AxiomaticTheory." Wolfram Language & System Documentation Center. Wolfram Research. Last Modified 2021.


Wolfram Language. (2019). AxiomaticTheory. Wolfram Language & System Documentation Center. Retrieved from


@misc{reference.wolfram_2024_axiomatictheory, author="Wolfram Research", title="{AxiomaticTheory}", year="2021", howpublished="\url{}", note=[Accessed: 19-July-2024 ]}


@online{reference.wolfram_2024_axiomatictheory, organization={Wolfram Research}, title={AxiomaticTheory}, year={2021}, url={}, note=[Accessed: 19-July-2024 ]}