Logica matematica/Calcolo delle proposizioni

Indice del libro


Partiremo dal punto più semplice: la logica proposizionale, ovvero relativa alle proposizioni. In questo contesto si studiano funzionamento e proprietà dei connettivi logici, e non si analizza come si arriva al valore di verità delle formule atomiche.

Il potere espressivo di questo linguaggio è limitato: in esso, infatti, possiamo esprimere proposizioni che sono vere o false, ma non proprietà che possono valere o meno su uno/molti/tutti gli individui di una certa classe. Col basso potere espressivo si coniuga la decidibilità di questa logica. Presentiamo la sintassi e la semantica della logica proposizionale.

Sintassi modifica

Introduciamo la nozione di linguaggio proposizionale   costruito su un alfabeto  . Iniziamo con la definizione di alfabeto.

Alfabeto modifica

  Definizione

Un alfabeto   è costituito da:

  • i connettivi proposizionali   (unario) e   (binari);
  • le costanti proposizionali   (per denotare il vero e il falso);
  • un insieme non vuoto (finito o numerabile) di simboli proposizionali  ;
  • i simboli separatori   e  .

Nel seguito scriveremo   quando   è chiaro dal contesto. Definiamo ora le formule di  .

Formule ben formate modifica

  Definizione

L'insieme PROP delle formule ben formate o formule del linguaggio proposizionale   è l'insieme definito induttivamente come segue:

  1. le costanti e i simboli proposizionali sono formule;
  2. se   è una formula,   è una formula;
  3. se   è un connettivo binario (cioè  ) e se   e   sono due formule,   è una formula.

Le costanti e i simboli proposizionali sono anche detti atomi, le loro negazioni sono dette atomi negati. Gli atomi e gli atomi negati sono anche detti letterali. Gli atomi negati sono talvolta detti letterali negativi. Una formula del linguaggio proposizionale è anche detta proposizione o enunciato proposizionale.

Data una formula   di PROP, ogni formula   che appare come componente di   è detta sottoformula di  . La definizione di sottoformula, di connettivo principale e di sottoformula immediata è la seguente.

Sottoformule modifica

  Definizione

Sia   una formula di PROP, l'insieme delle sottoformule di   è definito come segue:

  1.   stessa è una sottoformula di  ;
  2. se   è una formula del tipo  , allora le sottoformule di   sono anche sottoformule di  ;   è detto connettivo principale e   sottoformula immediata di  ;
  3. se   è una formula del tipo  , dove   è un connettivo binario (cioè  ), e   e   due formule, le sottoformule di   e   sono anche sottoformule di  ;   è detto connettivo principale;   e   sottoformule immediate di  .

Per evitare un uso eccessivo delle parentesi, introduciamo anche delle regole di precedenza tra i connettivi. Per le formule proposizionali, si usa la seguente convenzione: la massima precedenza a  , poi, nell'ordine, ai connettivi   e infine a  . Questo significa che, in assenza di parentesi, una formula ben formata va parentesizzata privilegiando le sottoformule i cui connettivi principali hanno precedenza più alta. A parità di precedenza, cioè se siamo in presenza di più occorrenze dello stesso connettivo, si assume che esso associ a destra, cioè la parentesizzazione va eseguita a partire dall'ultima occorrenza a destra del connettivo.

Simboli proposizionali occorrenti in una formula modifica

  Definizione

La funzione

 

su PROP nell'inseme potenza di   è definita ricorsivamente come segue:

  •   se  ;
  •  ;
  •  ;
  •  ;
  •  , dove  .

La funzione   restituisce l'insieme dei simboli proposizionali che occorrono in una formula. Essa è definita in  , cioè nell'inseme dei sottoinsiemi di  , dato che restituisce sempre un sottoinsieme di  .

Esempi modifica

Le regole appena esposte indicano come formare le frasi del calcolo proposizionale. Le frasi ben formate nascono applicando a formule atomiche i connettivi logici come indicato, se non è possibile risalire a queste regole la frase non è una frase ben formata.

Le formule atomiche rappresentano frasi del tipo:

  • "Oggi splende il sole"
  • "Mi chiamo Giovanni"
  • "Tre è dispari"

cioè frasi che possono essere vere o false. Da esse verranno poi costruite le formule ben formate.

Esempi di frasi ben formate:

  1.  
  2.  
  3.  

mentre frasi invalide sono:

  1.  
  2.  
  3.  

I vari connettivi

Queste regole definiscono la sintassi che utilizzeremo per il calcolo delle proposizioni. Ora dobbiamo dare un significato a queste frasi.

Semantica modifica

Dobbiamo definire come operano questi connettivi e lo faremo usando le tavole di verità. In questo modo potremo creare una semantica, ovvero dare un significato all'operazione che viene eseguita da ogni operatore.

Ci serviremo di variabili atomiche, ovvero indivisibili, che possono assumere solo valori di verità (vero o falso rispettivamente indicati con V o F o, se ci basiamo sulla lingua inglese T o F).

Sistema di valutazione modifica

  Per approfondire, vedi Tutti i connettivi.

  Definizione

Il sistema di valutazione   della logica proposizionale è definito da

  1.  
  2.  ;
  3.  , uno per ognuno dei connettivi del linguaggio  , con:
    •  ;
    •  ,  .

Negazione modifica

  Definizione

La funzione   della logica proposizionale è definita come segue:

  •  
  •  

Questo è di solito espresso in maniera concisa come:

  •  
  •  

cioè, la funzione di valutazione associata a un connettivo viene indicata col simbolo stesso del connettivo, e viene definita in forma tabellare mediante la tavola o tabella dei valori di verità per il connettivo come segue:

 

Tale tabella definisce la semantica dell'operazione di negazione. Se la frase   è vera, la sua negazione è falsa; se la frase   è falsa, la sua negazione è vera. Si tratta dell'unico connettivo unario, in quanto agisce su un'unica sentenza.

Evitando di presentare le funzioni   della logica proposizionale per i connettivi binari, le presentiamo subito in forma di tabella dei valori di verità.

Congiunzione modifica

  Definizione

 

Il connettivo di congiunzione   viene definito in modo che   è vero se sia   che   (i due congiunti) sono veri, quindi  .

Disgiunzione modifica

  Definizione

 

Il connettivo di disgiunzione   viene definito in modo che   è vero se   oppure   (uno dei due disgiunti) sono veri, quindi  . Si noti che, con questa definizione,   è la disgiunzione inclusiva, cioè corrisponde al "vel" latino e non all'"aut".

Implicazione modifica

  Definizione

 

La definizione della semantica del connettivo di implicazione   (detta implicazione materiale, in cui   è detto premessa e   conseguenza) è, in un certo senso, meno intuitiva. Innanzi tutto si noti che, con la definizione data, si ha che   è sempre vero, qualunque sia il valore di verità di  ; questo corrisponde alla nostra intuizione. Possiamo quindi accettare il fatto che, affinché   sia vero, basta che   sia vero, indipendentemente dal valore di verità di  . Questo di fatto ci dice che, se   è vero e   è vero, possiamo "rafforzare" la premessa sostituendo a   un qualunque   e l'implicazione resta vera. In sostanza, l'implicazione è falsa nel solo caso in cui la premessa è vera e la conseguenza è falsa.

Doppia implicazione modifica

  Definizione

 

La definizione della semantica del connettivo di doppia implicazione è del tutto intuitiva: il valore di verità di   è vero se i valori di verità di   e   coincidono.

Assegnazione booleana modifica

  Definizione

Un'assegnazione booleana   ai simboli proposizionali   è una funzione totale

 

Per il fatto che l'insieme delle formule proposizionali è liberamente generato, ogni assegnazione   si estende a un'unica interpretazione o valutazione booleana.

Valutazione booleana modifica

  Definizione

Una valutazione booleana

 

è l'estensione a PROP di un'assegnazione booleana, cioè

  •   se  ;
  •  ;
  •  ;
  •  ;
  •  .

dove  . Data un'assegnazione booleana  , l'esistenza e l'unicità dell'estensione   sono garantite dal teorema di ricorsione.

Il valore di verità di una formula   dipende dall'assegnazione booleana a tutti i simboli proposizionali, inclusi quelli che non occorrono in  . Tuttavia, per dare una valutazione booleana di   basta dire come vengono valutati (interpretati) i simboli proposizionali di  . Infatti, sia   una formula proposizionale e sia   l'insieme dei simboli proposizionali che occorrono in  , per essi vale la seguente proprietà.

Teorema di equivalenza delle valutazioni modifica

Se   e   sono due assegnazioni che coincidono su  , allora  .

Dimostrazione Procediamo per induzione strutturale.

  • (Passo Base) Osserviamo che l'asserto è vero per le formule   e   perché non contengono simboli proposizionali. Se  , allora abbiamo   e, per definizione,  . Pertanto l'asserto vale per i simboli proposizionali.
  • (Passo Induttivo) Sia  . Abbiamo per   e   che   e   e dunque, poiché per ipotesi induttiva  , segue che  . Analogamente, sia   con  ; abbiamo   e   e, per ipotesi induttiva,   e  , segue che  .

Soddisfacibilità modifica

Formula soddisfatta modifica

  Definizione

Una formula della logica proposizionale   è soddisfatta da una valutazione booleana   sse  .

Formula soddisfacibile modifica

  Definizione

Una formula della logica proposizionale   è soddisfacibile sse è soddisfatta da una qualche valutazione booleana  .

Tautologia modifica

  Definizione

Una formula della logica proposizionale   è tautologica, ossia è una tautologia, sse è soddisfatta da ogni valutazione booleana  .

Contraddizione modifica

  Definizione

Una formula della logica proposizionale   è contraddittoria, ossia è una contraddizione, sse non è soddisfatta da alcuna valutazione booleana  .

Tavole di verità modifica

Dal teorema di equivalenza delle valutazioni segue che, per determinare se una formula proposizionale   è soddisfacibile, tautologica o contraddittoria, basta costruire una tabella di valori di verità in cui compaiono   colonne, dove   è il numero di simboli proposizionali distinti   che compaiono in   e nella n+1-esima colonna viene riportato il corrispondente valore  . La tabella ha   righe, tante quante sono le possibili assegnazioni distinte di valori di verità ai simboli di  .

 

  è una tautologia sse l'ultima colonna contiene solo  , è soddisfacibile sse essa contiene almeno una  , è contraddittoria sse essa contiene tutte  .

Teorema modifica

Una formula   è una tautologia sse   è una contraddizione.

Dimostrazione

( ) Sia   una tautologia. Per definizione, per ogni valutazione booleana   si ha che  . Ora, per   si ha che:

 

quindi, per ogni valutazione booleana   si ha che:

 

dunque,   è una contraddizione.

Procedendo all'inverso, si dimostra analogamente che, se   è una contraddizione, allora   è una tautologia:

( ) sia   una contraddizione. Per definizione, per ogni valutazione booleana   si ha che  . Ora, per   si ha che:

 

quindi:

 

da cui, per la definizione di  , si deduce che, per ogni valutazione booleana  :

 

dunque,   è una tautologia.

Equivalenza logica modifica

Implicazione logica modifica

  Definizione

Diciamo che   implica logicamente   sse ogniqualvolta   anche  .

Equivalenza logica (Definizione) modifica

  Definizione

Diciamo che due proposizioni   e   sono logicamente equivalenti o tautologicamente equivalenti sse   per ogni valutazione booleana  . In tal caso scriviamo  .

Diamo qui di seguito una lista di formule tautologicamente equivalenti. L'equivalenza può essere facilmente verificata tramite tavole di verità.

      idempotenza della congiunzione
      idempotenza della disgiunzione
      associatività della congiunzione
      associatività della disgiunzione
      associatività della doppia implicazione
      commutatività della congiunzione
      commutatività della disgiunzione
      commutatività della doppia implicazione
      distributività della congiunzione sulla disgiunzione
      distributività della disgiunzione sulla congiunzione
      assorbimento della congiunzione sulla disgiunzione
      assorbimento della disgiunzione sulla congiunzione
      neutralità del vero nella congiunzione
      assorbimento del vero nella disgiunzione
      neutralità del falso nella disgiunzione
      assorbimento del falso nella congiunzione
      doppia negazione
      legge di De Morgan per la congiunzione
      legge di De Morgan per la disgiunzione
      terzo escluso
      contraddizione
      contrapposizione
      trasformazione dell'implicazione in disgiunzione


Esercizi ed esempi

Relativamente alla legge del terzo escluso, il fatto che   sia sempre vero sembra del tutto intuitivo. In effetti, questa è una caratteristica della logica classica; in altre logiche, per esempio nella logica intuizionista, questo fatto non vale.

Intuitivamente ci si aspetta che, se una proposizione   è logicamente equivalente a una proposizione  , sostituendo   al posto di   in una formula  , il valore di verità di   non cambi.

Cerchiamo ora di rendere più precisa questa nozione. Indichiamo con   una formula proposizionale che può contenere delle occorrenze del simbolo   (detto metavariabile o parametro proposizionale, cioè   sta ad indicare un atomo). Con la notazione   indicheremo la formula  , in cui tutte le occorrenze di   sono state uniformemente e simultaneamente sostituite con occorrenze di una formula  . Chiameremo quest'operazione sostituzione uniforme.

Primo teorema del rimpiazzamento modifica

Siano  ,   e   formule proposizionali e sia   una valutazione booleana. Se  , allora

 .

Dimostrazione Per induzione strutturale. Osserviamo innanzitutto che, se   non occorre in  , nessuna sostituzione è stata fatta, e quindi l'asserto è banalmente verificato.

(Passo Base) Supponiamo che  , allora   e  ; per ipotesi,  , e dunque  .

(Passo Induttivo) Sia  . Osserviamo che, per definizione di valutazione booleana:

 .

Per ipotesi induttiva:  .

Quindi  .

Di nuovo, per definizione di valutazione booleana:

 .

Dunque  .

Analogamente, sia  , con  . Osserviamo che, per definizione di valutazione booleana:

 .

Per ipotesi induttiva:   e  .

Quindi  .

Di nuovo, per definizione di valutazione booleana:

 .

Dunque  .

Secondo teorema del rimpiazzamento modifica

Se  , allora  .

Dimostrazione Essendo   un'equivalenza logica,   vale per ogni valutazione booleana  ; per il primo teorema del rimpiazzamento, si ha che   vale per ogni valutazione booleana. Ne consegue che  .

Modelli modifica

Possiamo fornire una nozione d'interpretazione basata sulla relazione  .

  Definizione

Sia   un'assegnazione booleana. L'insieme   associato a   è l'insieme dei simboli proposizionali tali che il loro valore di verità in   sia  . Più formalmente:

 

Definiamo la relazione   come segue:

  sse  

  sse  

Osserviamo che, nella definizione di  , stiamo sottintendendo il linguaggio proposizionale  . Nel caso in cui non sia chiaro dal contesto a quale linguaggio ci si riferisce, allora si usa indicare  .

Modello per una formula modifica

  Definizione

Sia   una formula. Se   diciamo che   è un modello di  , ovvero che   rende vera  .

Contromodello per una formula modifica

  Definizione

Sia   una formula. Se   diciamo che   è un contromodello per  , ovvero che   rende falsa  .

Modello per un insieme di formule modifica

  Definizione

Se   rende vere tutte le formule di un insieme  , cioè se   per ogni formula   in  , diciamo che   è un modello per   e indichiamo ciò con  .

Se   è una tautologia, possiamo scrivere  , in quanto   è vera in ogni modello, compreso quello vuoto.

Implicazione logica da un insieme di formule modifica

  Definizione

Dato un insieme di formule   e una formula  , diciamo che   soddisfa  , o implica logicamente  , e scriviamo  , sse (  oppure  ).

Soddisfacibilità modifica

  Definizione

Se   per qualche  , allora diciamo che   è soddisfacibile.

Insoddisfacibilità modifica

  Definizione

Se per nessun insieme di simboli proposizionali   è verificato che  , allora diciamo che   è insoddisfacibile.

Quindi una formula è insoddisfacibile sse per essa non esiste alcun modello.

Il simbolo   è giustificato quando si considerano le nozioni di implicazione logica e di equivalenza logica, perché permettono una semplificazione notazionale.

Infatti, se   implica logicamente   scriviamo   e se   è logicamente equivalente a  , cioè se  , scriviamo  .

Il seguente teorema lega le nozioni di implicazione logica e di insoddisfacibilità:

Teorema di soddisfacibilità modifica

  sse   è insoddisfacibile.

Dimostrazione

( ) Supponiamo che valga  , ma   sia soddisfacibile; allora esiste un modello   tale che   e  , cioè   e  , dunque non vale  , contraddizione.

( ) Supponiamo che   sia insoddisfacibile, ma non valga  ; allora esiste un modello   tale che   e  , cioè   e  , quindi  , dunque   è soddisfacibile, contraddizione.

La proprietà appena enunciata è quella che giustifica le dimostrazioni per assurdo: se si vuole provare che   segue da  , basta assumere   e provare che questo contraddice  .

Compattezza modifica

Segue quanto abbiamo già notato per le valutazioni booleane: quando consideriamo i modelli di una formula, basta prendere in considerazione solo quelli in cui compaiono i simboli proposizionali della formula. È chiaro che, se in una formula   occorrono   simboli proposizionali distinti, ovvero  , allora il numero degli insiemi di simboli che ci interessa verificare per conoscere il valore di verità di   è al più  . Tuttavia, è lecito chiedersi cosa succede se abbiamo un insieme infinito   di proposizioni e vogliamo sapere se  .

Il teorema di compattezza della soddisfacibilità fornisce una risposta a questa domanda.

Insieme di formule finitamente soddisfacibile modifica

  Definizione

Un insieme di formule   si dice finitamente soddisfacibile sse ogni suo sottoinsieme finito è soddisfacibile.

Teorema di compattezza della soddisfacibilità modifica

Un insieme di proposizioni   è soddisfacibile sse è finitamente soddisfacibile.

Dimostrazione Per contraddizione.

( ) Supponiamo che   sia soddisfacibile, ma che non sia finitamente soddisfacibile. Allora, esiste un sottoinsieme finito   tale che, per ogni  ,  , con  . Essendo  , allora  , quindi, per ogni   esiste una formula   tale che  . Dunque,   non è soddisfacibile. Contraddizione.

( ) Supponiamo che   sia finitamente soddisfacibile, ma che non sia soddisfacibile. Allora, per ogni   esiste una formula   tale che  . Quindi, esiste un sottoinsieme finito   tale che, per ogni  ,  , con  . Perciò,   non è soddisfacibile, dunque   non è finitamente soddisfacibile. Contraddizione.

Quella qui esposta è una dimostrazione non costruttiva, cioè non fornisce un esempio concreto di ciò che dimostra, ma suppone che la tesi sia falsa e arriva ad una contraddizione. Per una dimostrazione costruttiva, si veda la dimostrazione del teorema di compattezza.

Riformulazione del teorema di compattezza modifica

Il teorema di compattezza può essere enunciato in modo equivalente come segue:

un insieme di proposizioni   è insoddisfacibile sse esiste un sottoinsieme finito   che è insoddisfacibile.

Dimostrazione Per contraddizione.

( ) Supponiamo che   sia insoddisfacibile, ma che non esista un sottoinsieme finito   insoddisfacibile. Allora, ogni sottoinsieme finito   è soddisfacibile, quindi   è finitamente soddisfacibile. Ma, per il teorema di compattezza,   è soddisfacibile. Contraddizione.

( ) Supponiamo che esista un sottoinsieme finito   insoddisfacibile, ma che   sia soddisfacibile. Allora, per il teorema di compattezza,   è finitamente soddisfacibile, quindi ogni sottoinsieme finito   è soddisfacibile, dunque non può esistere un sottoinsieme finito   insoddisfacibile. Contraddizione.

Dal teorema di compattezza seguono delle proprietà interessanti, per esempio il seguente corollario.

Corollario del teorema di compattezza modifica

  sse esiste un sottoinsieme finito   di   tale che  .

Dimostrazione Per contraddizione. Supponiamo che, per ogni   finito,  , e consideriamo le seguenti trasformazioni:

  1.  , per ogni   finito, ipotesi;
  2. sse   è soddisfacibile per ogni   finito (da 1, per il teorema di soddisfacibilità);
  3. sse   è finitamente soddisfacibile (da 2, per definizione di insieme finitamente soddisfacibile);
  4. sse   è soddisfacibile (da 3, per il teorema di compattezza);
  5. sse   (da 4, per il teorema di soddisfacibilità).

Contraddizione.

Teorema di deduzione modifica

Definito il concetto di derivazione semantica, vediamo un importante teorema che permette di ridurre le ipotesi di cui abbiamo bisogno o di sfruttare come ipotesi una parte della sentenza che stiamo analizzando: il teorema di deduzione.

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

  sse  

cioè, il teorema dice che   e   soddisfano   se e solo se   soddisfa  .

Se la cosa può sembrare a prima vista sorprendente, ad una analisi più attenta si può notare come sia la semantica profonda dell'implicazione. Vediamo con un semplice esempio in linguaggio naturale:

da Oggi piove posso derivare ( ) prendo l' ombrello

equivale a:

senza nessuna precondizione posso derivare ( ) se Oggi piove allora ( ) prendo l' ombrello

Questo teorema sarà particolarmente utile nelle dimostrazioni, perché ci permette di spostare a destra o a sinistra del simbolo di derivazione l' antecedente dell' implicazione. Quindi, se dobbiamo dimostrare che A implica B, la strada più semplice sarà supporre A come ipotesi e quindi dimostrare B.

Dimostrazione modifica

Per definizione di implicazione logica su un insieme di formule,   sse, per ogni modello  , (  oppure   oppure  ).

Per definizione di  , (  oppure  ) sse (  oppure  ) sse  . Per definizione di  ,  . Per definizione di  ,   sse  . Dunque,   sse (  oppure  ) sse  .

Completezza di insiemi di connettivi modifica

I connettivi definiscono delle funzioni da   (nel caso del connettivo unario  ), oppure   (nel caso dei connettivi binari) in  . Ciascuna di queste funzioni, dette funzioni booleane, è definita attraverso la relativa tavola dei valori di verità, oppure, equivalentemente, attraverso le funzioni   e  , con  .

Più in generale, ogni formula proposizionale   contenente simboli proposizionali distinti   definisce una funzione booleana da   in  .

Funzione di verità modifica

  Definizione

Sia   una formula della logica proposizionale contenente esattamente   simboli proposizionali distinti  ; la funzione   tale che  , dove   è l'interpretazione per cui   per ogni   è detta la funzione di verità associata ad  .

Quindi, ogni formula del calcolo proposizionale definisce una funzione  -aria (possiamo anche chiamarla connettivo  -ario), dove   è il numero di atomi distinti che in essa compaiono. Si può facilmente verificare che, per ogni  , esistono   funzioni booleane distinte (cioè, tante quanti sono i sottoinsiemi di  ). Quindi, nel caso di   esistono 16 connettivi distinti. Qui ne sono stati introdotti 4 e, come alcune equivalenze logiche introdotte precedentemente hanno mostrato, essi non sono indipendenti, nel senso che alcuni sono esprimibili in termini di altri.

Derivazione di connettivi modifica

  Definizione

Dato un insieme di connettivi   e un connettivo   per cui si abbia una funzione di verità  , si dice che   si deriva da (oppure si definisce in termini dei) connettivi di   se esiste una formula proposizionale   costruita usando solo i connettivi di   tale che  .

Nella logica proposizionale valgono le seguenti equivalenze logiche.

     
     
     
     
     
     
     
     

Si noti che la costante proposizionale   (così come la costante proposizionale  ) può essere considerata come un connettivo  -ario.

Un insieme di connettivi logici è completo se mediante i suoi connettivi si può esprimere qualunque funzione booleana. Più formalmente diciamo che:

Insieme funzionalmente completo modifica

  Per approfondire, vedi Dimostrazione di completezza di insiemi di connettivi.

  Definizione

Un insieme di connettivi logici   si dice funzionalmente completo sse, data una qualunque   esiste una formula proposizionale   costruita mediante i connettivi dell'insieme   tale che  .

In particolare, un insieme di connettivi logici è completo se mediante i suoi connettivi si può esprimere qualunque altro connettivo.

È facile verificare che l'insieme dei connettivi   è completo, così come lo sono   e anche  .

Questo ci porta a concludere che nella trattazione della logica potremmo ridurci a considerare due soli connettivi. Si può in effetti anche dimostrare che un solo connettivo binario può bastare per definire tutti gli altri; in particolare, un connettivo a scelta tra il "nand" o il "nor" costituisce un insieme completo. Si può anche dimostrare che nand e nor sono gli unici due connettivi binari completi.

Usare un minor numero di connettivi nelle formule porterebbe sicuramente a una maggiore stringatezza nelle dimostrazioni date per casi sui singoli connettivi, ma nuocerebbe gravemente alla leggibilità delle formule stesse. Le equivalenze sopra mostrate ne forniscono evidenza. Si è quindi preferito la leggibilità alla concisione.

Decidibilità modifica

La logica proposizionale è decidibile. In effetti, la logica proposizionale si chiama calcolo delle proposizioni perché esiste una procedura effettiva che stabilisce se una proposizione   è una tautologia o meno. Nel caso del calcolo proposizionale, possiamo sempre essere in grado di calcolare le formule vere del linguaggio. In verità, come si vedrà nel caso della logica del primo ordine, la dizione calcolo si usa anche qualora si abbia una logica semidecidibile.

Per verificare la decidibilità del calcolo proposizionale siamo interessati a decidere se una formula   del calcolo proposizionale è una tautologia o meno.

Un altro interessante problema di decisione per il calcolo proposizionale consiste nello stabilire se una formula è soddisfacibile o meno (questo problema è di solito indicato con SAT).

Abbiamo visto che, per decidere se   è una tautologia, bisogna verificare le tavole di verità per ogni assegnazione ai simboli proposizionali che occorrono in  ; pertanto, se in   occorrono   simboli proposizionali, sarà sufficiente verificare   casi.

Diciamo che un insieme   di formule è enumerabile se può essere trasformato in una sequenza. Un insieme di formule è effettivamente enumerabile se esiste un metodo per determinare l' -esimo elemento della sequenza, per ogni  .

Lemma di enumerabilità modifica

Se   è effettivamente enumerabile, allora l'insieme delle conseguenze tautologiche di  , ovvero l'insieme   è effettivamente enumerabile.

Dimostrazione modifica

Dobbiamo mostrare che, data una formula  , se  , allora esiste una procedura che risponde SÌ. Consideriamo un'enumerazione   dei sottoinsiemi finiti di  . Data una formula  , consideriamo la lista dei sottoinsiemi finiti di   nel seguente modo:

 

 

 

 

Per il corollario del teorema di compattezza, se   esiste un   finito tale che  , e dunque tale   comparirà nell'enumerazione.

Teoria della dimostrazione modifica

Come abbiamo visto nel paragrafo precedente, il calcolo delle proposizioni è decidibile ed abbiamo un algoritmo (le tavole di verità) per verificare se una sentenza è soddisfacibile. Ora cercheremo dei metodi che ci permettano di dimostrare che una sentenza è valida.

Il metodo delle tabelle di verità è un metodo "semantico", cioè che esplora tutte le possibili configurazioni dell'universo per verificarne lo stato, ora vogliamo costruire dei metodi basati più sulla deduzione che non sull'esplorazione e che si basino sull'attività di costruire derivazioni e dimostrazioni, cioè sul ragionamento e non sulla forza bruta.

Svilupperemo quindi dei metodi puramente sintattici, cioè dei calcoli che trasformano simboli in altri simboli, che ci permetteranno di creare dimostrazioni sulle sentenze logiche.

Introduciamo un nuovo simbolo  , per indicare che da una sentenza possiamo derivare sintatticamente un'altra sentenza.

Abbiamo così due concetti:

 

significa che semanticamente se   è vera anche   è vera, mentre

 

significa che se   è vera possiamo costruire una dimostrazione di  .

Il grande risultato della logica moderna è stato legare tra loro questi due concetti nel teorema di completezza, che vedremo più avanti.

Esploreremo i maggiori sistemi di dimostrazione, tutti con peculiari caratteristiche. Il sistema di Hilbert è quello più simile alla definizione del metodo assiomatico, i sistemi di Gentzen (deduzione naturale e sequenti) tentano di mimare l'attività mentale di un matematico, i tableaux sfruttano la semantica e la risoluzione è il sistema più semplice da realizzare meccanicamente, tanto da essere alla base del linguaggio di programmazione PROLOG.

Il sistema di Hilbert si basa su un insieme di assiomi logici e un insieme di regole di inferenza; i tableaux e la risoluzione invece non fanno uso di assiomi logici, ma solo di regole di inferenza e sono basati sulla refutazione (cioè, per dimostrare che una formula è un teorema si dimostra in effetti che la sua negata è una contraddizione). Tra questi metodi, solo la risoluzione richiede che le formule siano scritte in una forma normale.

Tutti i sistemi deduttivi presentati sono per certi aspetti equivalenti, per tutti infatti vale un teorema di correttezza e completezza, quindi l'insieme di teoremi che si può derivare con ciascuno di essi è lo stesso.

Correttezza e completezza di un sistema modifica

Ogni sistema di dimostrazione, per essere un buon sistema, deve avere due proprietà: essere corretto ed essere completo.

La proprietà di correttezza è:

se   allora  .

cioè, se posso dimostrare   con il sistema  , allora   è una tautologia. In poche parole, tutto quello che può essere provato da   è vero.

La proprietà di completezza è:

se   allora  .

cioè, se una proposizione è una tautologia, posso dimostrarla utilizzando  .

I principali sistemi di dimostrazione modifica