Leggi di De Morgan e leggi distributive

Le lezioni precedenti di questa unità hanno costruito, l’una sull’altra, gli strumenti della deduzione: il sistema di assiomi e il modus ponens, le quattro tecniche di base e la sostituzione della doppia negazione, le simmetrie dei connettivi e le tecniche della logica classica. Questa lezione non aggiunge alcuna regola nuova; le mette a lavorare insieme. Se è così, il suo interesse non sta tanto negli enunciati, che forse si conoscono già da altri corsi, quanto nel modo di ottenerli: ogni riga deve essere giustificata da un assioma, una premessa, una definizione, una delle due regole primitive o un risultato già dimostrato, e nessuna può appoggiarsi su ciò che «sembra evidente».

Che cosa si usa e come si concatena

Dalla lezione sui sistemi deduttivi formali si prendono gli assiomi A1, A2 e A3 di Łukasiewicz, il modus ponens (MP), anche con premesse, 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 l’equivalenza dimostrabile ($\varphi \dashv\vdash \psi$ se $\{\varphi\} \vdash \psi$ e $\{\psi\} \vdash \varphi$), con le sue proprietà: è riflessiva, simmetrica e transitiva, e, se $\varphi \dashv\vdash \psi$, allora $\Gamma \vdash \varphi$ se e solo se $\Gamma \vdash \psi$. Dalla lezione sulle quattro tecniche di deduzione, la doppia negazione (DN: $\varphi \dashv\vdash \neg\neg\varphi$), la contrapposizione (CP), in particolare $(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi)$, e la seconda regola primitiva del sistema del corso, la sostituzione della doppia negazione (SDN), con la quale il teorema di deduzione continua a valere: se $\chi'$ risulta da $\chi$ sostituendo un’occorrenza di una sottoformula $\theta$ con $\neg\neg\theta$, o una di $\neg\neg\theta$ con $\theta$, da $\chi$ si inferisce $\chi'$; la riga così ottenuta dalla riga $i$ si giustifica SDN$(i)$. Tra le sue conseguenze immediate vi sono $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$, $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ e, in generale, $\chi \dashv\vdash \chi'$ quando $\chi'$ risulta da $\chi$ per SDN; ne segue che SDN$(i)$ si applica anche a una riga della forma $\chi \dashv\vdash \varphi$, per cambiare una doppia negazione in $\varphi$. Dalla lezione sulle simmetrie dei connettivi, la sostituzione di equivalenti (Sost) e le simmetrie (Sim), tra cui $(\varphi \vee \psi) \dashv\vdash (\psi \vee \varphi)$ e $(\varphi \wedge \psi) \dashv\vdash (\psi \wedge \varphi)$.

Dalla lezione sulle tecniche della logica classica si prendono, tutte con un insieme $\Gamma$ di premesse, le regole seguenti. L’introduzione della disgiunzione ($\vee$I): se $\Gamma \vdash \varphi$, allora $\Gamma \vdash (\varphi \vee \psi)$ e $\Gamma \vdash (\psi \vee \varphi)$. L’eliminazione della disgiunzione ($\vee$E, sillogismo disgiuntivo): se $\Gamma \vdash (\varphi \vee \psi)$ e $\Gamma \vdash \neg\varphi$, allora $\Gamma \vdash \psi$. L’introduzione della congiunzione ($\wedge$I): se $\Gamma \vdash \varphi$ e $\Gamma \vdash \psi$, allora $\Gamma \vdash (\varphi \wedge \psi)$. L’eliminazione della congiunzione ($\wedge$E): se $\Gamma \vdash (\varphi \wedge \psi)$, allora $\Gamma \vdash \varphi$ e $\Gamma \vdash \psi$. Il terzo escluso (TE): $\vdash (\varphi \vee \neg\varphi)$. E la dimostrazione per casi (Casi) nelle sue due forme: se $\Gamma \cup \{\varphi\} \vdash \chi$ e $\Gamma \cup \{\neg\varphi\} \vdash \chi$, allora $\Gamma \vdash \chi$; e se $\Gamma \cup \{\varphi\} \vdash \chi$, $\Gamma \cup \{\psi\} \vdash \chi$ e $\Gamma \vdash (\varphi \vee \psi)$, allora $\Gamma \vdash \chi$. Nelle deduzioni, la prima forma si cita con due righe, Casi$(i, j)$, e la seconda, con tre, Casi$(i, j, k)$, nell’ordine dell’enunciato: i due casi e, alla fine, la disgiunzione. Quella lezione ricorda inoltre che ogni regola già dimostrata vale dentro un contesto $\Gamma$, ed è così che qui si usano la doppia negazione e la contrapposizione.

Nomi di una stringa e formule equivalenti

Si ricordi, dalla lezione sul linguaggio della logica proposizionale, che i connettivi diversi da $\downarrow$ sono abbreviazioni con una definizione ufficiale e unica: $\neg\varphi := (\varphi \downarrow \varphi)$, $(\varphi \vee \psi) := \neg(\varphi \downarrow \psi)$, $(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)$, $(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi)$, $(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))$ e $(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)$. Una definizione non afferma nulla sulle formule: dà un secondo nome a una stringa che esisteva già. Ne segue che, se due espressioni designano la stessa stringa, l’una può essere messa al posto dell’altra in qualunque punto, anche dentro una formula più grande, perché ciò che si scrive è la stessa successione di cerchi e dischi. Così, $\neg(\varphi \wedge \psi)$ e $\neg\neg(\neg\varphi \vee \neg\psi)$ sono la stessa stringa: la seconda risulta dallo scrivere, dentro la prima, lo sviluppo della congiunzione. Nelle deduzioni, questo cambio di nome si giustifica con «Def», seguito dal connettivo che si sviluppa o si contrae.

Ora, un’equivalenza dimostrabile non è un’identità. Che valga $\varphi \dashv\vdash \neg\neg\varphi$ significa che da ciascuna si deduce l’altra, non che siano la stessa stringa: $\neg\neg\varphi$ è molto più lunga di $\varphi$. Pertanto, sapere che $\varphi \dashv\vdash \varphi'$ non autorizza di per sé a scrivere $\varphi'$ al posto di $\varphi$ dentro una formula più grande. Né autorizza a «negare entrambi i lati»: che da $\varphi \dashv\vdash \varphi'$ segua $\neg\varphi \dashv\vdash \neg\varphi'$ è un teorema, la sostituzione di equivalenti, la cui dimostrazione usa la contrapposizione, e non un’operazione evidente. C’è un solo caso in cui il sistema autorizza direttamente la sostituzione, in qualunque punto di una formula: quello di $\theta$ con $\neg\neg\theta$, o viceversa, che è la regola SDN; e la lezione sui sistemi deduttivi ha mostrato, con la marcatura, che neppure questo caso si deduce dagli assiomi e dal modus ponens, sicché è stato necessario postularlo. Questa cura non è pedanteria; è ciò che distingue una dimostrazione da una manipolazione di simboli che potrebbe, applicata ad altri connettivi o in altri sistemi, condurre a falsità.

Due risultati fissano con precisione ciò che è permesso. Il primo è la proposizione sulle proprietà dell’equivalenza dimostrabile della lezione sui sistemi deduttivi formali: se $\Gamma \vdash \varphi$ e $\varphi \dashv\vdash \varphi'$, allora $\Gamma \vdash \varphi'$, sicché un’equivalenza dimostrabile può applicarsi alla formula intera di una riga; e l’equivalenza dimostrabile è riflessiva, simmetrica e transitiva, sicché le equivalenze si concatenano (se $\chi \dashv\vdash \varphi$ e $\varphi \dashv\vdash \varphi'$, allora $\chi \dashv\vdash \varphi'$) e due espressioni che designano la stessa stringa sono, per riflessività, dimostrabilmente equivalenti. Il secondo, il lemma seguente, raccoglie, per poterla citare comodamente, l’estensione della sostituzione di equivalenti alla disgiunzione e alla congiunzione, che la lezione sulle simmetrie dimostra per la negazione, l’implicazione e la negazione congiunta ed estende a questi due connettivi in uno dei suoi problemi risolti.

D’ora in poi, «Sost» designa la sostituzione di equivalenti in una qualsiasi delle sue forme, anche quelle di questo lemma, e può applicarsi più volte di seguito, strato per strato, per raggiungere una sottoformula situata a qualunque profondità. Quando una riga si ottiene dalla riga $i$ applicando un’equivalenza già dimostrata, sia alla formula intera sia, con Sost, a una delle sue parti, si giustifica con il nome di quell’equivalenza e il numero della riga: DN$(i)$, «Sost, DM$(i)$». Un cambio di nome, che non applica alcuna equivalenza ma riscrive la stessa stringa, si giustifica allo stesso modo, con Def seguito dal connettivo che si sviluppa o si contrae: Def $\wedge$ $(i)$. La proposizione della lezione sui sistemi deduttivi formali garantisce che quelle righe sono giustificate, tanto se la riga $i$ afferma $\Gamma \vdash \varphi$ quanto se afferma un’equivalenza $\chi \dashv\vdash \varphi$ che si va prolungando.