Quattro tecniche di deduzione

Gli strumenti di partenza

Nella lezione sui sistemi deduttivi formali si è fissato il sistema di Łukasiewicz. Il suo linguaggio è la lingua dei cerchi e dei dischi, scritta con le abbreviazioni ufficiali della lezione sul linguaggio della logica proposizionale; i suoi assiomi sono tutte le istanze dei tre schemi seguenti, dove $\varphi$, $\psi$ e $\chi$ sono formule qualsiasi, e la sua unica regola è il modus ponens.

• A1: $(\varphi \rightarrow (\psi \rightarrow \varphi))$.
• A2: $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$.
• A3: $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$.
• MP: da $\varphi$ e $(\varphi \rightarrow \psi)$ si deduce $\psi$.

Una deduzione di $\varphi$ da un insieme $\Gamma$ di formule è una successione finita di formule che termina in $\varphi$ e in cui ogni formula è un assioma, un elemento di $\Gamma$ o il risultato dell’applicazione del modus ponens a due formule precedenti; se esiste, si scrive $\Gamma \vdash \varphi$, e se $\Gamma$ è vuoto, $\vdash \varphi$, e si dice che $\varphi$ è un teorema. In quella stessa lezione si sono dimostrati i metateoremi che useremo qui: la riflessività (Rifl: se $\varphi \in \Gamma$, allora $\Gamma \vdash \varphi$), la monotonia (Mon: se $\Gamma \subseteq \Delta$ e $\Gamma \vdash \varphi$, allora $\Delta \vdash \varphi$), il modus ponens tra deduzioni (se $\Gamma \vdash \varphi$ e $\Gamma \vdash (\varphi \rightarrow \psi)$, allora $\Gamma \vdash \psi$), il taglio (Taglio: se $\Gamma \vdash \varphi_{i}$ per ogni $i$ da $1$ a $n$ e $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, allora $\Gamma \vdash \psi$), la finitezza (se $\Gamma \vdash \varphi$, basta un sottoinsieme finito di $\Gamma$), il teorema di deduzione (TD: se $\Gamma \cup \{\varphi\} \vdash \psi$, allora $\Gamma \vdash (\varphi \rightarrow \psi)$) e il suo inverso (RTD), e il teorema $\vdash (\varphi \rightarrow \varphi)$, che nelle giustificazioni abbrevieremo Id. Infine, $\varphi \dashv\vdash \psi$ (equivalenza dimostrabile) significa che $\{\varphi\} \vdash \psi$ e $\{\psi\} \vdash \varphi$.

Conviene ricordare che $\neg$ e $\rightarrow$ non sono simboli della lingua di base, ma abbreviazioni: $\neg\varphi$ è la stringa $(\varphi \downarrow \varphi)$, e $(\varphi \rightarrow \psi)$ è $(\neg\varphi \vee \psi)$, cioè $\neg(\neg\varphi \downarrow \psi)$. I tre assiomi parlano solo di negazioni e di implicazioni, e la stessa lezione ha mostrato, con una marcatura a valori $0$ e $1$ che essi e il modus ponens conservano, il limite che ne segue: nel sistema di Łukasiewicz, da $(v_{1} \downarrow v_{2})$ non si deduce $(\neg\neg v_{1} \downarrow v_{2})$, e la negazione congiunta resta in parte fuori della sua portata. Questa lezione procede, pertanto, in due tempi. Fino alla doppia negazione inclusa, $\vdash$ si riferisce al sistema di Łukasiewicz, e nulla di ciò che si dimostra dipende dallo sviluppo delle abbreviazioni. Dimostrata la doppia negazione, si aggiunge al sistema una seconda regola primitiva, la sostituzione della doppia negazione, che agisce sulla stringa sviluppata; da quel punto, $\vdash$ si riferisce al sistema del corso, quello di Łukasiewicz più questa regola. Poiché ogni deduzione del primo è anche deduzione del secondo, nulla di ciò che si è dimostrato prima va perduto.

Due stili di deduzione

Ci sono due modi di scrivere una deduzione, ed entrambi saranno usati. Il primo è la deduzione propriamente detta, una successione di formule in cui ogni riga è un assioma, una premessa o il risultato del modus ponens; ogni riga si giustifica con A1, A2, A3, Premessa o MP$(i, j)$, dove la riga $i$ è l’antecedente e la riga $j$ è l’implicazione il cui antecedente è esattamente la riga $i$ (e, da quando sarà introdotta la regola nuova, SDN$(i)$). Il secondo è la deduzione sulle deduzioni, le cui righe non sono formule, ma affermazioni della forma $\Gamma \vdash \varphi$; ciascuna si giustifica con un metateorema già dimostrato, e l’intera successione è un ragionamento del metalinguaggio che garantisce che esiste una deduzione del primo stile, anche se non la scrive. Le giustificazioni di questo secondo stile si leggono come segue.

• Rifl: la formula di destra appartiene all’insieme di sinistra.
• A1, A2, A3: la formula di destra è un’istanza dello schema; un’istanza di un assioma si deduce da qualunque $\Gamma$ con una deduzione di una sola riga.
• MP$(i, j)$: il modus ponens tra deduzioni, applicato alla riga $i$, $\Gamma \vdash \varphi$, e alla riga $j$, $\Gamma \vdash (\varphi \rightarrow \psi)$, con lo stesso $\Gamma$.
• TD$(i)$ e RTD$(i)$: il teorema di deduzione o il suo inverso, applicato alla riga $i$.
• Il nome di un teorema già dimostrato, come Id o DN: la formula di destra è un’istanza di quel teorema, e si deduce da qualunque $\Gamma$ per monotonia, perché l’insieme vuoto è contenuto in $\Gamma$.
• Premessa, in una deduzione sulle deduzioni: la riga è una delle ipotesi della regola che si sta dimostrando.

Ogni risultato di questa lezione si enuncia con metavariabili e vale, pertanto, per formule qualsiasi: la sua dimostrazione è uno schema, e cambiando in essa ogni metavariabile con una formula si ottiene un’altra dimostrazione, perché le istanze di uno schema di assioma restano tali e ogni modus ponens resta tale (lo stesso varrà per ogni applicazione della regola nuova). Così, da $\vdash (\varphi \rightarrow \varphi)$ segue $\vdash (\neg\psi \rightarrow \neg\psi)$, con $\neg\psi$ al posto di $\varphi$. Questo espediente, applicare un risultato a una formula più complessa di quella dell’enunciato, è quello che rende di più in ciò che segue.

Dal risultato alla regola

Le tecniche di questa lezione si dimostrano da premesse fisse, come $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$; ma si usano nel mezzo di deduzioni con altre premesse, dove $(\varphi \rightarrow \psi)$ e $(\psi \rightarrow \chi)$ non sono premesse, ma formule già dedotte. Il lemma seguente, conseguenza diretta della monotonia e del taglio, autorizza questo uso una volta per tutte.

Ne segue che ogni tecnica dimostrata da premesse ha tre presentazioni: il risultato stesso, il teorema che si ottiene scaricandone le premesse e la regola che si applica sotto qualunque $\Gamma$. In una deduzione sulle deduzioni, la regola si invoca con il nome della tecnica e i numeri delle righe a cui si applica, come SI$(3, 4)$, e il lemma garantisce che il passo è legittimo.