Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert: differenze tra le versioni

Scriviamo la tesi nella sua forma contrappositiva, ovvero:

 

 

Mostriamo che, se <math>A \to B</math> non è un teorema, allora <math>A \to B</math> non è una tautologia, cioè non è una formula valida, vale a dire che <math>B</math> non segue logicamente da <math>A</math>. A tal fine basta costruire, analogamente a ciò che si fa nella [[Logica/Calcolo delle proposizioni/Dimostrazione del teorema di compattezza|dimostrazione del teorema di compattezza]], un insieme <math>\Delta</math> (deduttivamente chiuso e [[Logica/Calcolo delle proposizioni/Sistema di Hilbert#Insieme di formule completo|completo]], cioè consistente e massimale) dal quale <math>A \to B</math> non è derivabile, cioè <math>\Delta \nvdash A \to B</math>. Mostreremo quindi che <math>\Delta</math> ha un modello che soddisfa <math>A</math> e non soddisfa <math>B</math>; dunque <math>\nvDash A \to B</math>.

Per costruire l'insieme <math>\Delta</math>, procediamo nel seguente modo. Enumeriamo tutte le formule del linguaggio:

 

 

Definiamo, ora, una sequenza di insiemi di formule, per induzione:

 

 

\Delta_i \cup \{A_i\}, & \text{se }\Delta_i, A_i \nvdash B; \\

\Delta_i, & \text{altrimenti.}