Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert

Indice del libro


L'approccio al problema della deduzione seguito nei sistemi assiomatici consiste nell'individuare un insieme di proposizioni da cui partire, come dei principi che ci permettano di ottenere altre proposizioni, e di limitare al minimo il numero di regole di inferenza. Le proposizioni da cui partire, che quindi vengono assunte come primitive, sono gli assiomi (logici).

Sono stati proposti vari sistemi assiomatici. Presentiamo qui di seguito quello introdotto da Hilbert, noto come sistema hilbertiano per la logica proposizionale. Il sistema di dimostrazione è stato proposto in modo formale da Hilbert, ma era già in uso dall'opera di Frege, per cui lo indichiamo con i due nomi. Si noti come questo sistema ricordi la geometria di Euclide: degli assiomi su cui non si discute e delle regole per derivare da questi nuove verità.

Definizione

modifica

  Definizione

Siano  ,   e   tre simboli proposizionali. Il calcolo proposizionale è definito dai seguenti schemi di assioma e dalle seguenti regole di inferenza.

1. Schemi di assioma

(a)  ;
(b)  ;
(c)  .

2. Regole di inferenza

  • Modus Ponens (MP)
 
cioè, da   e   è possibile derivare  .
  • Sostituzione Uniforme (SU)
 
dove   è un simbolo proposizionale che può occorrere in  ,   è una proposizione e   non occorre in  ,   è detta un'istanza di  .

Gli assiomi del sistema hilbertiano coinvolgono solo i connettivi   e  ; vedremo nel seguito come estenderli agli altri connettivi. In effetti, è in virtù della sostituzione uniforme che possiamo parlare di schemi di assioma; in altri termini, l'insieme   degli assiomi del calcolo proposizionale è l'insieme di tutte le formule che si ottengono sostituendo uniformemente proposizioni al posto dei simboli proposizionali negli schemi a, b e c. È dunque chiaro che l'insieme degli assiomi   è un insieme infinito, poiché l'insieme delle istanze di a, b e c è infinito.

Altre possibili definizioni

modifica

Modus Tollens

modifica

Il modus tollens (MT) è un'altra possibile regola di inferenza:

  cioè, da   e   è possibile derivare  .

L'assioma di Meredith

modifica

Un logico Irlandese, Carew Meredith, nel 1953 ha proposto un singolo schema di assioma, che può sostituire i tre schemi che abbiamo visto sopra.

Lo schema è:

 .

I logici credono, ma non è ancora stato provato, che questa sia la singola formula più corta possibile da cui può essere derivato l'intero calcolo delle proposizioni basato su implicazione e negazione e con le sole regole deduttive MP e SU.

Relazione di derivazione

modifica

Seguendo le definizioni di dimostrazione e di teorema, diciamo che una sequenza   è una dimostrazione di   sse   e, per ogni  ,  ,   è un'istanza di uno schema di assioma (cioè, è ottenuto da a, b e c per mezzo di SU), oppure   è ottenuto da   e  ,  , per MP, dove  . In tal caso,   è un teorema del calcolo proposizionale e lo indichiamo:

 

che si legge "  è dimostrabile", dove il pedice   sta a indicare che la dimostrazione è stata fatta con l'apparato deduttivo hilbertiano. Diciamo che una proposizione   ha una prova da un insieme di proposizioni   se esiste una derivazione   tale che, per ogni  ,  ,   è un'istanza di uno schema di assioma (cioè, è ottenuto da a, b e c per mezzo di SU), oppure   è ottenuto da   e  ,  , per MP, dove  , o   è in  . Se   ha una dimostrazione da  , scriviamo:

 

che si legge "da   si deriva  ". Gli elementi di   sono chiamati premesse, o ipotesi, o anche dipendenze di  . Dalla definizione di dimostrazione, è evidente che

  implica   per qualunque  

quindi, in particolare,

  per ogni  .

Nel seguito, non essendoci possibilità di confusione, ometteremo il pedice  ; inoltre, se   ha una dimostrazione da  , scriviamo  . Scriviamo   per indicare che   per ogni formula  .

Proprietà

modifica

Illustriamo ora le proprietà della relazione di derivazione  . Diciamo che   è una relazione, in quanto  .

Le seguenti sono proprietà della relazione di derivazione   nel calcolo proposizionale:

  1. Inclusione: Se   allora  ;
  2. Monotonia: Se   e   allora  ;
  3. Compattezza:   sse esiste un   finito, tale che   e  ;
  4. Taglio: Se   e per ogni   si ha che  , allora  .

Dimostrazione

1. Inclusione. Sia  , dalla definizione di dimostrazione di   da   segue che  .
2. Monotonia. Sia  , dunque esiste una dimostrazione  , da   per  . Procediamo per induzione completa.
(Passo base)   oppure   è un assioma. Se  , allora  , dunque, per inclusione,  ; se   è un'istanza di assioma, allora  .
(Passo induttivo) Supponiamo vero per ogni   che  . Se   o   è un'istanza di assioma, allora, come sopra,  . Se   è stato derivato mediante MP, lo si è ottenuto da  ,  ,  , ma per ipotesi induttiva   e  , pertanto, per MP,  .
3. Compattezza. Se  , allora esiste una dimostrazione   da  . Se nessun  , allora  , dunque la tesi è vera. Altrimenti, consideriamo l'insieme   degli   che occorrono nella dimostrazione di   tali che  . Tale insieme è finito. Siccome per ogni altro   che occorre nella dimostrazione di   abbiamo che o è un'istanza di uno schema di assioma, o è ottenuto da due precedenti proposizioni per MP, ne segue che  . Viceversa, supponiamo che  ; per monotonia, poiché  , abbiamo  . (Si può notare che una direzione della compattezza è per l'appunto la monotonia).
4. Taglio. Supponiamo   e, per ogni  ,  . Consideriamo una derivazione   di   da  . Se   è vuoto, la tesi è dimostrata. Altrimenti, per ogni  , avremo per ipotesi una dimostrazione   da  . Possiamo quindi sostituire in   ciascun   con la relativa dimostrazione a partire da  , ottenendo la sequenza  . Questa sequenza è una dimostrazione di   da  , quindi  .

Introduzione di ulteriori connettivi

modifica

Come accennato in precedenza, altri connettivi possono essere introdotti mediante definizioni, ad esempio:

  1.  ;
  2.  ;
  3.  .

Osserviamo che, in questo contesto, abbiamo dato delle definizioni per i connettivi perché non possiamo utilizzare la nozione di completezza di insiemi di connettivi, che si basa sulla nozione di valutazione booleana. Qui, infatti, stiamo solo considerando un "calcolo", che è una nozione puramente sintattica, dunque non siamo autorizzati a utilizzare nozioni semantiche, quali l'equivalenza logica. Non possiamo usare nozioni semantiche fintantoché non dimostreremo un teorema che ci dice che "possiamo utilizzare le tautologie come teoremi", ovvero il teorema di completezza.

Teorema di deduzione

modifica

Sia   un insieme di formule proposizionali e siano   e   due formule proposizionali, allora

  sse  .

Dimostrazione

modifica

( ) Sia   una dimostrazione di   da  . Procediamo per induzione completa.

(Passo base)  , oppure   è un assioma, oppure è   stesso. Per lo schema a abbiamo  , dunque, se   o   è un assioma, abbiamo per MP che  . Se  , siccome   è un teorema, abbiamo  .

(Passo induttivo) Supponiamo che  , per ogni  . Consideriamo  . Come sopra, se   o   è un assioma o   abbiamo che  . Supponiamo allora che   sia stato derivato per MP. Dunque, lo si è ottenuto da due formule  ,  ,  . Per ipotesi induttiva,   e  .   è della forma  , dunque abbiamo  . Per lo schema di assioma b, abbiamo che  . Da questa formula, da   e da  , applicando due volte MP, si ha  .

( ) Supponiamo che  . Per monotonia abbiamo che  . Per inclusione, invece, si ha che  . Dunque, per MP si ottiene che  .

Osservazioni

modifica

Il teorema di deduzione ci dice che una formula può passare da sinistra a destra della relazione   introducendo il connettivo  , oppure da destra a sinistra eliminandolo. Questo risultato è importante per due ragioni. In primo luogo, perché ci fornisce la possibilità di esprimere una relazione metalinguistica (quale  ) mediante una formula del linguaggio.

In secondo luogo, esso ci fornisce la possibilità di trattare generiche derivazioni da insiemi di formule come teoremi. Infatti, in virtù della proprietà di compattezza di  , abbiamo che, se  , allora esiste un insieme finito   tale che  . Siccome   è finito, sarà del tipo  , o equivalentemente  , quindi   implica  , che equivale a   e  . Per il teorema di deduzione, otteniamo   e  .

Consistenza

modifica

Introduciamo ora la nozione di consistenza.

Insieme di formule consistente

modifica

  Definizione

Un insieme di formule proposizionali   è consistente sse è verificata una delle seguenti proprietà:

  1. non esiste una proposizione   tale che   e  ;
  2. esiste una proposizione   tale che  .

Si può dimostrare che le due formulazioni sono equivalenti.

( ) Se non esiste una proposizione   tale che   e  , allora si ha che   oppure   per ogni proposizione  , dunque esiste una proposizione   tale che  .

( ) Scriviamo la tesi in forma contrappositiva: se esiste una proposizione   tale che   e  , allora non esiste una formula   tale che  , che equivale a dire   per ogni formula  .

Se si dimostra che   per ogni formula  , allora, per taglio sulle premesse, si ha che  .

Per il teorema di deduzione, abbiamo che  . Dunque,   sse  .

Essendo   un teorema, effettivamente vale  , e, per taglio sulle premesse, si ha che   per ogni formula  .

Dunque, per contrapposizione, se esiste una formula   tale che  , allora non esiste una proposizione   tale che   e  .

Insieme di formule completo

modifica

  Definizione

Un insieme di formule   si dice consistente e massimale o completo se, per ogni formula  , si verifica una e una sola delle seguenti relazioni:

  oppure  .

Notare che la nozione di insieme consistente e massimale è analoga a quella di insieme massimale soddisfacibile.

Correttezza e completezza

modifica

Precedentemente, sono state introdotte le nozioni di "dimostrazione", "teorema", "assioma", "derivazione", ecc. e abbiamo mostrato delle utili proprietà della relazione  .

Illustriamo ora la relazione che lega i teoremi e le tautologie. La domanda che ci poniamo è: tutto ciò che deriviamo mediante   senza premesse è vero in tutti i modelli della logica?

In secondo luogo, vogliamo sapere in che relazione stanno le formule proposizionali derivabili da un insieme di proposizioni   con le formule vere nei modelli di  . Supponiamo che   sia un insieme di proposizioni che descrivono una determinata realtà; quando deriviamo un enunciato   da  , è importante sapere se   è vero nelle realtà che sono modelli di  . Ovvero, ci interessa sapere se c'è una corrispondenza effettiva tra ciò che consegue dalle premesse e ciò che è vero nelle strutture che interpretano tali premesse.

Per verificare questa corrispondenza, dobbiamo mostrare che:

(i) l'insieme delle tautologie coincide con l'insieme dei teoremi

  sse  ;

(ii) ciò che deriva da un insieme   è vero in tutti i modelli di  

  sse  .

La proprietà al punto i è detta correttezza e completezza debole, mentre quella al punto ii è detta correttezza e completezza forte. In effetti, per le logiche in cui, come nel nostro caso, vale un teorema di compattezza e di deduzione, i due enunciati sono equivalenti:   può essere scritto come  , dove   è la congiunzione delle formule di  .

Dire che l'insieme dei teoremi è parte dell'insieme delle tautologie assicura che l'apparato deduttivo è corretto, non può infatti dimostrare formule non valide o contraddittorie. Dire che l'insieme delle tautologie è parte dell'insieme dei teoremi assicura che l'apparato deduttivo è completo, cioè che tutte le formule valide sono dimostrabili.

L'insieme dei teoremi del sistema deduttivo hilbertiano può essere definito induttivamente: esso è l'insieme generato dagli schemi di assioma e chiuso rispetto alle regole di MP e SU. Pertanto, la correttezza si può dimostrare induttivamente.

Più difficile da dimostrare è invece la completezza, perché l'insieme delle tautologie non è definito induttivamente.

Teorema di correttezza

modifica
  implica  .

Dimostrazione

modifica

È sufficiente dimostrare che:

  1. gli schemi a, b e c sono tautologie;
  2. MP e SU sono chiusi rispetto alla conseguenza logica. Ovvero, se   e   sono soddisfatte da  , anche   è soddisfatta da  , e se   è una tautologia, anche   lo è.
  3. Ogni formula di una dimostrazione per   da   è soddisfatta da  .

La verifica che a, b e c sono tautologie è banale.

Verifichiamo che MP è chiuso rispetto alla conseguenza logica. Supponiamo per assurdo che   e  , ma  . Se  , allora esiste un modello   tale che   e  ; ma   è soddisfatta da  , perciò è verificata in  . Pertanto,   e   e, per definizione di implicazione,  . Dunque, essendo che  ,  ; contraddizione.

Per quanto riguarda la SU, sia   una tautologia. Allora,   per qualunque assegnazione booleana alle lettere proposizionali di  , in particolare a  ; dunque, per qualunque proposizione   possiamo porre  . Per il teorema del rimpiazzamento,  , da cui segue  .

Dimostriamo ora il punto 3. Sia   una dimostrazione da   per  . Procediamo per induzione completa.

(Passo base)   vale sse, per ogni modello  , se   allora  .   oppure   è un assioma. Se  , allora abbiamo   per definizione di modello; se   è un'istanza di assioma, allora, essendo SU chiuso rispetto alla conseguenza logica,  , dunque  .

(Passo induttivo) Supponiamo vero per ogni   che  . Se   o   è un'istanza di assioma, allora, come sopra,  . Se   è stato derivato mediante MP, lo si è ottenuto da  ,  ,  , ma per ipotesi induttiva   e  , pertanto, essendo MP chiuso rispetto alla conseguenza logica,  .

Teorema di completezza

modifica
  implica  .

Per dimostrare il teorema di completezza, ci serviamo dei seguenti lemmi.

Lemma 1

modifica

Sia   un insieme di formule e sia   una formula.   sse   è inconsistente.

Dimostrazione

( ) Supponiamo che  . Allora, per monotonia,  . Dal momento che, per inclusione,  ,   è inconsistente.

( ) Supponiamo che   sia inconsistente. Allora da esso è possibile derivare qualsiasi formula, dunque abbiamo che  . Per il teorema di deduzione, si ha che  . Essendo   un teorema, per MP otteniamo  .

Lemma 2

modifica

Se   è un insieme di formule consistente, allora, per ogni formula  ,   oppure   è consistente.

Dimostrazione

Supponiamo, per assurdo, che   sia consistente, ma sia   che   siano inconsistenti. Siccome   è inconsistente, per il lemma 1 abbiamo che  . Ma, essendo pure   inconsistente, abbiamo anche  . Dunque,   è inconsistente; contraddizione.

Lemma 3

modifica

Sia   un insieme di formule. Se   è insoddisfacibile, allora   è inconsistente.

Dimostrazione

Dimostriamo la tesi in forma contrappositiva: se   è consistente, allora   è soddisfacibile.

Supponiamo che   sia consistente.

Sia   l'enumerazione di tutte le formule del linguaggio  . Definiamo, per induzione, una sequenza di insiemi di formule:

 

 

Per ogni  , l'esistenza di   è giustificata dal lemma 2 e, per costruzione, ogni   è consistente.

Sia  . Osserviamo che

  1.  , per costruzione.
  2.   è massimale, cioè, per ogni formula  ,   o la sua negazione appartengono a  . Infatti, siccome l'enumerazione delle formule è completa, per costruzione dei  , presa una qualunque  , esisterà un   per cui  , quindi   oppure  .
  3. Ciascun   è consistente (per induzione:   è consistente; il passo induttivo è giustificato dal lemma 2).
  4.   è consistente. Supponiamo per assurdo che non lo sia. Allora esiste una formula   tale che   e  . Quindi, per compattezza, esistono due insiemi finiti   tali che   e  . Per costruzione, abbiamo che   oppure  . Se  , per monotonia si ha che  , dunque   è inconsistente, contraddizione con il punto 3. Viceversa, se  , per monotonia si ha che  , dunque   è inconsistente, contraddizione con il punto 3.
  5. Per ogni formula  ,   sse  . Supponiamo che  . Allora, essendo   massimale, abbiamo che  . Supponiamo per assurdo che  , ma  . Allora, per inclusione, si ha che   e  , dunque,   è inconsistente. Contraddizione con il punto 4.
  6. Per ogni formula  , se   allora  . Supponiamo per assurdo che  , ma  . Allora, per il punto 5, abbiamo che  , quindi, per inclusione,  , dunque,   è inconsistente. Contraddizione con il punto 4.
  7. Per ogni formula   e  ,   sse   o  . Supponiamo per assurdo che  ,   e  . Per inclusione, abbiamo che   e  , pertanto, per MP,   e, per il punto 6,  ; contraddizione. Se  , allora, per il punto 5,  . Per inclusione, abbiamo che  . Essendo   un teorema, per MP otteniamo  , dunque  . Se  , allora, per inclusione, abbiamo  . Per monotonia, si ha che  , quindi, per il teorema di deduzione, otteniamo  , dunque  .

Dobbiamo ora mostrare che   è soddisfacibile. Per far questo, costruiamo un modello per esso. Definiamo il modello   come:

 

dove   è l'insieme dei simboli proposizionali del linguaggio. Dimostriamo ora, per induzione strutturale sulle formule, che per ogni formula  :

  sse  .

(Passo base) Per costruzione di  .

(Passo induttivo) Sia  . Abbiamo che   sse   (per definizione) sse   (per ipotesi induttiva) sse   (per il punto 5).

Sia  . Abbiamo che   sse  o   (per definizione) sse   o   (per ipotesi induttiva) sse   (per il punto 7).

Abbiamo quindi mostrato che   è un modello per  ; siccome  , abbiamo che  , ovvero   è soddisfacibile.

Dimostrazione

modifica

Supponiamo che  . Allora, per il teorema di soddisfacibilità,   è insoddisfacibile e, per il lemma 3, è anche inconsistente. Dunque, per il lemma 1,  .

Regole derivate

modifica

Le seguenti sono regole derivate dal MP e gli schemi di assioma, per permettere di utilizzare agevolmente il sistema di Hilbert.

Regola di deduzione
modifica

 

Equivalente al teorema di deduzione.

Regola di contrapposizione
modifica

 

Si deriva dallo schema c con il teorema di deduzione.

Regola di transitività
modifica

 

Corrisponde al sillogismo ipotetico.

Regola di scambio delle premesse
modifica

 

Dimostrazione

  1.  : ipotesi;
  2.  : teorema di deduzione su 1;
  3.  : teorema di deduzione su 2;
  4.  : teorema di deduzione su 3;
  5.  : teorema di deduzione su 4.

Dunque,   sse  .

Regola dello Pseudo-Scoto
modifica

 

Dimostrazione

Da   (teorema dello Pseudo-Scoto), per il teorema di deduzione, si ha che  .

Consequentia mirabilis
modifica

 

Dimostrazione

  1.  : ipotesi;
  2.  : SU sul teorema dello Pseudo-Scoto;
  3.  : SU in b;
  4.  : MP tra 2 e 3;
  5.  : MP tra 1 e 4;
  6.  : contrapposizione di 5;
  7.  : MP tra 1 e 6.

Quindi,  . Dunque, per il teorema di deduzione,  .

Eliminazione della doppia negazione
modifica

 

Dimostrazione

  1.  : ipotesi;
  2.  : SU sul teorema dello Pseudo-Scoto;
  3.  : MP tra 1 e 2;
  4.  : Consequentia mirabilis;
  5.  : MP tra 3 e 4.

Dunque,  , quindi, per il teorema di deduzione,  .

Introduzione della doppia negazione

modifica

 

Dimostrazione

  1.  : eliminazione della doppia negazione;
  2.  : SU in 1 con   al posto di  ;
  3.  : contrapposizione di 2;
  4.  : teorema di deduzione su 3.

Modus Tollens

modifica

 

Dimostrazione

  1.  : ipotesi;
  2.  : ipotesi;
  3.  : eliminazione della doppia negazione;
  4.  : sillogismo ipotetico tra 3 e 1;
  5.  : introduzione della doppia negazione;
  6.  : sillogismo ipotetico tra 4 e 5;
  7.  : contrapposizione di 6;
  8.  : MP tra 2 e 7.

Dunque,  .

Applicando il teorema di deduzione, abbiamo la contrapposizione all'inverso:  .

Esempi di dimostrazioni

modifica

Riflessività dell'implicazione

modifica

Dimostriamo che  .

  1.  : SU sullo schema b con   al posto di   e  ,   al posto di  ;
  2.  : SU in a con   al posto di   e   al posto di  ;
  3.  : MP tra 1 e 2;
  4.  : SU in a con   al posto di   e   al posto di  ;
  5.  : MP tra 3 e 4.

Sillogismo ipotetico

modifica

Dimostriamo che  .

  1.  : ipotesi;
  2.  : ipotesi;
  3.  : MP tra 1 e 2;
  4.  : ipotesi;
  5.  : MP tra 3 e 4.

Così abbiamo dimostrato che  .

Applicando il teorema di deduzione (se   allora  ), otteniamo il risultato voluto, eliminando   dalle ipotesi che abbiamo utilizzato.

Teorema dello Pseudo-Scoto

modifica

Dimostriamo che  .

  1.  : ipotesi;
  2.  : SU in a;
  3.  : MP tra 1 e 2;
  4.  : contrapposizione di 3.

Abbiamo dimostrato che  . Dunque, per il teorema di deduzione,  .