Axiomizatoin of Arithmatics

Arithmatics is something like $\forall x \exists y, x \cdot y = y\cdot x \ldots$

Theory $T$ is a collection of propositions. Model $M$ is something that really exists. $M \models T$(satisfies): All propositions in $T$ are true in $M$. $T_1 \models T_2$: Theory is a valid consequence of $T_1$ if and only if for every model of $T_1$, it is also a model of $T_2$.

Definition 6   A proof $S_1S_2\ldots S_n$ is a sequence of statements such that every statement is either AXIOM or follows from previous statements by a PROOF RULE.

Axioms at Group Theory:

1. $\forall x \in G, \forall y \in G, x+y \in G$
2. $\forall x \in G, \forall y \in G, \forall z \in G, (x+y)+z= x +(y+z)$
3. $\exists e \in G, \forall x\in G, x + e = e + x = x$,
4. $\forall x,f \exists y, x + y = e$.

Proof rules:

1. $x$, and $x\rightarrow y$, then we can conclude $y$.
2. $\forall x P(x)$ then you can conclude $P(1), P(2), \ldots$.

Definition 7   $T \vdash S$, theory proves a proposition statement, if there is a proof of $S$ from the axioms of $T$.

Now the question becomes:

Input:

proposition $S$

Output:

Group Theory proves $S$?

How to do that?

First, if in the proof rules, only the first can be used, then a BFS-based technique can be used. However, if the second is also applicable, then that BFS should be modified to enumerate the search space in a different way, using the tecnique of Diagnalization.