Vai al contenuto
Topos Uranos

Riepilogo

Questa lezione chiude l’unità dedicata alla deduzione. Ricostruisce la catena deduttiva che va dalla definizione del sistema di Łukasiewicz (tre schemi di assiomi e il modus ponens) al teorema di deduzione e al limite di quel sistema nella lingua della negazione congiunta; da lì alle quattro tecniche di base e alla regola della sostituzione della doppia negazione, che completa il sistema del corso; dal lemma fondamentale della negazione congiunta alla sostituzione di equivalenti e alle simmetrie, e da lì alle regole della logica classica e alle leggi di De Morgan e alle leggi distributive, indicando a ogni anello quali risultati usa e in quale lezione si dimostra. Distingue ciò che l’unità ha dimostrato da ciò che ha ammesso, colloca quanto ottenuto rispetto al piano del corso e spiega perché la domanda che l’unità lascia aperta, quella di sapere se il deducibile coincide con il vero, conduce all’unità di semantica. Ripete nella sua valutazione d’uscita le abilità della valutazione d’ingresso e termina con sei sfide, di difficoltà superiore a quella dei problemi delle lezioni, che richiedono di combinare gli strumenti di più lezioni.

Obiettivi di apprendimento

  1. Ricostruire l’ordine logico dei risultati dell’unità, identificando i risultati precedenti su cui ciascuno si appoggia e la lezione in cui si dimostra.
  2. Spiegare come si concatenano il teorema di deduzione, la doppia negazione, la regola della sostituzione della doppia negazione, la contrapposizione, il lemma fondamentale e la sostituzione di equivalenti, e perché da essi dipendono le regole classiche, le leggi di De Morgan e le leggi distributive.
  3. Distinguere ciò che l’unità ha dimostrato da ciò che ha ammesso (gli schemi di assiomi, le due regole primitive, l’induzione forte, quella strutturale e la leggibilità unica) e da ciò che ha lasciato alle unità seguenti, in particolare la relazione tra deduzione e verità.
  4. Risolvere problemi che combinano le marcature, la regola della sostituzione della doppia negazione, il teorema di deduzione, la dimostrazione per casi, la riduzione all’assurdo, la sostituzione di equivalenti, le leggi di De Morgan e le leggi distributive.

Ciò che l’unità ha ottenuto

L’unità si era proposta di dotare il linguaggio dell’unità precedente di un sistema deduttivo, cioè di un modo puramente sintattico di ottenere formule a partire da altre, e di dimostrare con quel sistema, riga per riga, le tecniche con cui ragiona la matematica. Il proposito è stato raggiunto con poche riserve, ciascuna dichiarata al suo posto: i tre schemi di assiomi e le due regole primitive, che non si dimostrano ma si scelgono, e la cui scelta appropriata è una domanda che l’unità pone senza rispondervi del tutto; l’induzione forte e quella strutturale, la leggibilità unica e la definizione per ricorsione, che sono state dimostrate nell’unità precedente e qui si usano; e l’indispensabile della teoria degli insiemi (sottoinsiemi, unioni e insiemi finiti), che è stato richiamato dove serviva. Con queste riserve, il cammino percorso può leggersi come un’unica catena deduttiva in quattro tratti.

Il sistema di Łukasiewicz e il suo limite

La lezione sui sistemi deduttivi formali ha definito un sistema come un linguaggio, alcuni assiomi e alcune regole, tutti verificabili guardando soltanto le stringhe, e ha fissato la prima tappa del sistema del corso, il sistema di Łukasiewicz: gli schemi A1, A2 e A3 e il modus ponens come unica regola, che la leggibilità unica rende applicabile senza ambiguità. Ha definito la deduzione da un insieme Γ\Gamma di premesse e la relazione Γ⊢φ\Gamma \vdash \varphi, ha dedotto ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) in cinque righe e ha dimostrato le proprietà strutturali: riflessività, monotonia, modus ponens tra deduzioni, taglio e finitezza. Con esse e con l’induzione forte sul numero di righe ha dimostrato il teorema di deduzione, il cui secondo caso richiede di aver dedotto prima (φ→φ)(\varphi \rightarrow \varphi), e il suo inverso; da essi ha ottenuto l’equivalenza dimostrabile, riflessiva, simmetrica e transitiva. Infine, ha stabilito il limite di quel sistema: una marcatura a valori 00 e 11, definita per ricorsione sulla forma primitiva (α↓β)(\alpha \downarrow \beta), tratta la negazione e l’implicazione come sempre, è conservata da A1, A2, A3 e dal modus ponens, e lascia libero il valore di formule come (v1↓v2)(v_{1} \downarrow v_{2}). Ne segue che ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) non è un teorema del sistema di Łukasiewicz, e che da (v1↓v2)(v_{1} \downarrow v_{2}) non si deduce (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}), né viceversa. Poiché ogni marcatura dà lo stesso valore a θ\theta e a ¬¬θ\neg\neg\theta, la lezione ha inoltre avvertito che nemmeno la doppia negazione, una volta dimostrata, avrebbe rimediato a quel limite.

Le quattro tecniche e la regola nuova

La lezione sulle quattro tecniche di deduzione ha dimostrato anzitutto il lemma «dal risultato alla regola»: se {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta, la stessa conclusione si ottiene da qualunque Γ\Gamma che deduca le αi\alpha_{i}, e inoltre ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)). È questo lemma a permettere di usare ogni tecnica in tre presentazioni (da premesse, come teorema e come regola), e le lezioni sulle simmetrie e su De Morgan, che riuniscono catene di equivalenze con il taglio, si appoggiano a tal fine sulle proprietà dell’equivalenza dimostrabile della prima lezione, che sono la stessa idea applicata a una sola premessa; nella catena ogni risultato figura una sola volta, dove si dimostra. Con esso, la lezione ha dedotto il sillogismo ipotetico da A1 e A2 in sette righe, lo scambio delle premesse con il teorema di deduzione, la doppia negazione (la cui prima direzione applica A3 due volte a un’implicazione fabbricata con A1, e la cui seconda applica la prima a ¬φ\neg\varphi e A3) e la contrapposizione nelle sue tre forme, che ripartiscono in tre modi le negazioni di un’implicazione; tutte e quattro valgono già nel sistema di Łukasiewicz.

Dimostrata la doppia negazione, la lezione ha completato il sistema del corso con una seconda regola primitiva, la sostituzione della doppia negazione (SDN): da χ\chi si inferisce χ′\chi' quando χ′\chi' risulta dal sostituire in χ\chi un’occorrenza di una sottoformula θ\theta con ¬¬θ\neg\neg\theta, o una di ¬¬θ\neg\neg\theta con θ\theta. La regola deve essere postulata, perché la marcatura m1m_{1} dà 11 ai teoremi della doppia negazione e, tuttavia, separa (v1↓v2)(v_{1} \downarrow v_{2}) da (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}); SDN non conserva m1m_{1}, e per questo amplia il deducibile, ma conserva la marcatura onesta, e per questo non lo amplia troppo. La regola agisce sulla stringa della lingua di base, dove una negazione duplica il suo argomento: (φ→ψ)(\varphi \rightarrow \psi) contiene due volte la sottoformula ¬φ\neg\varphi, e mettere una doppia negazione davanti al suo antecedente richiede due applicazioni. La stessa osservazione sostiene l’estensione del teorema di deduzione: se una riga si ottiene con la regola, l’ipotesi induttiva dà l’implicazione il cui conseguente è la riga precedente, e due applicazioni della regola, una in ciascuna copia di quel conseguente, danno l’implicazione cercata; le altre proprietà strutturali valgono con la stessa dimostrazione. Le prime conseguenze sono che una formula equivale a ogni formula che ne risulti con la regola, in particolare (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) e (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi), e che le implicazioni corrispondenti, che altri sistemi prendono come assiomi, sono qui teoremi.

Connettivi e sostituzione

La lezione sulle simmetrie dei connettivi ha affrontato la difficoltà propria della lingua dei cerchi e dei dischi: gli assiomi di Łukasiewicz parlano solo di negazioni e di implicazioni, e quasi nessuna negazione congiunta è l’una o l’altra cosa. Il lemma fondamentale, (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi), getta il ponte: poiché ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) è ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi), la regola SDN mette la doppia negazione interna e la doppia negazione quella esterna; in senso inverso, la doppia negazione e la regola le tolgono. Con esso, la sostituzione di equivalenti, dimostrata prima sotto la negazione e ai due lati dell’implicazione con la contrapposizione e il sillogismo ipotetico, è stata estesa a entrambi gli argomenti della negazione congiunta e, da lì, alla disgiunzione e alla congiunzione. La regola e la sostituzione non si rendono superflue a vicenda: la regola scambia soltanto θ\theta e ¬¬θ\neg\neg\theta, mentre la sostituzione ammette equivalenti qualsiasi; e la sostituzione, dimostrata con il lemma fondamentale, poggia a sua volta sulla regola. La lezione ha poi dimostrato che le forme che altri testi prendono per definizioni sono equivalenze: (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi), che richiede due applicazioni della regola, una in ciascuna copia che crea la negazione esterna, e (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi), che richiede la doppia negazione; invece, (φ∧ψ)(\varphi \wedge \psi) e ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi) sono la stessa stringa. Infine, ha dimostrato le cinque simmetrie nell’ordine che impongono le definizioni: quella della negazione congiunta con il lemma fondamentale e la contrapposizione, e ciascuna delle altre con la precedente, trasportata con la sostituzione sotto la negazione quando serve.

Le regole classiche e le leggi

La lezione sulle tecniche della logica classica ha dimostrato, tutte con un insieme Γ\Gamma di premesse che si trascina di riga in riga, l’introduzione e l’eliminazione della disgiunzione e della congiunzione, il terzo escluso e la non contraddizione, l’esplosione, la riduzione all’assurdo nelle sue due forme e la dimostrazione per casi, con una formula e la sua negazione e con una disgiunzione qualsiasi. L’ordine delle dipendenze è stretto: l’esplosione poggia sulle regole della disgiunzione; la riduzione all’assurdo classica, sull’esplosione e su A3; la dimostrazione per casi, sulla contrapposizione e sulla riduzione all’assurdo. Nessuna di queste dimostrazioni invoca direttamente la regola SDN: la regola agisce attraverso le forme equivalenti e la sostituzione di equivalenti. La lezione sulle leggi di De Morgan e leggi distributive ha messo queste regole a lavorare insieme: la prima legge di De Morgan risulta dalla definizione della congiunzione e dalla doppia negazione; la seconda richiede di entrare nella negazione congiunta, dove la regola SDN interviene due volte, una in ciascun argomento e senza bisogno della simmetria, e da essa segue che (φ↓ψ)(\varphi \downarrow \psi) equivale a (¬φ∧¬ψ)(\neg\varphi \wedge \neg\psi), la lettura «né φ\varphi né ψ\psi» che l’unità precedente aveva stipulato; le varianti includono ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi). Le due leggi distributive sono state dimostrate nei loro due sensi per casi, scegliendo in ciascuno la forma della dimostrazione per casi che conviene.

La figura seguente riunisce i quattro tratti in un’unica catena. Ogni nodo della colonna è una definizione o un risultato, numerato secondo l’ordine logico e unito da un arco agli anelli precedenti che la sua dimostrazione usa; attorno fluttuano i sostegni, cioè i principi e gli strumenti a cui la catena ricorre di continuo, ciascuno unito da un tratto pieno agli anelli che vi si appoggiano e da uno punteggiato all’anello in cui viene stabilito, salvo quelli che questa catena non dimostra (gli schemi di assiomi, che si ammettono, e gli strumenti dell’unità precedente), che si disegnano come corone circolari. La regola della sostituzione della doppia negazione, benché anch’essa si ammetta senza dimostrazione, figura unita all’anello che la introduce, perché lì si spiega perché debba essere postulata. Facendo clic su un sostegno si evidenziano tutti gli anelli che lo usano, e ogni anello rimanda alla lezione in cui si dimostra. Si osservi che il teorema di deduzione e la doppia negazione sono, dopo gli assiomi, i sostegni più visitati dell’unità, e che la regola nuova sostiene tutto ciò che l’unità dice della negazione congiunta: il teorema di deduzione esteso, il lemma fondamentale, le forme equivalenti e la seconda legge di De Morgan.

Sostegni della catena

  • ALeggibilità unica e ricorsione. Se ∙φψ=∙φ′ψ′\sigI\varphi\psi = \sigI\varphi'\psi', con le quattro stringhe formule, allora φ=φ′\varphi = \varphi' e ψ=ψ′\psi = \psi'; donde una regola che calcola il valore di ∙φψ\sigI\varphi\psi a partire da φ\varphi, da ψ\psi e dai loro valori definisce una sola funzione sulle formule. È stata dimostrata nell’unità precedente. Ammesso senza dimostrazione in questa unità.
  • BInduzione forte. Se una proprietà vale per un naturale ogni volta che vale per tutti i minori, vale per tutti i naturali. È stata dedotta dall’induzione semplice nell’unità precedente, e qui si applica al numero di righe di una deduzione. Ammesso senza dimostrazione in questa unità.
  • CAssiomi di Łukasiewicz. Gli schemi A1, (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)); A2, ((φ→(ψ→χ))→((φ→ψ)→(φ→χ)))((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi))); e A3, ((¬ψ→¬φ)→(φ→ψ))((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi)). Si ammettono. Ammesso senza dimostrazione in questa unità.
  • DSostituzione della doppia negazione. Seconda regola primitiva del sistema del corso: da χ\chi si inferisce χ′\chi' se χ′\chi' risulta da χ\chi sostituendo un’occorrenza di una sottoformula θ\theta con ¬¬θ\neg\neg\theta, o una di ¬¬θ\neg\neg\theta con θ\theta. Si postula dopo aver dimostrato la doppia negazione. Stabilito in: 8. Sostituzione della doppia negazione.
  • ETeorema di deduzione. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi se e solo se Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi); si dimostra nel sistema di Łukasiewicz e vale, con un caso in più, nel sistema del corso. Stabilito in: 3. Teorema di deduzione ed equivalenza dimostrabile.
  • FDal risultato alla regola. Se {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta e Γ⊢αi\Gamma \vdash \alpha_{i} per ogni ii, allora Γ⊢β\Gamma \vdash \beta: ogni tecnica dimostrata da premesse si applica sotto qualunque insieme di premesse. Stabilito in: 5. Dal risultato alla regola.
  • GDoppia negazione. φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, con i teoremi ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) e ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi). Stabilito in: 7. Doppia negazione.
  • HSostituzione di equivalenti. Se φ⊣⊢φ′\varphi \dashv\vdash \varphi', si può mettere φ′\varphi' al posto di φ\varphi sotto una negazione, ai due lati di un’implicazione, di una negazione congiunta, di una disgiunzione e di una congiunzione, senza alterare l’equivalenza. Stabilito in: 12. Sostituzione di equivalenti.
  1. Tratto 1 Il sistema di Łukasiewicz e il suo limite

    • Riconoscere le istanze degli schemi e decidere se una successione di formule è una deduzione da un insieme di premesse.
    • Dimostrare le proprietà strutturali della deduzione e il teorema di deduzione per induzione forte sul numero di righe.
    • Costruire deduzioni sulle deduzioni con riflessività, monotonia, taglio, il teorema di deduzione e il suo inverso.
    • Dimostrare che una formula non si deduce mediante una marcatura che gli assiomi e il modus ponens conservano, e spiegare con essa il limite del sistema di Łukasiewicz.
    1. Sistema, deduzione e identità. Gli assiomi del sistema di Łukasiewicz sono le istanze uniformi degli schemi da A1 ad A3, e la sua unica regola è il modus ponens. Γ⊢φ\Gamma \vdash \varphi se esiste una successione finita di formule che termina in φ\varphi, ciascuna delle quali è un assioma, un elemento di Γ\Gamma o è ottenuta con il modus ponens da due precedenti. Il primo teorema, ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi), si deduce in cinque righe con A1 e A2.

      Si appoggia su: A (Leggibilità unica e ricorsione), C (Assiomi di Łukasiewicz). Dimostrato in: Sistemi deduttivi formali.

    2. Proprietà strutturali. Se φ∈Γ\varphi \in \Gamma, Γ⊢φ\Gamma \vdash \varphi; se Γ⊆Δ\Gamma \subseteq \Delta e Γ⊢φ\Gamma \vdash \varphi, Δ⊢φ\Delta \vdash \varphi; da Γ⊢φ\Gamma \vdash \varphi e Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) segue Γ⊢ψ\Gamma \vdash \psi; se Γ⊢φi\Gamma \vdash \varphi_{i} per ogni ii e Γ∪{φ1,…,φr}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{r}\} \vdash \psi, Γ⊢ψ\Gamma \vdash \psi; e se Γ⊢φ\Gamma \vdash \varphi, basta qualche sottoinsieme finito di Γ\Gamma.

      Usa: 1. Sistema, deduzione e identità. Dimostrato in: Sistemi deduttivi formali.

    3. Teorema di deduzione ed equivalenza dimostrabile. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi se e solo se Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), per induzione forte sul numero di righe, con A1, A2 e l’identità. Ne segue che l’equivalenza dimostrabile, φ⊣⊢ψ\varphi \dashv\vdash \psi, è riflessiva, simmetrica e transitiva, e che due formule equivalenti si deducono dagli stessi insiemi.

      Usa: 1. Sistema, deduzione e identità, 2. Proprietà strutturali. Si appoggia su: B (Induzione forte), C (Assiomi di Łukasiewicz). Dimostrato in: Sistemi deduttivi formali.

    4. Limite del sistema di Łukasiewicz. Una marcatura a valori 00 e 11 definita per ricorsione soddisfa m(¬φ)=1−m(φ)m(\neg\varphi) = 1 - m(\varphi) e m((φ→ψ))=1−m(φ)(1−m(ψ))m((\varphi \rightarrow \psi)) = 1 - m(\varphi) \left( 1 - m(\psi) \right), e A1, A2, A3 e il modus ponens conservano la marcatura 11; donde ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) non è un teorema del sistema di Łukasiewicz, e {(v1↓v2)}⊬(¬¬v1↓v2)\{(v_{1} \downarrow v_{2})\} \nvdash (\neg\neg v_{1} \downarrow v_{2}), né viceversa. Poiché ogni marcatura dà 11 alla doppia negazione, la sostituzione deve essere postulata.

      Usa: 1. Sistema, deduzione e identità. Si appoggia su: A (Leggibilità unica e ricorsione), B (Induzione forte), C (Assiomi di Łukasiewicz). Dimostrato in: Sistemi deduttivi formali.

  2. Tratto 2 Le quattro tecniche e la regola nuova

    • Convertire un risultato da premesse in un teorema e in una regola applicabile sotto qualunque insieme di premesse.
    • Concatenare implicazioni, riordinare antecedenti, mettere e togliere doppie negazioni e scegliere la forma della contrapposizione che corrisponde a ciascuna implicazione.
    • Applicare la regola della sostituzione della doppia negazione, individuando le occorrenze che le abbreviazioni nascondono e ripetendola in ciascuna copia che crea una negazione.
    • Spiegare con la marcatura perché la regola si postula, e dimostrare che il teorema di deduzione vale con essa.
    1. Dal risultato alla regola. Se {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta, allora da Γ⊢α1\Gamma \vdash \alpha_{1}, …\ldots, Γ⊢αn\Gamma \vdash \alpha_{n} segue Γ⊢β\Gamma \vdash \beta, e ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)); in particolare, se α⊣⊢α′\alpha \dashv\vdash \alpha', Γ⊢α\Gamma \vdash \alpha se e solo se Γ⊢α′\Gamma \vdash \alpha'.

      Usa: 2. Proprietà strutturali. Si appoggia su: E (Teorema di deduzione). Dimostrato in: Quattro tecniche di deduzione.

    2. Sillogismo ipotetico e scambio. {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi), con una deduzione di sette righe da A1 e A2; e {(φ→(ψ→χ))}⊢(ψ→(φ→χ))\{(\varphi \rightarrow (\psi \rightarrow \chi))\} \vdash (\psi \rightarrow (\varphi \rightarrow \chi)).

      Usa: 1. Sistema, deduzione e identità. Si appoggia su: C (Assiomi di Łukasiewicz), E (Teorema di deduzione), F (Dal risultato alla regola). Dimostrato in: Quattro tecniche di deduzione.

    3. Doppia negazione. ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi), applicando A3 due volte a un’implicazione che A1 fabbrica a partire da ¬¬φ\neg\neg\varphi; ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi), applicando quanto precede a ¬φ\neg\varphi e A3; donde φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, già nel sistema di Łukasiewicz.

      Si appoggia su: C (Assiomi di Łukasiewicz), E (Teorema di deduzione). Dimostrato in: Quattro tecniche di deduzione.

    4. Sostituzione della doppia negazione. Si postula la regola SDN, perché la marcatura dà 11 alla doppia negazione e non alla sostituzione dentro una negazione congiunta. Se χ′\chi' risulta da χ\chi con la regola, χ⊣⊢χ′\chi \dashv\vdash \chi'; in particolare, (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) e (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi).

      Usa: 3. Teorema di deduzione ed equivalenza dimostrabile, 4. Limite del sistema di Łukasiewicz. Si appoggia su: G (Doppia negazione). Dimostrato in: Quattro tecniche di deduzione.

    5. Teorema di deduzione nel sistema del corso. Riflessività, monotonia, taglio e finitezza valgono con la regola nuova, e così pure Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi se e solo se Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi): nel caso nuovo, poiché (φ→χ)(\varphi \rightarrow \chi) è ((¬φ↓χ)↓(¬φ↓χ))((\neg\varphi \downarrow \chi) \downarrow (\neg\varphi \downarrow \chi)), la regola si applica due volte, una in ciascuna copia di χ\chi. Ne segue che ⊢((φ↓ψ)→(¬¬φ↓ψ))\vdash ((\varphi \downarrow \psi) \rightarrow (\neg\neg\varphi \downarrow \psi)) e il suo inverso sono teoremi.

      Usa: 2. Proprietà strutturali, 3. Teorema di deduzione ed equivalenza dimostrabile. Si appoggia su: B (Induzione forte), D (Sostituzione della doppia negazione). Dimostrato in: Quattro tecniche di deduzione.

    6. Contrapposizione. (φ→ψ)⊣⊢(¬ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), (¬φ→ψ)⊣⊢(¬ψ→φ)(\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi) e (φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi): i membri cambiano lato, e ciascuno cambia segno nel passare.

      Usa: 6. Sillogismo ipotetico e scambio. Si appoggia su: C (Assiomi di Łukasiewicz), E (Teorema di deduzione), G (Doppia negazione), F (Dal risultato alla regola). Dimostrato in: Quattro tecniche di deduzione.

  3. Tratto 3 Connettivi e sostituzione

    • Sviluppare le abbreviazioni per decidere se due espressioni designano la stessa stringa o formule la cui equivalenza richiede una deduzione.
    • Tradurre la negazione congiunta nella negazione e nell’implicazione con il lemma fondamentale.
    • Portare un’equivalenza all’interno di una formula con la sostituzione di equivalenti, distinguerla dalla regola della sostituzione della doppia negazione e concatenare equivalenze.
    • Dimostrare le cinque simmetrie nell’ordine che impongono le definizioni.
    1. Lemma fondamentale. (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi): poiché ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) è ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi), la regola SDN mette la doppia negazione interna e la doppia negazione quella esterna; in senso inverso, la doppia negazione e la regola le tolgono.

      Si appoggia su: D (Sostituzione della doppia negazione), G (Doppia negazione). Dimostrato in: Le simmetrie dei connettivi.

    2. Sostituzione di equivalenti. Se φ⊣⊢φ′\varphi \dashv\vdash \varphi', allora ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi', (φ→ψ)⊣⊢(φ′→ψ)(\varphi \rightarrow \psi) \dashv\vdash (\varphi' \rightarrow \psi) e (ψ→φ)⊣⊢(ψ→φ′)(\psi \rightarrow \varphi) \dashv\vdash (\psi \rightarrow \varphi'); con il lemma fondamentale, lo stesso ai due lati della negazione congiunta, e da lì, della disgiunzione e della congiunzione. A differenza della regola SDN, ammette equivalenti qualsiasi.

      Usa: 6. Sillogismo ipotetico e scambio, 10. Contrapposizione, 11. Lemma fondamentale. Si appoggia su: E (Teorema di deduzione). Dimostrato in: Le simmetrie dei connettivi.

    3. Forme equivalenti. (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi), con due applicazioni della regola SDN, una in ciascuna copia che crea la negazione esterna; (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi), per la doppia negazione; e (φ∧ψ)(\varphi \wedge \psi) è la stessa stringa di ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi).

      Si appoggia su: D (Sostituzione della doppia negazione), G (Doppia negazione). Dimostrato in: Le simmetrie dei connettivi.

    4. Le cinque simmetrie. (φ↓ψ)⊣⊢(ψ↓φ)(\varphi \downarrow \psi) \dashv\vdash (\psi \downarrow \varphi), per il lemma fondamentale e la contrapposizione; da essa, successivamente, le simmetrie di ∨\vee, ∧\wedge, ↔\leftrightarrow e ⊻\veebar, ciascuna con la precedente, trasportata con la sostituzione sotto la negazione quando serve.

      Usa: 11. Lemma fondamentale, 10. Contrapposizione. Si appoggia su: H (Sostituzione di equivalenti). Dimostrato in: Le simmetrie dei connettivi.

  4. Tratto 4 Le regole classiche e le leggi

    • Dimostrare con premesse l’introduzione e l’eliminazione della disgiunzione e della congiunzione, il terzo escluso e la non contraddizione.
    • Dimostrare l’esplosione, la riduzione all’assurdo e la dimostrazione per casi con premesse, e spiegare perché senza di esse non bastano.
    • Dimostrare per deduzione le leggi di De Morgan, le loro varianti e le leggi distributive nei loro due sensi.
    • Trasformare formule in forme normali semplici mediante catene di equivalenze giustificate.
    1. Regole dei connettivi. Con qualunque Γ\Gamma: da φ\varphi segue (φ∨ψ)(\varphi \vee \psi); da (φ∨ψ)(\varphi \vee \psi) e ¬φ\neg\varphi, ψ\psi; da φ\varphi e ψ\psi, (φ∧ψ)(\varphi \wedge \psi); da (φ∧ψ)(\varphi \wedge \psi), φ\varphi e ψ\psi; inoltre, ⊢(φ∨¬φ)\vdash (\varphi \vee \neg\varphi) e ⊢¬(φ∧¬φ)\vdash \neg(\varphi \wedge \neg\varphi).

      Usa: 1. Sistema, deduzione e identità, 2. Proprietà strutturali, 6. Sillogismo ipotetico e scambio, 10. Contrapposizione, 13. Forme equivalenti, 14. Le cinque simmetrie. Si appoggia su: C (Assiomi di Łukasiewicz), E (Teorema di deduzione), F (Dal risultato alla regola), G (Doppia negazione). Dimostrato in: Le tecniche della logica classica.

    2. Esplosione e riduzione all’assurdo. Se Γ⊢φ\Gamma \vdash \varphi e Γ⊢¬φ\Gamma \vdash \neg\varphi, allora Γ⊢ψ\Gamma \vdash \psi per ogni ψ\psi; se Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} deduce ψ\psi e ¬ψ\neg\psi, allora Γ⊢φ\Gamma \vdash \varphi; e se Γ∪{φ}\Gamma \cup \{\varphi\} le deduce, Γ⊢¬φ\Gamma \vdash \neg\varphi.

      Usa: 1. Sistema, deduzione e identità, 2. Proprietà strutturali, 15. Regole dei connettivi. Si appoggia su: C (Assiomi di Łukasiewicz), E (Teorema di deduzione), G (Doppia negazione). Dimostrato in: Le tecniche della logica classica.

    3. Dimostrazione per casi. Se Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi e Γ∪{¬φ}⊢ψ\Gamma \cup \{\neg\varphi\} \vdash \psi, allora Γ⊢ψ\Gamma \vdash \psi; e se Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi, Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi e Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi), allora Γ⊢χ\Gamma \vdash \chi.

      Usa: 2. Proprietà strutturali, 10. Contrapposizione, 15. Regole dei connettivi, 16. Esplosione e riduzione all’assurdo. Si appoggia su: E (Teorema di deduzione). Dimostrato in: Le tecniche della logica classica.

    4. Leggi di De Morgan. ¬(φ∧ψ)⊣⊢(¬φ∨¬ψ)\neg(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \vee \neg\psi), per la definizione e la doppia negazione; ¬(φ∨ψ)⊣⊢(¬φ∧¬ψ)\neg(\varphi \vee \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi), con un’applicazione della regola SDN in ciascun argomento della negazione congiunta; donde (φ↓ψ)⊣⊢(¬φ∧¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi) e ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi).

      Si appoggia su: D (Sostituzione della doppia negazione), G (Doppia negazione), H (Sostituzione di equivalenti). Dimostrato in: Leggi di De Morgan e leggi distributive.

    5. Leggi distributive. (φ∧(ψ∨χ))⊣⊢((φ∧ψ)∨(φ∧χ))(\varphi \wedge (\psi \vee \chi)) \dashv\vdash ((\varphi \wedge \psi) \vee (\varphi \wedge \chi)) e (φ∨(ψ∧χ))⊣⊢((φ∨ψ)∧(φ∨χ))(\varphi \vee (\psi \wedge \chi)) \dashv\vdash ((\varphi \vee \psi) \wedge (\varphi \vee \chi)), ciascuna nei suoi due sensi per casi; con le simmetrie, anche da destra.

      Usa: 14. Le cinque simmetrie, 15. Regole dei connettivi, 17. Dimostrazione per casi. Si appoggia su: H (Sostituzione di equivalenti). Dimostrato in: Leggi di De Morgan e leggi distributive.

Verso la semantica. La catena si ferma dove la deduzione raggiunge tutte le tecniche con cui ragiona la matematica. Resta da sapere se ciò che si deduce è esattamente ciò che è vero in ogni assegnazione: l’unità seguente definirà la verità, e l’ultima confronterà le due nozioni.

Le abbreviazioni delle giustificazioni

Le deduzioni dell’unità giustificano ogni riga con un’abbreviazione, la stessa in tutte le lezioni. Sono riunite qui, ordinate secondo la lezione che le introduce. «Premessa» designa un’ipotesi dell’enunciato e, nelle deduzioni sulle deduzioni, un’ipotesi della regola che si dimostra. I numeri tra parentesi citano le righe a cui si applica la regola; un’equivalenza già dimostrata si cita senza numero quando si scrive come riga, e con il numero della riga che trasforma quando si applica a quella riga, anche a una delle sue parti con «Sost».

  • Prima lezione: A1, A2 e A3 (gli schemi di assiomi); MP(i,j)(i, j) (modus ponens); Def (espansione o contrazione di un’abbreviazione, con il connettivo che si sviluppa: «Def ∨\vee», «Def ⊣⊢\dashv\vdash»); Id (identità, il teorema ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)); Rifl (riflessività: se φ∈Γ\varphi \in \Gamma, allora Γ⊢φ\Gamma \vdash \varphi); Mon (monotonia); Taglio (ciò che è stato dedotto può essere usato come premessa); Fin (finitezza); TD (teorema di deduzione) e RTD (il suo inverso).
  • Seconda lezione: SI (sillogismo ipotetico); SP (scambio delle premesse); DN (doppia negazione); SDN(i)(i) (sostituzione della doppia negazione nella riga ii; SDN senza numero cita l’equivalenza tra una formula e quella che ne risulta con la regola); CP (contrapposizione, in una qualsiasi delle sue tre forme); «Risolto nn» (un risultato del problema risolto nn della stessa lezione, scritto come riga).
  • Terza lezione: LF (lemma fondamentale, (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)); Sost (sostituzione di equivalenti, in una qualsiasi delle sue forme, seguita dall’equivalenza che si applica: «Sost, DM(i)(i)»); Eq (forme equivalenti della disgiunzione e della congiunzione, (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) e (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)); Sim (simmetria di un connettivo).
  • Quarta lezione: ∨\veeI e ∨\veeE (introduzione ed eliminazione della disgiunzione); ∧\wedgeI e ∧\wedgeE (introduzione ed eliminazione della congiunzione); TE (terzo escluso); NC (non contraddizione; l’abbreviazione nomina il teorema, ma non giustifica nessuna riga dell’unità); Espl (esplosione); Casi(i,j)(i, j) e Casi(i,j,k)(i, j, k) (dimostrazione per casi, con una formula e la sua negazione o con una disgiunzione); «Casi senza premesse» (la dimostrazione per casi senza insieme Γ\Gamma, che compare solo in un problema); RA (riduzione all’assurdo, nelle sue due forme).
  • Quinta lezione: DM (leggi di De Morgan); Dist (distributività); Assoc (associatività della disgiunzione); Istanza(i)(i) (la riga ii, che vale per formule qualsiasi, riscritta con altre formule al posto delle sue metavariabili; si indica il cambio).
  • Sfide di questa lezione: M3 (lo schema che la terza sfida mette al posto di A3).