Logica/Calcolo delle proposizioni
Wikibooks, manuali e libri di testo liberi.
Il nostro studio della logica partirà del punto più semplice: la logica delle proposizioni. In questo contesto non viene analizzato come si perviene al valore di verità delle formule atomiche e si studiano i connettivi logici e le loro proprietà.
Indice |
[modifica] Formule ben formate
Il primo passo è definire il linguaggio che adopereremo e quindi studiare come i valori di verità possono essere dedotti e si propagano da frasi semplici a formule sempre più complesse.
Per costruire una formula nel calcolo delle proposizioni dobbiamo definire con precisione le regole di formazione.
Partiamo da una serie di formule atomiche che indicheremo con le lettere miuscolo dell' alfabeto: A,B,C....
Queste formule di base rappesentano frasi del tipo:
- "Oggi splende il sole"
- "Mi chiamo Giovanni"
- "Tre è dispari"
cioè frasi che possono essere vere o false. Queste saranno gli atomi delle nostre formule.
Vediamo ora come comporre frasi più complesse partendo dalle frasi atomiche.
- Se A è una frase,
A è una frase. - Se A e B sono frasi, A → B è una frase.
- Se A e B sono frasi, A ∨ B è una frase.
- Se A e B sono frasi, A ∧ B è una frase.
- Se A è una frase, (A) è una frase.
Queste regole 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.
Esempi di frasi ben formate:
- ((A → B) ∧ (C → D)) → ((A ∧ C) → (B ∧ D))
- A → A
- A → B ∨ C
mentre frasi invalide sono:
- A (B)
- → A → B
- A →∧ B
Queste regole definiscono la sintassi che utilizzeremo per il calcolo delle proposizioni. Ora dobbiamo dare un significato a queste frasi.
[modifica] Tavole di verità
Definiamo come operano questi connettivi e lo faremo utilizzando le tavole di verità. Questo ci porterà a definire una semantica per i nostri operatori, cioè a dare un significato all' operazione che viene eseguita.
Le variabili atomiche sono sentenze che hanno un valore di verità, cioè che possono valere vero o falso e che normalmente indicheremo con T e F.
Ora definiamo come i connettivi operano sul valore di verità di una sentenza.
La negazione (not) funziona in questo modo:
| A | A |
|---|---|
| Vero | Falso |
| Falso | Vero |
questo tipo di tabella è la tabella di verità che definisce la semantica dell' operazione di negazione.
Se la frase A è vera la sua negazione è falsa, se la frase A è falsa la sua negazione è vera.
Diamo ora le tabelle di verità degli altri tre connettivi, questa volta basati su due sentenze e quindi con quattro combinazioni possibili.
L' implicazione:
| A | B | A → B |
|---|---|---|
| Vero | Vero | Vero |
| Vero | Falso | Falso |
| Falso | Vero | Vero |
| Falso | Falso | Vero |
Notiamo che se una sentenza vera implica un' altra sentenza vera, allora la sentenza composta unendo queste due frasi con il segno di implicazione è anch' essa vera. Una premessa (la prima sentenza falsa) può implicare quello che vuole, e la frase completa è vera. Il senso di questo è che affermazioni del tipo "se sono Napoleone allora oggi piove" sono sempre vere. Una premessa vera che porta and una conseguenza falsa invece rende non vera L' implicazione.
La congiunzione:
| A | B | A ∧ B |
|---|---|---|
| Vero | Vero | Vero |
| Vero | Falso | Falso |
| Falso | Vero | Falso |
| Falso | Falso | Falso |
cioè la sentenza che congiunge le due frasi è vera se lo sono entrambe le due sentenze che vengono unite.
La disgiunzione:
| A | B | A ∨ B |
|---|---|---|
| Vero | Vero | Vero |
| Vero | Falso | Vero |
| Falso | Vero | Vero |
| Falso | Falso | Falso |
In questo caso la sentenza di disgiunzione è vera se anche solo una delle due sentenze che la compongono è vera.
[modifica] Espressioni e Tavole di verità
Le tavole di verità sono utili per studiare il valore anche di espressioni complesse.
Proviamo per esempio a scrivere la tavola di verità di una espressione più complessa come (A → B) ∨ (B → A). In questa tabella T stà per Vero (True) e F per Falso, per avere una presentazione più compatta.
| A | B | A → B | B → A | (A → B) ∨ (B → A) |
|---|---|---|---|---|
| Vero | Vero | T | T | T |
| Vero | Falso | F | T | T |
| Falso | Vero | T | F | T |
| Falso | Falso | T | T | T |
L' espressione è stata valutata per passi, prima le sottoespressioni (le due implicazioni) e quindi la disgiunzione finale, applicando l' operatore OR ai risultati intermedi.
La colonna finale ci da come valore sempre Vero, quindi questa frase è vera indipendentemente dal valore che assumono le due sentenze A e B. Questo tipo di frasi sempre vere vengono chiamate Tautologie.
[modifica] Algebra delle Proposizioni
Le proposizioni possono essere manipolate con delle semplici regole algebriche, che mantengono inalterato il valore di verità della proposizione.
Vediamo con un semplice esempio come può essere manipolata una proposizione:
A può essere trasformato in A
Il valore di verità della prima proposizione coincide con quello della seconda. Negando un negazione si torna infatti al valore originale. Per verificare se la trasformazione è corretta basta sviluppare la tavola di verità delle due sentenze e controllare se ogni riga ha lo stesso valore.
Vediamo alcune trasformazioni valide nella manipolazioni delle sentenze.
 |
 |
 |
eliminazione della doppia negazione |
 |
|
 |
trasformazione dell' implicazione in disgiunzione |
 |
|
 |
legge di deMorgan per la congiunzione |
 |
|
 |
legge di deMorgan per la disgiunzione |
 |
|
 |
associatività della congiunzione |
 |
|
 |
associatività della disgiunzione |
 |
|
 |
distribuzione della congiunzione sulla disgiunzione |
 |
|
 |
distribuzione della disgiunzione sulla congiunzione |
 |
|
 |
assorbimenti nella disgiunzione |
 |
|
|
|
 |
|
|
|
 |
|
|
assorbimenti nella congiunzione |
 |
|
 |
|
 |
|
|
[modifica] Soddisfacibilità
Una sentenza viene detta soddisfacibile quando un assegnamento di valori alle frasi atomiche che la compongono porta ad un valore di Vero per tutta la sentenza. Le sentenze che risultano sempre vere indipendentemente dal valore di verità che viene assegnato alle frasi atomiche vengono dette tautologie.
Introduciamo un nuovo simbolo 
, per indicare che una sentenza è soddisfacibile. Alla sinistra elenchiamo le proposizioni che devono essere vere, alla destra la proposizione che viene soddisfatta da queste condizioni.
indica che B è vera quando A è vera, o meglio che da A posso derivare (semanticamente) B. Un modo alternativo per indicare questo fatto è dire che A è un modello per B; forse poco comprensibile nel contesto del calcolo proposizionale, vedremo in seguito come invece sia molto importante nel calcolo dei predicati.
indica che A è una tautologia perché non ha bisogno di nessuna condizione per essere vera.
Per esempio:
La soddisfacibilità è un problema di semplice soluzione: basta isolare le frasi atomiche e quindi creare tutte le possibili combinazioni. verificare per via semantica se una sentenza è valida o meno è quindi facile, ma non computazionalmente economico. Se la sentenza da analizzare ha 10 frasi atomiche ci sono 2^10 = 1024 combinazioni da testare.
Per questa proprioetà quindi il calcolo proposizionale è decidibile, cioè esiste una procedura che termina che permette di decidere se una sentenza è vera o falsa.
Il problema della soddisfacibilità del calcolo proposizionale (SAT) ha degli aspetti molto interessanti per la teoria della complessità computazionale (vedi P=NP)
[modifica] Teorema di deduzione
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.
è equivalente a 
cioè il teorema dice che se A è un modello per B allora A → B è una tautologia.
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.
[modifica] Teoria della dimostrazione
Come abbiamo visto nel paragrafo precedente il calcolo delle proposizioni è decidibile ed abbiamo un algoritmo (le tavole di verità) per verificare se una sentenza è soddifacibile. 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 A è vera anche B è vera, mentre
significa che se A è vera possiamo costruire una dimostrazione di B.
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.
[modifica] Consistenza e completezza di un sistema
Ogni sistema di dimostrazione per essere un buon sistema deve avere due proprietà: essere consistente ed essere completo.
La proprieta di consistenza è:
cioè se posso dimostrare Φ con il sistema S, allora Φ è un teorema per il calcolo delle proposizioni. In poche parole tutto quello che può essere provato da S è vero.
La proprietà di completezza è:
cioè se una proposizione è vera posso dimostrarla utilizzando S.
[modifica] I principali sistemi di dimostrazione
- Il sistema di Frege-Hilbert
- La deduzione naturale
- Il calcolo dei sequenti
- I tableaux semantici
- La risoluzione
[modifica] Completezza
Il calcolo delle proposizioni è un sistema completo, cioè ogni formula vera è dimostrabile.
Questo risultato unisce due concetti completamente diversi tra loro, quello di verità, concetto semantico e legato all' universo che stiamo esplorando, con quello di dimostrazione, concetto sintattico e legato alla manipolazione dei simboli che costituiscono le proposizioni.
