Function Repository Resource:

# FindEquationalCounterexample

Try to find a counterexample to an equational hypothesis in a given system of axioms

Contributed by: Jonathan Gorard
 ResourceFunction["FindEquationalCounterexample"][hyp,axms] tries to find an equational counterexample to the symbolic hypotheses hyp using the axioms axms.

## Details and Options

If ResourceFunction["FindEquationalCounterexample"][hyp,axms] succeeds in finding a counterexample to the hypotheses hyp given the axioms axms, then it returns a CounterexampleObject expression.
Axioms and hypotheses must be given in equational form.
The inputs hyp and axms can be any logical combination of terms of the form:
 expr1⩵expr2 assertion of equality ForAll[vars,stmt] assertion that stmt is true for all values of vars
The expri can be arbitrary symbolic expressions, with heads representing formal operators, functions etc.
ResourceFunction["FindEquationalCounterexample"][expr1&&expr2&&,axm1&&axm2&&] will treat each expri as a separate hypothesis and each axmi as a separate axiom.
ResourceFunction["FindEquationalCounterexample"][{expr1,expr2,},{axm1,axm2,}] is equivalent to ResourceFunction["FindEquationalCounterexample"][expr1&&expr2&&,axm1&&axm2&&].
ResourceFunction["FindEquationalCounterexample"] uses the back end of FindEquationalProof to find an appropriate counterexample to the hypothesis.

## Examples

### Basic Examples (2)

Find a counterexample to an elementary hypothesis in group theory:

 In[1]:=
 Out[1]=

Show the counterexample association:

 In[2]:=
 Out[2]=

Generate a function to verify that this is a valid counterexample to the hypothesis:

 In[3]:=
 Out[3]=
 In[4]:=
 Out[4]=

Generate a function to verify that this counterexample is consistent with the underlying axioms:

 In[5]:=
 Out[5]=
 In[6]:=
 Out[6]=

Find a counterexample to a more sophisticated hypothesis in group theory:

 In[7]:=
 Out[7]=

Show the counterexample association:

 In[8]:=
 Out[8]=

Generate a function to verify that this is a valid counterexample to the hypothesis:

 In[9]:=
 Out[9]=
 In[10]:=
 Out[10]=

Generate a function to verify that this counterexample is consistent with the underlying axioms:

 In[11]:=
 Out[11]=
 In[12]:=
 Out[12]=

### Scope (5)

#### Axiom Systems (3)

FindEquationalCounterexample supports hypotheses formulated in any equational axiom system, including Wolfram's shortest possible axiom for Boolean algebra (finding a counterexample to the hypothesis that the Nand operator is associative):

 In[13]:=
 Out[13]=

Show the counterexample association:

 In[14]:=
 Out[14]=

Generate a function to verify that this is a valid counterexample to the hypothesis:

 In[15]:=
 Out[15]=
 In[16]:=
 Out[16]=

Generate a function to verify that this counterexample is consistent with the underlying axioms:

 In[17]:=
 Out[17]=
 In[18]:=
 Out[18]=

Ring theory (finding a counterexample to the hypothesis that every ring is commutative):

 In[19]:=
 Out[19]=

Show the counterexample association:

 In[20]:=
 Out[20]=

Generate a function to verify that this is a valid counterexample to the hypothesis:

 In[21]:=
 Out[21]=
 In[22]:=
 Out[22]=

Generate a function to verify that this counterexample is consistent with the underlying axioms:

 In[23]:=
 Out[23]=
 In[24]:=
 Out[24]=

Equational Presburger arithmetic (finding a counterexample to the hypothesis that every integer is equal to its negation):

 In[25]:=
 Out[25]=

Show the counterexample association:

 In[26]:=
 Out[26]=

Generate a function to verify that this is a valid counterexample to the hypothesis:

 In[27]:=
 Out[27]=
 In[28]:=
 Out[28]=

Generate a function to verify that this counterexample is consistent with the underlying axioms:

 In[29]:=
 Out[29]=
 In[30]:=
 Out[30]=

#### Hypothesis and Axiom Specification (2)

Find a counterexample from a list of axioms:

 In[31]:=
 Out[31]=

Express the axioms as a conjunction:

 In[32]:=
 Out[32]=

Find a counterexample to a list of hypotheses:

 In[33]:=
 Out[33]=
 In[34]:=
 Out[34]=

Express the hypotheses as a conjunction:

 In[35]:=
 Out[35]=

Jonathan Gorard

## Version History

• 1.0.0 – 28 August 2020