(forall x)P(x) -> not (exists x) not P(x)    Tautologia

(forall x)P(x) -> (exists x)P(x)      Enunciato che risulterà valido (ai sensi della semantica)
                                      e dimostrabile (nell'apparato deduttivo, detto "calcolo"),
                                      *non* tautologica
                                      
(forall x)(forall y) =(+(x,y),+(y,x)) Enunciato che risulterà vero in tutti i modelli
                                     dell'aritmetica di Peano; risulterà anche dimostrabile
                                     sotto determinati assiomi propri