Vai al contenuto
Topos Uranos
Italiano

Sistemi deduttivi formali

Riepilogo

Questa lezione trasforma il linguaggio dell’unità precedente in uno strumento per dimostrare. Definisce che cos’è un sistema deduttivo formale (un linguaggio, alcuni schemi di assiomi e alcune regole d’inferenza) e presenta il primo dei due con cui lavora il corso, il sistema di Łukasiewicz: tre schemi di assiomi e il modus ponens come unica regola. Definisce con precisione la deduzione da un insieme di premesse, il teorema e la relazione Γ⊢φ\Gamma \vdash \varphi, deduce ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) in cinque righe e dimostra le proprietà strutturali della deduzione: riflessività, monotonia, modus ponens tra deduzioni, taglio e finitezza. Dimostra poi, per induzione forte sul numero di righe, il teorema di deduzione e il suo inverso, che permettono di ragionare con deduzioni sulle deduzioni, e definisce l’equivalenza dimostrabile. Infine, stabilisce senza ricorrere ai valori di verità il limite di quel sistema in una lingua il cui unico connettivo è la negazione congiunta: una marcatura a valori 00 e 11, calcolata per ricorsione sulle formule, che gli assiomi di Łukasiewicz e il modus ponens conservano, prova che certe formule che dovrebbero dedursi non si deducono, e che non si passa neppure da (v1↓v2)(v_{1} \downarrow v_{2}) a (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}). Ne segue la necessità di una seconda regola, la sostituzione della doppia negazione, con cui la lezione successiva completa il sistema.

Obiettivi di apprendimento

  1. Riconoscere le istanze degli schemi A1, A2 e A3 e decidere se una successione di formule è una deduzione da un insieme di premesse.
  2. Costruire deduzioni nel sistema di Łukasiewicz, con assiomi, premesse e modus ponens, e deduzioni sulle deduzioni con riflessività, monotonia, taglio, il teorema di deduzione e il suo inverso.
  3. Dimostrare le proprietà strutturali della deduzione e il teorema di deduzione per induzione forte sul numero di righe.
  4. Stabilire equivalenze dimostrabili e usare il fatto che l’equivalenza dimostrabile è riflessiva, simmetrica e transitiva.
  5. Dimostrare che una formula non è deducibile mediante una marcatura che gli assiomi e il modus ponens conservano, e spiegare con essa il limite del sistema di Łukasiewicz nella lingua di un solo connettivo e perché occorre una seconda regola.

Che cos’è un sistema deduttivo formale

L’unità precedente ha costruito un linguaggio: ha deciso quali stringhe di cerchi e dischi sono formule, e nient’altro. Ora, un linguaggio da solo non afferma né dimostra nulla; per dimostrare occorrono, inoltre, un punto di partenza e un modo di avanzare. Un sistema deduttivo formale consta, pertanto, di tre componenti: un linguaggio formale, che fissa le formule; un insieme di assiomi, formule che si ammettono senza dimostrazione; e un insieme di regole d’inferenza, che dicono quale formula si può scrivere a partire da altre già scritte. Il punto decisivo è che le tre cose sono puramente sintattiche: per verificare che una formula è un assioma, o che una regola è stata applicata bene, basta guardare le stringhe, senza chiedersi che cosa significhino. Se è così, una dimostrazione in un sistema formale può essere controllata meccanicamente, simbolo per simbolo, e in questa possibilità risiede tutto il suo valore.

Conviene avvertire fin dall’inizio che un assioma non è qui una «verità evidente di per sé», come nell’uso antico della parola, ma una formula scelta come punto di partenza. Che la scelta sia azzeccata (che gli assiomi siano veri in un senso che la semantica preciserà, e che bastino a dedurre tutto ciò che deve dedursi) è una domanda sul sistema, a cui si risponde con teoremi su di esso e non con l’intuizione: l’unità sulla metateoria vi risponde, e l’ultima sezione di questa lezione mostra che la domanda non è oziosa.

Schemi di assiomi e istanze

I sistemi della logica proposizionale non enunciano i loro assiomi uno per uno, perché sono infiniti, ma mediante schemi: espressioni del metalinguaggio scritte con metavariabili, come (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)). Uno schema non è una formula; è uno stampo. Un’istanza dello schema è la formula che risulta dal cambiare ogni metavariabile con una formula, in modo uniforme: tutte le occorrenze di una stessa metavariabile si cambiano con la stessa formula, sebbene metavariabili distinte possano ricevere la stessa formula o formule distinte.

EsempioIstanze di uno schema

Con φ:=v1\varphi := v_{1} e ψ:=¬v2\psi := \neg v_{2}, lo schema (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) dà l’istanza (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1})); con φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) e ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}), dà ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))), perché nulla impedisce che due metavariabili ricevano la stessa formula. Invece, (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) non è istanza di quello schema: la prima e l’ultima occorrenza di φ\varphi riceverebbero formule distinte, e il cambio non sarebbe uniforme. Ogni istanza, una volta sviluppate le abbreviazioni, è una stringa di cerchi e dischi; lo schema, invece, vive solo nel metalinguaggio.