LOGICA FORMALE 20: DEDUZIONE NATURALE
LOGICA FORMALE 20: DEDUZIONE NATURALE
Apr 18[ad#Ret Big]
È ascoltando finissimo metal norvegese che scrivo questo post invece che essere al mare, ed ho le farfalle nello stomaco perché da oggi parte il nuovo argomento del nostro bel corso di logica, che sono sicuro che vi piacerà abbastanza. (Mangiare farfalle è una cosa snervante: ne servono moltissime per saziarsi)
Perciò mentre finisco di cacciar farfalle copierò Berto per introdurre il tema, il quale scrive:
Allorchè si supera il livello del linguaggio enunciativo, le tavole di verità non sono più uno strumento adeguato per stabilire la correttezza dei ragionamenti. Occorrerà un approccio diverso, e questo consisterà nello sviluppo di un sistema formale. In generale, un sistema formale è un apparato di regole e di principi che consente di costruire dimostrazioni formali. Questo apparato è sempre impiantato su un certo linguaggio formale: nel nostro caso, i linguaggi di riferimento saranno quello predicativo e quello enunciativo […].
[…] presenteremo un sistema formale che consente di dimostrare formalmente la validità di schemi d’argomento, deducendo (o, come anche si dice, derivando) la loro conclusione dalle premesse attraverso una sequenza di deduzioni elementari; ovvero, consente di esibire la bontà di una inferenza attraverso una concatenazione di inferenze più basilari.
Il sistema formale che illustrerò sarà il calcolo della deduzione naturale, sistema inventato dal matematico Gerhard Gentzen. Mentre il primo e più classico sistema formale è dovuto invece a Gottlob Frege e David Hillbert che svilupparono l’assiomatica.
La deduzione naturale è un sistema molto complesso che nasconde molte finezze e grandi possibilità per gli addetti ai lavori, mentre noi cercheremo insieme di studiarne almeno le basi, non crediate però che sia tutto qui!
La formula generale di un argomento, espressa con metavariabili, sarà la seguente:
α1, …, αn ᅡβ
A sinistra abbiamo le premesse scritte con metavariabili da “α1” a “αn” e separate da virgole. Le premesse sono separate dalla conclusione dal simbolo “ᅡ” che a volte è detto segno di asserzione e risale a Frege: esso indica l’inferibilità o derivabilità della conclusione dalle premesse.
In deduzione naturale non esistono normalmente assiomi ma regole di inferenza e per essere precisi vi è una regola detta di “introduzione” e una detta di “eliminazione” per ogni operatore logico e per ogni quantificatore, a parte che per la negazione.
Oggi per iniziare tratteremo la regola di “assunzione”, abbreviata con “Ass” che è culo in inglese. Questa regola non riguarda propriamente i simboli logici tanto per cominciare, ma è la regola che permette di introdurre premesse nel ragionamento.
Seguimo Berto e facciamo un primo esempio, immaginiamo che una dimostrazione formale cominci con la seguente riga:
(1) 1 P→Q Ass
Il primo “1” fra parentesi indica il numero della riga, in questo caso prima riga. Il secondo “1” a destra del primo indica da quale riga dipende la formula della riga in questione. “Ass”, culo vuol dire che è una assunzione. Essendo la prima riga del ragionamento, ed essendo per l’appunto una assunzione, questa formula dipenderà solo da se stessa quindi nella seconda colonna che chiameremo colonna delle assunzioni troviamo scritto sempre “1”. Se invece la medesima formula, non derivata ma assunta, fosse introdotta nell’ottava riga del nostro ragionamento allora troveremo scritto:
(8) 8 P→Q Ass
Nella prima colonna c’è un “8” fra parentesi che sta ad indicare il numero progressivo di riga del ragionamento, mentre nella seconda colonna c’è un “8” senza parentesi perché questa assunzione non è derivata dalle formule delle sette righe precedenti ma introdotta ora e quindi dipende solo da se stessa.
Le assunzioni sono formule introdotte che non derivano da precedenti formule utilizzate nel ragionamento. Le premesse sono formule grazie alle quali si ottengono, attraverso regole di inferenza, altre formule per la prosecuzione dell’inferenza. Questa è una precisazione del tutto terminologica, nei fatti le premesse che vengono introdotte nel ragionamento, lo sono allo scopo di divenire premesse per permettere la deduzione di altre formule.
Sembra che sia un metodo del tutto aleatorio introdurre una assunzione, ma è quello che facciamo sempre ogni giorno attraverso il ragionamento ipotetico. Faccio un esempio: “a Pasqua voglio andare al mare” ma poniamo il caso ipotetico “a Pasqua piove” e “se piove non vado al mare”, come la mettiamo? È per questo motivo che è così facile assumere formule nel ragionamento, perché se non sono pertinenti non inficeranno il ragionamento, se sono formule che lo mettono in qualche modo alla prova allora concorreranno al procedimento di prova di validità del ragionamento stesso.
Cosa fate a pasquetta?
[Errata corrige: nell’appuntamento numero 9 del corso di logica in luogo di un argomento scorretto era stata pubblicata l’immagine di una tavola di verità che riportava lo svolgimento del modus ponens. Perdono! Ora è tutto a posto.]