Dimostrazioni e tableaux semantici

1. Che cos'è una dimostrazione

Un argomento è l'affermazione che una conclusione segue da certe premesse. Una dimostrazione è ciò che risolve quell'affermazione: un oggetto finito e controllabile che chiunque può leggere riga per riga e accettare, senza doversi fidare della vostra parola. Il pregio di una dimostrazione non è che convinca - lo fa anche un buon discorso -, ma che ogni suo passo non avrebbe potuto andare diversamente.

È una richiesta più severa di quanto sembri. «Piove, quindi il terreno è bagnato» è una cosa ragionevole da dire, ma si appoggia a ciò che sapete di pioggia e terreno. La logica formale mette da parte tutto questo e pone una domanda più stretta: data la sola forma delle frasi, c'è un modo qualsiasi perché le premesse siano vere e la conclusione falsa? Se non c'è, l'argomento è valido, e la dimostrazione è il resoconto del perché non ce ne sia alcuno.

Questa guida riguarda un modo di produrre quel resoconto: il metodo dei tableaux semantici, detti anche alberi di verità. È il metodo che questo sito usa ogni volta che scrivete un argomento nel calcolatore, e una volta seguito basta una penna per verificare un argomento su carta.

2. Valido, e come accorgersene

Scrivete un argomento con un segno di conseguenza: le premesse a sinistra, la conclusione a destra. L'affermazione p → q, ¬q ⊨ ¬p dice che da un condizionale e dalla negazione del suo conseguente segue la negazione del suo antecedente. Il segno di conseguenza non è un connettivo in più. È un'affermazione sulle formule che lo affiancano, ed è giusta o sbagliata.

La definizione di validità indica subito un modo di metterla alla prova: percorrete ogni assegnazione di vero e falso alle variabili e guardate se una di esse rende vere tutte le premesse e falsa la conclusione. È ciò che fa una tavola di verità, e con due o tre variabili va benissimo. Il guaio è che la tavola cresce come 2ⁿ. Dieci variabili richiedono mille righe, venti un milione, e la tavola non dice nulla su quali righe contassero.

Un tableau affronta la stessa domanda dall'altro capo. Invece di elencare ogni possibilità e cercarne una cattiva, suppone che ne esista una cattiva e prova a costruirla. Se il tentativo crolla in contraddizione su ogni strada possibile, nessuna assegnazione simile esiste e l'argomento è valido. Se il tentativo riesce, ciò che ha costruito è un controesempio che potete leggere direttamente.

3. Il metodo dei tableaux

Un tableau è un albero di formule segnate. Ogni riga è una formula preceduta da una T o da una F, e il segno dice che cosa il ramo suppone di quella formula: non qual è il suo valore di verità, ma quale dovrebbe essere perché l'argomento fallisca. L'intero metodo sta in quattro passi:

1. Scrivete ogni premessa con una T. State supponendo che tutte le premesse dell'argomento valgano.
2. Scrivete la conclusione con una F. State supponendo che fallisca lo stesso: è l'assunzione che volete confutare.
3. Prendete una riga che non sia ancora un atomo e applicate la regola del suo connettivo principale e del suo segno, aggiungendo ciò che quella regola produce in fondo a ogni ramo che vi passa.
4. Chiudete un ramo appena porta insieme T A e F A per la stessa formula A. Fermatevi quando ogni ramo è chiuso, o quando non resta più alcuna riga da scomporre.

Nulla in questo ciclo richiede acume o una scelta di strategia. Ogni riga ha esattamente una regola, e applicarle in qualsiasi ordine dà lo stesso verdetto: per questo una macchina può farlo, e per questo potete fidarvi del risultato quando lo fa.

4. Le regole

C'è una regola per ciascun connettivo sotto ciascun segno: dieci in tutto. Si dividono in due specie, e la differenza fra le specie è l'intera ragione per cui un tableau è un albero e non un elenco. Una regola α dice che più cose devono valere insieme, e impila i suoi risultati lungo il ramo. Una regola β dice che deve valere una di due cose, e quindi divide il ramo in due lasciando che ogni caso vada per la sua strada.

Ogni regola non è che la condizione di verità del suo connettivo, letta a rovescio. Una congiunzione è vera solo quando lo sono entrambi i lati, quindi T (A ∧ B) impila T A e T B. Una congiunzione è falsa quando almeno un lato lo è, ma la formula non dice quale, quindi F (A ∧ B) deve provarli entrambi: dirama. La stessa asimmetria corre al contrario per la disgiunzione, e un condizionale falso significa che l'antecedente valeva e il conseguente è venuto meno, l'unico caso in cui un'implicazione si rompe.

Notate ciò che le regole non fanno mai: non inventano mai una formula. Tutto ciò che una regola produce è un pezzo della riga da cui è venuta. Quella proprietà - la proprietà della sottoformula - è ciò che rende finito il metodo, e ci torniamo più sotto.

5. Chiudere un ramo

Un ramo è un unico filo di ragionamento: leggete dalla radice a una foglia e avete un insieme completo di assunzioni. Un ramo si chiude quando quelle assunzioni si contraddicono apertamente, cioè quando porta insieme T A e F A per una stessa formula. Non importa quanto A sia complicata né quanto le due righe siano distanti: se un ramo pretende che una formula sia insieme vera e falsa, nulla lo soddisfa.

Segnate un ramo chiuso con ×, indicando le due righe che l'hanno chiuso, e smettete di lavorarci. Da un'assunzione già impossibile non si impara altro.

Quando ogni ramo si chiude, il tableau è chiuso, e quella è la dimostrazione. Mostra che la supposizione di partenza - tutte le premesse vere, la conclusione falsa - porta a contraddizione su ogni strada che poteva prendere. Poiché non è rimasta alcuna strada, non esiste un'assegnazione simile, e l'argomento è valido. È una dimostrazione per assurdo, disposta in modo che nessun caso possa sfuggire.

6. Una dimostrazione, riga per riga

Prendiamo il modus tollens: p → q, ¬q ⊨ ¬p. Le righe 1 e 2 sono le premesse, supposte vere. La riga 3 è la conclusione, supposta falsa; e poiché la conclusione è ¬p, supporla falsa significa supporre p vera, come registra la riga 5. La riga 4 viene dalla regola di negazione applicata alla riga 2: se ¬q è vera, q è falsa. Il condizionale della riga 1 è l'unica riga rimasta con un connettivo, ed è una regola β: l'albero quindi si biforca.

Il ramo di sinistra suppone che il condizionale valesse perché il suo antecedente è venuto meno, ma la riga 5 ha già p vera, quindi il ramo si contraddice e si chiude. Il ramo di destra suppone che valesse perché il suo conseguente era vero, ma la riga 4 ha già q falsa, quindi si chiude anch'esso.

Entrambi i rami si sono chiusi, dunque non c'è modo di avere p → q e ¬q vere con ¬p falsa. L'argomento è valido, e l'albero ne è la ragione. Notate che la dimostrazione non nomina né pioggia né terreno né che cosa stiano per p e q. Non ne aveva bisogno.

7. Quando un ramo resta aperto

Non ogni argomento è valido, ed è qui che il metodo si guadagna il posto. Se lavorate un ramo finché nulla su di esso può essere scomposto oltre - restano solo atomi e atomi negati - e non si è ancora chiuso, quel ramo è saturo e aperto. Non si è chiuso, e non perché vi siate fermati troppo presto: non c'è più nulla da provare.

Un ramo aperto è più di un verdetto di «non valido». Leggete i segni dei suoi atomi e avete un'assegnazione: ogni atomo segnato T è vero, ogni atomo segnato F è falso. Quell'assegnazione rende vere tutte le premesse e falsa la conclusione, che è esattamente ciò che è un controesempio. I logici lo chiamano contromodello, ed è una risposta concreta a «perché no?» invece di un rifiuto.

L'affermazione del conseguente, p → q, q ⊨ p, è il caso da manuale. Il suo tableau lascia un ramo aperto con p falsa e q vera: una situazione in cui il condizionale vale e il suo conseguente vale, eppure l'antecedente no. Quella sola assegnazione confuta l'argomento da sé.

8. Perché finisce sempre

Ogni regola sostituisce una formula con le sue stesse sottoformule, e ogni sottoformula è strettamente più corta della formula da cui viene. Nessun ramo può quindi crescere all'infinito: ogni passo scende una scala finita di pezzi dell'argomento iniziale, e la scala ha un fondo. Prima o poi ogni riga di un ramo è un atomo o la negazione di uno, e non resta altro da fare.

È una garanzia vera, non una speranza. Significa che il metodo è una procedura di decisione per la logica proposizionale: applicatelo a un argomento qualsiasi e si fermerà, con un albero chiuso o con un ramo aperto, e mai con un'alzata di spalle. Il dimostratore di questo sito impone in più un budget di nodi, ma solo come difesa contro una formula patologica che esaurisca una scheda del browser: la matematica non ha bisogno di alcun limite simile.

9. Altri sistemi di dimostrazione

I tableaux sono uno fra vari sistemi di dimostrazione, e sono quello a forma di confutazione: lavorano escludendo il fallimento. La deduzione naturale fa il contrario e costruisce la conclusione in avanti a partire dalle premesse, con regole come il modus ponens e la prova condizionale, e somiglia molto di più al modo in cui un matematico argomenta in prosa. Una dimostrazione in deduzione naturale è di solito più corta; trovarla richiede di solito più inventiva.

Il calcolo dei sequenti formalizza il segno di conseguenza stesso e tratta le affermazioni di conseguenza come oggetti, il che ne fa lo strumento d'elezione per dimostrare cose sulle dimostrazioni. La risoluzione riduce tutto a clausole e a una sola regola, cosa poco vistosa da leggere ed estremamente rapida da eseguire: su di essa sono costruiti la maggior parte dei dimostratori automatici e dei risolutori SAT.

Tutti concordano su quali argomenti proposizionali siano validi; differiscono per l'aspetto di una dimostrazione e per ciò che è facile trovare. I tableaux sono i più accoglienti per imparare, perché una dimostrazione fallita non è un vicolo cieco: vi consegna il controesempio.

10. Esercitarsi

Il modo più rapido di imparare il metodo è eseguirlo. Scrivete un argomento nel calcolatore con ⊨, ⊢ o |= e il tableau viene disegnato accanto alla tavola di verità, così potete confrontare l'albero con le righe. Poi svolgete qualche dimostrazione su carta prima di guardare.