[(∀x. xz=x ∧ zx=x) ∧ ¬(z=e)]1
                  ----------------------------------
                        (∀x. xz=x ∧ zx=x)                        (∀x. xe=x ∧ ex=x) 
                     -------------------------------            -------------------------
                               ez=e ∧ ze=e                             ze=z ∧ ez=z
                            -----------------                     --------------------
                                  ez=e                                    ez = z              [(∀x. xz=x ∧ zx=x) ∧ ¬(z=e)]     
                                -----------------------------------------------------       ----------------------------------
                                                        e=z                                                 ¬(z=e)
                                              -------------------------------------------------------------------------- (**)
   [∃v.((∀x. xv=x ∧ vx=x) ∧ ¬(v=e))]2                                            ⊥
----------------------------------------------------------------------------------------------- (1)
                                                 ⊥
                                  -------------------------------- (2)
                                    ∀v((∀x. xv=x ∧ vx=x) → v=e)


Notare che ∃v.((∀x. xv=x ∧ vx=x) ∧ ¬(v=e)) equivale a ¬ ∀v.((∀x. xv=x ∧ vx=x) → v=e) poiche'
∃v.A equivale a ¬ ∀v.¬A
A→B equivale a ¬A ∨ B
A ∨ B equivale a ¬(¬A ∧ ¬B)
¬¬A equivale ad A

Notare come la regola (*) non sia presente nel nostro sistema formale. E' pero' una regola derivata (sia nel sistema alla Hilbert in [SM] che in quello di deduzione naturale in [AU]; la dimostrazione della sua derivabilita' e' presente nei testi citati). Noi la utilizziamo qui poiche' e' utile in questo putno e non modifica la potenza del sistema logico.
E' un classico esempio di utilizzo ed utilita' delle regole derivabili o ammissibili.


Vediamo qual e' la dimostrazione dell'unicita' dell'elemento neutro che viene solitamente data quando si studia la teoria dei gruppi in matematica:
Supponiamo che esista un elemento neutro diverso da e, chiamiamolo z. Essendo z un elemento neutro, lo e' in particolare per e, per cui ez=e. Inoltre, poiche' z e' un elemento del gruppo ed e e' un elemento neutro, avremo anche che e>z=z. Poiche' abbiamo che ez=e e che ez=z otteniamo che e=z, ottenendo quindi una contraddizione con l'assunzione che avevamo fatto, cioe' che e fosse diverso da z. E' quindi falso che possa esistere un elemento neutro diverso da e. Quindi ogni elemento che sia neutro per il gruppo deve necessariamente essere uguale ad e.

Vediamo come la dimostrazione in deduzione naturale nella logica dei predicati rifletta e renda piu' preciso il ragionamento utilizzato in questa dimostrazione:

Supponiamo, per assurdo, che esista un elemento neutro differente da e:
   ∃v.((∀x. xv=x ∧ vx=x) ∧ ¬(v=e))
chiamiamo z tale elemento:
                       (∀x. xz=x ∧ zx=x) ∧ ¬(z=e)
per quanto ipotizzato, tale elemento z e' appunto un elemento neutro del gruppo:

                      (∀x. xz=x ∧ zx=x) ∧ ¬(z=e)
                  ----------------------------------
                          (∀x. xz=x ∧ zx=x)                        
Poiche' z e' elemento neutro, lo e' in particolare per e, che e' un elemento del gruppo:

                      (∀x. xz=x ∧ zx=x) ∧ ¬(z=e)
                  ----------------------------------
                          (∀x. xz=x ∧ zx=x)                        
                        -------------------------            
                              ez=e ∧ ze=e                             
in particolare

                      (∀x. xz=x ∧ zx=x) ∧ ¬(z=e)
                  ----------------------------------
                          (∀x. xz=x ∧ zx=x)                        
                        --------------------------            
                               ez=e ∧ ze=e                             
                            -----------------                    
                                  ez=e                                   

Ora, essendo e un elemento neutro, lo e' in particolare per z:

                
                    
                                                                       (∀x. xe=x ∧ ex=x) 
                                                                   -------------------------
                                                                          ze=z ∧ ez=z
                                                                      -----------------
                                                                            ez = z              

Quindi e=z:

                     (∀x. xz=x ∧ zx=x) ∧ ¬(z=e)
                  -------------------------------
                        (∀x. xz=x ∧ zx=x)                        (∀x. xe=x ∧ ex=x) 
                     ----------------------------               -------------------------
                               ez=e ∧ ze=e                             ze=z ∧ ez=z
                            -----------------                     --------------------
                                  ez=e                                    ez = z                 
                                -----------------------------------------------------       
                                                        e=z                                                 
Questo fatto e' pero' in contraddizione con il fatto che z sia diverso da e:

                  (∀x. xz=x ∧ zx=x) ∧ ¬(z=e)
                  ----------------------------------
                        (∀x. xz=x ∧ zx=x)                        (∀x. xe=x ∧ ex=x) 
                     -------------------------------            -------------------------
                               ez=e ∧ ze=e                             ze=z ∧ ez=z
                            -----------------                     --------------------
                                  ez=e                                    ez = z              (∀x. xz=x ∧ zx=x) ∧ ¬(z=e)    
                                -----------------------------------------------------       -------------------------------
                                                        e=z                                                 ¬(z=e)
                                              --------------------------------------------------------------------------
                                                                                      ⊥
A questo punto possiamo affermare che l'aver assunto che esista un elemento neutro diverso da e ci ha portato ad una contraddizione:

                 [(∀x. xz=x ∧ zx=x) ∧ ¬(z=e)]1
                  ----------------------------------
                        (∀x. xz=x ∧ zx=x)                        (∀x. xe=x ∧ ex=x) 
                     -------------------------------            -------------------------
                               ez=e ∧ ze=e                             ze=z ∧ ez=z
                            -----------------                     --------------------
                                  ez=e                                    ez = z              [(∀x. xz=x ∧ zx=x) ∧ ¬(z=e)]     
                                -----------------------------------------------------       ----------------------------------
                                                        e=z                                                 ¬(z=e)
                                              --------------------------------------------------------------------------
 ∃v.((∀x. xv=x ∧ vx=x) ∧ ¬(v=e))                                               ⊥
----------------------------------------------------------------------------------------- (1)
                                                 ⊥
                                  
L'esser arrivati ad una contraddizione partendo dall'assunzione dell'esistenza di un elemento neutro diverso da e ci permette quindi di affermare che non esiste un elemento neutro diverso da e:

                 [(∀x. xz=x ∧ zx=x) ∧ ¬(z=e)]1
                  ----------------------------------
                        (∀x. xz=x ∧ zx=x)                        (∀x. xe=x ∧ ex=x) 
                     -------------------------------            -------------------------
                               ez=e ∧ ze=e                             ze=z ∧ ez=z
                            -----------------                     --------------------
                                  ez=e                                    ez = z              [(∀x. xz=x ∧ zx=x) ∧ ¬(z=e)]     
                                -----------------------------------------------------       ----------------------------------
                                                        e=z                                                 ¬(z=e)
                                              --------------------------------------------------------------------------
 [∃v.((∀x. xv=x ∧ vx=x) ∧ ¬(v=e))]2                                              ⊥
----------------------------------------------------------------------------------------- (1)
                                                 ⊥
                                ------------------------------------ (2)
                                 ¬(∃v.((∀x. xv=x ∧ vx=x)) ∧ ¬(v=e))) 
Notiamo come affermare che non esiste un elemento neutro diverso da e equivale ad affermare che tutti gli elementi neutri sono uguali ad e: ∀v((∀x. xv=x ∧ vx=x) → v=e), che e' la formulazione utilizzata in [AAb]pag.116.