How to formally prove $\forall x: x11=x$ in the theory of groups.

86 Views Asked by At

Def 1: $M$ is a $\underline{theory}$, if it is a collection of first order statements.

Def 2: Given theory $M$ and first order statement $\phi$, then $M$ can $\underline{prove}$ $\phi$ if, starting with some statements $m_0,m_1,...,m_n \in M$ and following the rules of deduction we arrive at $\phi$.

Def 3: Given a constant symbol 1, the $\underline{theory \ of \ groups}$ is:

Identity $$\forall x : x1=x $$

Associativity $$\forall x,y,z: (xy)z=x(yz) $$

Inverses $$\forall x : x^{-1} x = x x^{-1} = 1 $$ $$ $$

$$Updated \ Proof \ Attempt: $$

\begin{align*} 1. \ \forall x : x1=x& \ \ \ Identity \\ 2. \ \forall x: x1=x \Rightarrow \ y1=y& \ \ \ Universal \ Instantiation \ (with \ x=y) \\ 3. \ \forall x: x1=x \Rightarrow \ (y1)1=y1& \ \ \ Universal \ Instantiation \ (with \ x=y1) \\ 4. \ y1=y& \ \ \ 1,2, \ Modus \ Ponens \\ 5. \ (y1)1=y1& \ \ \ 1,3, \ Modus \ Ponens \\ 6. \ (y1)1=y& \ \ \ 4,5, \ Transitivity \\ 7. \forall x : (x1)1 = x& \ \ \ 2-6, \ Universal \ Generalization \ (y \ was \ arbitrary) \end{align*}

1

There are 1 best solutions below

2
On

Almost always,$^*$ the way to produce a formal proof is to first produce a very detailed informal proof, and then step-by-step convert it into your specific proof calculus (there are many different notions of formal proof for first-order logic; they're all ultimately equivalent, but they have different details, and a complete answer to your question is impossible without knowing your specific system).

An informal proof of $\forall x[(x1)1=x]$ goes as follows:

  • For all $z$, $z1=z$ from the group axioms.

  • In particular, this implies $(x1)1=x1$ (applying the above with $z=x1$).

  • Separately, this implies $x1=x$ (applying the first bullet with $z=x$).

  • Putting these together, we get $(x1)1=x1$.

Now it should be clear what you're going to want to do here: you need to do a couple instantiations, and then compose equalities. Can you see how to do this in your specific proof calculus?


There are exceptions, when the statement in question is "obvious" but the proof system is meaningfully weak. For example, intuitively we should be able to combine a proof of $B$ from $A$ and a proof of $C$ from $B$ to get a proof of $C$ from $A$; however, depending on what proof calculus you use this turns out to be more complicated than it sounds (even though it does work in the end). And these are not always pathological cases - indeed, the issue in the previous sentence ("cut elimination") is of fundamental importance in mathematical logic, specifically proof theory.

However, this is not the situation you're in here.