Logica matematica/Calcolo delle proposizioni

Wikibooks, manuali e libri di testo liberi.
Jump to navigation Jump to search
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]

Viewmag.png 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]

Viewmag.png 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]

Viewmag.png 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]

Viewmag.png 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:

mentre frasi invalide sono:

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]

Searchtool.svg Per approfondire, vedi Tutti i connettivi.

Viewmag.png Definizione

Il sistema di valutazione della logica proposizionale è definito da

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

Negazione[modifica]

Viewmag.png 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]

Viewmag.png Definizione

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

Disgiunzione[modifica]

Viewmag.png 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]

Viewmag.png 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]

Viewmag.png 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]

Viewmag.png 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]

Viewmag.png 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]

Viewmag.png Definizione

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

Formula soddisfacibile[modifica]

Viewmag.png Definizione

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

Tautologia[modifica]

Viewmag.png Definizione

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

Contraddizione[modifica]

Viewmag.png 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]

Viewmag.png Definizione

Diciamo che implica logicamente sse ogniqualvolta anche .

Equivalenza logica (Definizione)[modifica]

Viewmag.png 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 .

Viewmag.png 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]

Viewmag.png Definizione

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

Contromodello per una formula[modifica]

Viewmag.png Definizione

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

Modello per un insieme di formule[modifica]

Viewmag.png 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]

Viewmag.png Definizione

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

Soddisfacibilità[modifica]

Viewmag.png Definizione

Se per qualche , allora diciamo che è soddisfacibile.

Insoddisfacibilità[modifica]

Viewmag.png 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]

Viewmag.png 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]

Viewmag.png 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]

Viewmag.png 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]

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

Viewmag.png 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]