Prendiamo come definizione generale (e semplificata) di correttezza di un sistema formale la seguente:
  Un sistema e' corretto rispetto ad una semantica quando, se alpha e' derivabile (e quindi un teorema), allora alpha e' valido.

Con questa definizione semplificata di correttezza non e' vero che
     in un sistema corretto gli assiomi sono validi e le regole

     permettono di affermare conclusioni valide nel caso in cui le premesse siano valide.

Basta infatti prendere un sistema formale con una regola di inferenza che abbia come premessa una fbf valida
e come conseguenza una fbf non valida, e che inoltre non sia mai utilizzabile in una deduzione di un teorema.
Per esempio possiamo prendere il sistema
 S={0,1}
W={x in S*| x e' lunga 2}
Ax={10}
R =  __00___
       11

e possiamo considerare la semantica secondo la quale sono valide tutte e sole le fbf che contengono almeno uno '0'
R ha come premessa una formula valida, ma ha come conclusione una fbf non valida.
Eppure il sistema e' corretto (con la definizione di correttezza che abbiamo dato).


Quello che si puo' dimostrare invece (per induzione) e' qualcosa di diverso:
    se un sistema e' corretto (rispetto ad una certa semantica) allora
    tutti gli assiomi sono validi e in ogni deduzione, se i questa e'  presente la conclusione di una regola, questa conclusione e' valida.
[Farlo per esercizio]

Se come definizione di correttezza invece prendiamo quella piu' generale, e cioe':
        un sistema e' corretto quando
       SE Gamma |-- alpha ALLORA nel caso in cui tutte le fbf di Gamma siano valide, anche alpha e' valida
allora l'affermazione dell'esercizio e' dimostrabile in modo banale:
prendiamo un assioma A e consideriamo la derivazione composta solo da A. Per definizione di correttezza, A e' necessariamente valida;
porendiamo una qualsiasi regola e siano alpha-1,.., alpha-n le sue premesse e sia beta la sua conclusione. In questo caso prendiamo
come derivazione la sequenza alpha-1..alpha-n beta, che ci permette di affermare  alpha-1,.., alpha-n |-- beta e questo per
definizione di correttezza corrisponde a dire che la conclusione della regola e' valida se le premesse sono valide.

In realta' uan definizione di correttezza VERAMENTE GENERALE (che possa cioe' essere sensata per ogni possibile sistema formale)
non si puo' dare.
Vedremo infatti che in Po la definizione di correttezza non e' esattamente quella che abbiamo fornito ora.
Lo stesso vale per la completezza