Le simmetrie dei connettivi

Ciò che si usa e ciò che bisogna dimostrare

La lezione sui sistemi deduttivi formali ha fissato il sistema di Łukasiewicz: gli assiomi A1, A2 e A3 e il modus ponens. Ha stabilito inoltre la riflessività (Rifl: se $\varphi \in \Gamma$, allora $\Gamma \vdash \varphi$), la monotonia (Mon), il taglio (Taglio: se $\Gamma \vdash \varphi_{i}$ per ogni $i$ e $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, allora $\Gamma \vdash \psi$), il teorema di deduzione (TD) e il suo inverso (RTD) e l’equivalenza dimostrabile, $\varphi \dashv\vdash \psi$, che significa che $\{\varphi\} \vdash \psi$ e $\{\psi\} \vdash \varphi$; e ha mostrato, con una marcatura che gli assiomi e il modus ponens conservano, che quel sistema non deduce certe formule sulla negazione congiunta. La lezione sulle quattro tecniche di deduzione ha aggiunto il sillogismo ipotetico (SI: $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$), lo scambio delle premesse (SP), la doppia negazione (DN: $\varphi \dashv\vdash \neg\neg\varphi$, con i suoi due teoremi $\vdash (\neg\neg\varphi \rightarrow \varphi)$ e $\vdash (\varphi \rightarrow \neg\neg\varphi)$) e la contrapposizione (CP) nelle sue tre forme:

Dimostrata la doppia negazione, quella stessa lezione ha completato il sistema del corso con una seconda regola primitiva, la sostituzione della doppia negazione (SDN): se $\chi'$ risulta da $\chi$ sostituendo un’occorrenza di una sottoformula $\theta$ con $\neg\neg\theta$, o un’occorrenza di una sottoformula $\neg\neg\theta$ con $\theta$, allora da $\chi$ si inferisce $\chi'$. La riga ottenuta così dalla riga $i$ si giustifica con SDN$(i)$. Da quel punto in poi, $\vdash$ si riferisce al sistema del corso (da A1 ad A3, il modus ponens e SDN), nel quale continuano a valere Rifl, Mon, Taglio, TD e RTD. La regola agisce sulla stringa della lingua di base, in modo che raggiunge anche le occorrenze che un’abbreviazione nasconde, e in ciascuno dei due argomenti di una negazione congiunta; tra le sue conseguenze immediate ci sono

e, in generale, $\chi \dashv\vdash \chi'$ ogni volta che $\chi'$ risulta da $\chi$ per SDN. Una riga di equivalenza di questa forma si giustifica con «SDN», senza numero di riga, allo stesso modo in cui una riga «DN» o «CP» cita un’equivalenza già dimostrata. Come lì, un teorema già dimostrato può essere scritto come riga di una deduzione, perché la sua stessa deduzione può essere inserita in quel punto; e, per il lemma «dal risultato alla regola» di quella lezione, ogni tecnica si applica anche come regola sotto qualunque insieme $\Gamma$ di premesse, citata con i numeri delle righe a cui si applica, come CP$(i)$ o SI$(i, j)$. Nelle deduzioni sulle deduzioni, «Premessa» designa un’ipotesi della regola che si dimostra.

Le abbreviazioni ufficiali, fissate nella lezione sul linguaggio della logica proposizionale, sono le uniche definizioni dei connettivi:

Una riga giustificata con «Def» non deduce nulla: scrive la stessa formula con un altro nome, e l’annotazione dice quale abbreviazione si sviluppa o si contrae («Def $\rightarrow$», «Def $\vee$»). Conviene ricordare il fenomeno osservato nella lezione sulla formalizzazione del linguaggio naturale: una stessa formula ammette vari nomi, in modo che una congiunzione è anche, come stringa, una disgiunzione. Per esempio, sviluppando l’implicazione con $\neg\varphi$ al posto di $\varphi$, si ottiene

e la doppia negazione che compare davanti a $\varphi$, nascosta dall’abbreviazione, è la ragione per cui la regola SDN interverrà in tutto ciò che segue.

L’equivalenza dimostrabile come uguaglianza

Le dimostrazioni di questa lezione sono, quasi tutte, catene di equivalenze: $\varphi_{1} \dashv\vdash \varphi_{2}$, $\varphi_{2} \dashv\vdash \varphi_{3}$, e così via. Perché da una catena si concluda $\varphi_{1} \dashv\vdash \varphi_{n}$, l’equivalenza dimostrabile deve comportarsi come un’uguaglianza, ed è ciò che ha stabilito la proposizione sulle proprietà dell’equivalenza dimostrabile della lezione sui sistemi deduttivi formali: la relazione è riflessiva ($\varphi \dashv\vdash \varphi$), simmetrica (se $\varphi \dashv\vdash \psi$, allora $\psi \dashv\vdash \varphi$) e transitiva (se $\varphi \dashv\vdash \psi$ e $\psi \dashv\vdash \chi$, allora $\varphi \dashv\vdash \chi$), e due formule dimostrabilmente equivalenti sono intercambiabili come conclusioni (se $\Gamma \vdash \varphi$ e $\varphi \dashv\vdash \varphi'$, allora $\Gamma \vdash \varphi'$, per ogni insieme $\Gamma$ di formule). Conviene ricordare come si sono dimostrate le ultime due, perché tutta la lezione poggia su di esse: da $\{\varphi\} \vdash \varphi'$ si passa, per monotonia, a $\Gamma \cup \{\varphi\} \vdash \varphi'$, e da questa e da $\Gamma \vdash \varphi$, per taglio, a $\Gamma \vdash \varphi'$; la transitività risulta dall’applicare ciò con $\Gamma = \{\varphi\}$ in un senso e con $\Gamma = \{\chi\}$ nell’altro.

D’ora in poi, il passo che riunisce una catena di equivalenze in una sola si giustifica con «Taglio», che è lo strumento di quella proposizione. Ora, ogni anello $\varphi_{i} \dashv\vdash \varphi_{i+1}$ contiene le due deduzioni, quella di andata e quella di ritorno; donde una catena di equivalenze dimostra allo stesso tempo i due sensi della sua conclusione, e nulla resta «come esercizio».