Prove properties of abelian groups

2025年6月4日

A group is a non-empty set G together with a binary operation on G, here denoted “\(\cdot\)”, that combines any two elements a and b of G to form an element of G, denoted \(a\cdot b\), such that the three requirements, known as “group axioms”, are satisfied: Associativity, left and right Identity element, left and right Inverse element. Further, the last two axioms can be relaxed by only requiring left identity and left inverse because right identity and right inverse can be deduced.

In a nutshell, a group satisfies the following properties: \begin{gather} \forall x. 1\cdot x=x & \label{left-identity} \\ \forall x. x^{-1}\cdot x=1 & \label{inverse} \\ \forall x \forall y \forall z. (x\cdot y)\cdot z=x\cdot (y\cdot z) & \label{associative} \end{gather}

An abelian group is also called a commutative group. It has the property \(\forall x \forall y. x\cdot y=y\cdot z\). So, if there is a group, of which all elements has order 2, ie. \eqref{assumption}, is this group abelian? \begin{equation} \forall x. x\cdot x=1 \label{assumption} \end{equation} Lemma: \(\forall x \forall y. x\cdot y\cdot x=y^{-1}\cdot 1\).

Let’s prove the lemma. \begin{align*} & x\cdot y\cdot x &\\ =& 1\cdot x \cdot y \cdot x & \eqref{left-identity}\\ =& y^{-1}\cdot y \cdot x \cdot y \cdot x & \eqref{inverse}\\ =& y^{-1}\cdot (y \cdot x) \cdot (y \cdot x) & \eqref{associative}\\ =& y^{-1}\cdot 1 & \eqref{assumption} \end{align*}

Now let’s prove the original statement. \begin{align*} & x\cdot x=1 & \eqref{assumption}\\ \Rightarrow & (x\cdot y) \cdot (x \cdot y) = 1 & \\ \Rightarrow & (x\cdot y) \cdot (x \cdot y) = x^{-1} \cdot x & \eqref{inverse} \\ \Rightarrow & x\cdot (y \cdot x) \cdot y = x^{-1} \cdot x & \eqref{associative} \\ \Rightarrow & x\cdot (y \cdot x) \cdot y \cdot x = x^{-1} \cdot x \cdot x & \\ \Rightarrow & x\cdot (y \cdot x) \cdot y \cdot x = x^{-1} \cdot 1 & \eqref{assumption} \\ \Rightarrow & x\cdot (y \cdot x) \cdot y \cdot x = y\cdot x \cdot y & \text{lemma} \\ \Rightarrow & y \cdot x\cdot (y \cdot x) \cdot y \cdot x = y \cdot y\cdot x \cdot y & \\ \Rightarrow & (y \cdot x) \cdot (y \cdot x) \cdot y \cdot x = y \cdot y\cdot x \cdot y & \eqref{associative} \\ \Rightarrow & 1 \cdot y \cdot x = 1 \cdot x \cdot y & \eqref{assumption} \\ \Rightarrow & y \cdot x = x \cdot y & \eqref{left-identity} \\ \end{align*}

We get the desired property.

vampire –saturation_algorithm (-sa) Select the saturation algorithm: – discount: – otter: – limited resource: – fmb : finite model building for satisfiable problems. – z3 : pass the preprocessed problem to z3, will terminate if the resulting problem is not ground. z3 and fmb aren’t influenced by options for the saturation algorithm, apart from those under the relevant heading default: lrs values: discount,fmb,lrs,otter,z3 –mode Select the mode of operation. Choices are: -vampire: the standard mode of operation for first-order theorem proving -portfolio: a portfolio mode running a specified schedule (see schedule) -casc, casc_sat, smtcomp – like portfolio mode, with competition specific presets for schedule, etc. -preprocess,axiom_selection,clausify: modes for producing output for other solvers. -tpreprocess,tclausify: output modes for theory input (clauses are quantified with sort information). -output,profile: output information about the problem Some modes are not currently maintained (get in touch if interested): -bpa: perform bound propagation -consequence_elimination: perform consequence elimination default: vampire values: axiom_selection,casc,casc_hol,casc_sat,clausify,consequence_elimination, model_check,output,portfolio,preprocess,preprocess2,profile, smtcomp,spider,tclausify,tpreprocess,vampire vampire –input_syntax tptp tutorial.p vampire –input_syntax tptp tutorial.p -sa fmb vampire –input_syntax tptp tutorial.p –mode casc vampire –input_syntax tptp tutorial.p –mode casc_sat