AxiomaticTheory

AxiomaticTheory["theory"]

gives an axiomatic representation of the specified axiomatic theory.

AxiomaticTheory[{"theory","op1"s1,"op2"s2,}]

uses si to represent the operator opi 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 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.

Examples

open all close all

Basic Examples  (3)

Give a statement of the standard axioms for group theory:

In[1]:=
Click for copyable input
Out[1]=

Find supertheories of group theory:

In[2]:=
Click for copyable input
Out[2]=

This is Wolfram's shortest possible axiom for Boolean algebra:

In[1]:=
Click for copyable input
Out[1]=

By default, the axiom uses CenterDot to format the binary operator used:

In[2]:=
Click for copyable input
Out[2]=

Return the axiom using your own named operator:

In[3]:=
Click for copyable input
Out[3]=

Prove commutativity of the operator:

In[4]:=
Click for copyable input
Out[4]=

Give a list of currently supported axiomatic theories:

In[1]:=
Click for copyable input
Out[1]=

Applications  (1)

Introduced in 2019
(12.0)