Le tecniche della logica classica

Le regole all’interno di un contesto

Nella lezione sui sistemi deduttivi formali si è fissato il sistema di Łukasiewicz: gli schemi di assiomi A1, A2 e A3, la regola del modus ponens (MP) e la nozione di deduzione da un insieme $\Gamma$ di premesse, con le sue prime proprietà: 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 taglio (Taglio), il modus ponens tra deduzioni (se $\Gamma \vdash \varphi$ e $\Gamma \vdash (\varphi \rightarrow \psi)$, allora $\Gamma \vdash \psi$, che si cita anche come MP), il teorema di deduzione (TD: se $\Gamma \cup \{\varphi\} \vdash \psi$, allora $\Gamma \vdash (\varphi \rightarrow \psi)$) e il suo inverso (RTD). Le lezioni sulle quattro tecniche di deduzione e sulle simmetrie dei connettivi hanno aggiunto il sillogismo ipotetico (SI), lo scambio delle premesse (SP), la doppia negazione (DN), la contrapposizione (CP) nelle sue tre forme, la sostituzione di equivalenti (Sost), le simmetrie (Sim) e le forme equivalenti della disgiunzione e della congiunzione. La prima di queste lezioni, dopo aver dimostrato la doppia negazione, ha inoltre 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 $\neg\neg\theta$ con $\theta$, da $\chi$ si inferisce $\chi'$. D’ora in poi, $\vdash$ si riferisce a quel sistema (gli schemi da A1 ad A3, MP e SDN), nel quale continuano a valere la riflessività, la monotonia, il taglio, il teorema di deduzione e il suo inverso; le tecniche di questa lezione ne sono regole derivate, benché nessuna delle loro dimostrazioni invochi SDN direttamente: la regola agisce attraverso le forme equivalenti e la sostituzione di equivalenti, che la lezione sulle simmetrie ha dimostrato con essa.

Ora, in matematica nessuno ragiona senza premesse: si ragiona a partire da certi assiomi, dalle ipotesi di un teorema e da ciò che si è supposto per discutere un caso. Se è così, una tecnica di ragionamento è utile solo se è enunciata con un insieme $\Gamma$ di premesse che ci si porta dietro di riga in riga. Ne segue che ogni regola di questa lezione si enuncia e si dimostra per un $\Gamma$ qualsiasi; il caso senza premesse è il caso particolare $\Gamma = \emptyset$, e non il contrario.

Le dimostrazioni sono deduzioni sulle deduzioni: ogni riga afferma che qualcosa è deducibile da un insieme, $\Gamma \vdash \varphi$, e la sua giustificazione rimanda a righe precedenti. In esse, «Premessa» indica le righe che l’enunciato della regola dà per presupposte, e il nome di un assioma (A1, A3) o di un teorema già dimostrato (come Id, il teorema $\vdash (\varphi \rightarrow \varphi)$) indica una riga $\Gamma \vdash \varphi$ in cui $\varphi$ è un’istanza di quello schema o di quel teorema, deducibile da qualunque insieme.

La lezione sulle quattro tecniche di deduzione ha dimostrato, con la monotonia e il taglio, il lemma «dal risultato alla regola», che rende possibile questo modo di lavorare: se $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ e $\Gamma \vdash \alpha_{i}$ per ogni $i$, allora $\Gamma \vdash \beta$. Con $n = 1$, applicato in ciascun verso di un’equivalenza $\alpha \dashv\vdash \alpha'$, dice che $\Gamma \vdash \alpha$ se e solo se $\Gamma \vdash \alpha'$. Pertanto, ogni regola già dimostrata e ogni equivalenza già dimostrata si applicano alle righe di una deduzione con premesse: se una riga dice $\Gamma \vdash (\varphi \rightarrow \psi)$, la contrapposizione permette di scrivere sotto $\Gamma \vdash (\neg\psi \rightarrow \neg\varphi)$ e di giustificarla con «CP» e il numero della riga. Per le due forme equivalenti della lezione sulle simmetrie, che si useranno di continuo, si scrive «Eq»:

Conviene insistere sul fatto che la prima di queste equivalenze non è una definizione; la seconda, come ha mostrato la lezione sulle simmetrie, è un’identità di stringhe, ma si cita come Eq insieme alla prima. Per definizione, $(\varphi \vee \psi)$ è $\neg(\varphi \downarrow \psi)$ e $(\neg\varphi \rightarrow \psi)$ è $(\neg\neg\varphi \vee \psi)$, che sono stringhe distinte; leggere l’una come l’altra «per definizione dell’implicazione» è l’errore che questa lezione evita. «Def», invece, è riservato a scrivere la stessa stringa con un altro nome, come quando si legge $(\varphi \rightarrow \psi)$ come $(\neg\varphi \vee \psi)$.