Semantica: sintesi e sfide

Riepilogo

Questa lezione chiude l’unità dedicata alla semantica. Ricostruisce la catena deduttiva che va dall’estensione di un’assegnazione a tutte le formule e dal lemma di coincidenza alla conseguenza, all’equivalenza e ai loro due teoremi di lavoro, la sostituzione e la sostituzione uniforme; da lì alle leggi per un numero qualsiasi di termini, alla completezza funzionale e agli insiemi di connettivi, e da lì alle forme normali, al loro algoritmo e ai circuiti, indicando in ogni anello quali risultati usa e in quale lezione si dimostra. Distingue ciò che l’unità ha dimostrato da ciò che ha preso dalle precedenti, decide in tre modi un argomento che il corso porta con sé dalla prima unità e spiega perché la domanda che l’unità lascia aperta, quella di sapere se ciò che è vero in ogni assegnazione coincide con ciò che è derivabile, conduce alla metateoria. Ripete nella sua valutazione d’uscita le abilità della valutazione d’ingresso e termina con sei sfide, più difficili dei problemi delle lezioni, che richiedono di combinare gli strumenti di parecchie di esse.

Obiettivi di apprendimento

Ricostruire l’ordine logico dei risultati dell’unità, identificando i risultati precedenti su cui ciascuno si appoggia e la lezione in cui si dimostra.
Spiegare come l’estensione ricorsiva, il lemma di coincidenza, la sostituzione semantica e le leggi generalizzate conducono alla completezza funzionale, all’esistenza delle forme normali e alla correttezza e alla terminazione del loro algoritmo.
Distinguere ciò che l’unità ha dimostrato da ciò che ha preso dalle precedenti e da ciò che ha lasciato alla metateoria, in particolare la coincidenza della conseguenza semantica con la derivabilità, e la compattezza.
Risolvere problemi che combinano il calcolo con valori, la conseguenza, la sostituzione uniforme, gli insiemi di connettivi, le forme normali e i circuiti.

Che cosa ha ottenuto l’unità

L’unità si era proposta di dare significato alle formule del linguaggio costruito nella prima unità, senza toccare il sistema deduttivo della seconda, e di ricavare da quel significato procedimenti per decidere le domande che la logica pone su di esse: se una formula è valida, se è soddisfacibile, se segue da altre, se dice lo stesso di un’altra. Il proposito è stato realizzato con alcune riserve, ciascuna dichiarata al suo posto: la bivalenza e la verofunzionalità, che non si dimostrano ma si scelgono, e il cui prezzo è stato mostrato dalla lezione sulla formalizzazione; la leggibilità unica, la definizione per ricorsione, l’induzione e le abbreviazioni ufficiali, che sono state dimostrate o fissate nella prima unità e qui si usano; e i fatti indispensabili su insiemi e funzioni, che sono stati richiamati dove servivano. Con queste riserve, il cammino percorso può leggersi come un’unica catena deduttiva in sei tratti, uno per lezione.

Il valore di una formula

La lezione sulla semantica della logica proposizionale ha definito un’assegnazione come una funzione dalle variabili in $\{0, 1\}$ e ha dimostrato, con il teorema di definizione per ricorsione sulle formule, che si estende in modo unico a tutte le formule con una sola clausola: $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ . A partire dalle abbreviazioni ufficiali ha calcolato, senza stipulare nient’altro, il valore di ogni connettivo definito, scritto come un polinomio nei valori delle componenti, e con esso la tavola dell’implicazione, che qui è un teorema. Ha dimostrato per induzione sulla complessità il lemma di coincidenza, dal quale segue che la tavola di verità, con le sue $2^{n}$ righe, contiene tutto ciò che le infinite assegnazioni dicono di una formula con $n$ variabili; ha definito il soddisfacimento, la validità, la soddisfacibilità, la contraddizione e la contingenza, ha precisato che $\not\models \varphi$ dice che $\varphi$ non è valida e non che è contraddittoria, ha fissato $\top := (v_{1} \rightarrow v_{1})$ e $\bot := \neg\top$ , e ha ottenuto la decidibilità della validità e della soddisfacibilità, con un costo esponenziale che la ricerca diretta di un’assegnazione che falsifichi riduce senza eliminarlo.

Conseguenza ed equivalenza

La lezione sulla conseguenza e l’equivalenza semantica ha definito la conseguenza a partire da un insieme di premesse, finito o infinito, e ha dimostrato che ha le proprietà strutturali della deduzione (riflessività, monotonia, taglio e transitività), con dimostrazioni che passano per le assegnazioni invece di manipolare righe. Il teorema di deduzione semantico, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , si è ridotto all’unica riga falsa dell’implicazione, e la conseguenza si è ridotta all’insoddisfacibilità: $\Gamma \models \varphi \Leftrightarrow \Gamma \cup \{\neg\varphi\}$ è insoddisfacibile. L’equivalenza semantica, definita come uguaglianza di valori, si è rivelata coincidente con la conseguenza reciproca e con la validità della doppia implicazione. I suoi due teoremi di lavoro sono stati dimostrati per induzione sulla complessità: la sostituzione di un’occorrenza di una sottoformula con un’altra equivalente, con il caso dell’occorrenza totale, che non si può omettere, e la sostituzione uniforme di formule qualsiasi al posto delle variabili, che conserva la validità, l’equivalenza e la conseguenza. Grazie a essi, le leggi del catalogo, verificate come identità tra polinomi, si applicano in qualunque punto di qualunque formula e si possono concatenare.

Leggi per un numero qualsiasi di termini

La lezione sulle leggi generalizzate di De Morgan e distributive ha definito per ricorsione, associando a sinistra, la congiunzione e la disgiunzione di $n$ formule, e ha dimostrato per induzione sul numero di termini il lemma del valore, che dice che una congiunzione è vera se e solo se lo sono tutti i suoi termini e una disgiunzione se e solo se lo è qualcuno. Con esso e con la compatibilità dei connettivi con l’equivalenza ha ottenuto l’associatività generalizzata, che è stata dimostrata con una catena di equivalenze perché valga anche per l’equivalenza dimostrabile, l’indipendenza dall’ordine e dalle ripetizioni, le leggi di De Morgan generalizzate e la distributività generalizzata, la cui induzione su due indici è stata organizzata in modo che l’ipotesi induttiva copra tutte le lunghezze della seconda lista; la legge duale è stata ottenuta con De Morgan, senza ripetere la doppia induzione.

Funzioni di verità

La lezione sulla completezza funzionale ha percorso il cammino inverso, dalla tavola alla formula. Ha contato le funzioni di verità di $n$ argomenti, $2^{2^{n}}$ , ha mostrato che ogni formula ne rappresenta esattamente una e che due formule sono equivalenti se e solo se rappresentano la stessa, e ha dimostrato il teorema di completezza funzionale: la congiunzione di una riga è vera esattamente sulla sua riga, e la disgiunzione delle congiunzioni delle righe in cui la funzione vale $1$ la rappresenta. Poiché quella formula è una stringa di cerchi e dischi, la negazione congiunta basta da sola; con il criterio della negazione congiunta bastano anche $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ e la negazione alternativa; e con il principio di chiusura ha dimostrato che tutte le formule di $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ conservano il valore $1$ , sicché quell’insieme non basta.

Forme normali

La lezione sulle forme normali ha scelto, in ogni classe di formule equivalenti, rappresentanti di forma fissa. Ha definito i letterali, le clausole e le congiunzioni elementari, e ha dimostrato che la negazione di una forma normale è equivalente alla sua duale, che cambia ogni congiunzione in una disgiunzione e ogni letterale nel suo opposto. Ha costruito a partire dalla tavola le forme canoniche, uniche una volta fissate le variabili, e ha dimostrato l’esistenza delle due forme normali in due modi: con la tavola, come corollario della completezza funzionale, e per induzione sulla complessità, con l’unico caso della negazione congiunta, che equivale alla congiunzione delle negazioni delle sue componenti, e con un’ipotesi induttiva che richiede le due forme insieme, perché la negazione le scambia. Ha mostrato, infine, che la validità di una forma congiuntiva e la soddisfacibilità di una disgiuntiva si leggono a colpo d’occhio nelle loro coppie complementari.

L’algoritmo e i circuiti

La lezione sull’algoritmo delle forme normali e le sue applicazioni ha trasformato la seconda dimostrazione di esistenza in un procedimento che agisce su scritture: eliminare i connettivi diversi da $\neg$ , $\wedge$ e $\vee$ , far scendere le negazioni fino alle variabili e distribuire. Ha dimostrato la sua correttezza con la sostituzione in una scrittura, che adatta il teorema di sostituzione alle abbreviazioni, e la sua terminazione con tre misure che decrescono a ogni passo, l’ultima delle quali legge la congiunzione come un prodotto; ha dimostrato, inoltre, che la forma congiuntiva di $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ ha necessariamente $2^{n}$ clausole, sicché la crescita non è un difetto dell’algoritmo. Ha poi ottenuto le forme normali di una scatola nera a partire dalla sua tavola, le ha abbreviate fondendo righe vicine e le ha trasformate in circuiti di interruttori, la cui conduzione è il valore della loro formula.

La figura seguente riunisce i sei tratti in un’unica catena. Ogni nodo della colonna è una definizione o un risultato, numerato secondo l’ordine logico e collegato da un arco agli anelli precedenti che la sua dimostrazione usa; intorno fluttuano i sostegni, cioè i principi e gli strumenti a cui la catena ricorre di continuo, ciascuno collegato da una linea continua agli anelli che si appoggiano su di esso e da una tratteggiata all’anello in cui si stabilisce, tranne quelli che questa catena non dimostra (la leggibilità unica con la ricorsione, l’induzione e le abbreviazioni ufficiali, della prima unità), che sono disegnati come corone circolari. Un clic su un sostegno mette in evidenza tutti gli anelli che lo usano, e ogni anello rimanda alla lezione in cui si dimostra. Si noti che l’induzione e i valori dei connettivi sono i sostegni più frequentati dell’unità, e che il lemma del valore, benché si dimostri nella terza lezione, regge quasi tutto ciò che le ultime tre dicono su congiunzioni e disgiunzioni.

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'$ ; perciò una regola che calcola il valore di $\sigI\varphi\psi$ a partire da $\varphi$ , da $\psi$ e dai loro valori definisce un’unica funzione sulle formule. È stato dimostrato nella prima unità. Ammesso senza dimostrazione in questa unità.
BInduzione. Semplice e forte sui naturali, e sulla complessità delle formule, i cui unici casi sono le variabili e la negazione congiunta $(\varphi \downarrow \psi)$ . È stata dimostrata nella prima unità. Ammesso senza dimostrazione in questa unità.
CAbbreviazioni ufficiali. $\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)$ . Sono state fissate nella prima unità. Ammesso senza dimostrazione in questa unità.
DValori dei connettivi. Con $a = v(\varphi)$ e $b = v(\psi)$ : $v(\neg\varphi) = 1 - a$ , $v((\varphi \vee \psi)) = a + b - ab$ , $v((\varphi \wedge \psi)) = ab$ , $v((\varphi \rightarrow \psi)) = 1 - a(1 - b)$ , $v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b)$ e $v((\varphi \veebar \psi)) = a + b - 2ab$ , dove $a^{2} = a$ . Stabilito in: 1. Estensione di un’assegnazione.
ELemma di coincidenza. Se due assegnazioni coincidono sulle variabili di $\varphi$ , danno a $\varphi$ lo stesso valore; per questo la tavola con $2^{n}$ righe dice tutto. Stabilito in: 2. Lemma di coincidenza e tavole.
FSostituzione semantica. Se $\theta \eqsem \theta'$ e $\chi'$ risulta dal sostituire in $\chi$ un’occorrenza di $\theta$ con $\theta'$ , allora $\chi \eqsem \chi'$ . Stabilito in: 7. Teorema di sostituzione semantica.
GLeggi di equivalenza. Doppia negazione, idempotenza, commutatività, associatività, distributività, De Morgan, assorbimento, identità, dominanza, terzo escluso e non contraddizione, per formule qualsiasi. Stabilito in: 9. Leggi di equivalenza.
HLemma del valore. $v\left( \bigwedge_{i=1}^{n} \varphi_i \right) = 1$ se e solo se $v(\varphi_i) = 1$ per ogni $i$ ; $v\left( \bigvee_{i=1}^{n} \varphi_i \right) = 1$ se e solo se $v(\varphi_i) = 1$ per qualche $i$ . Stabilito in: 10. Lemma del valore e compatibilità.

Tratto 1 Il valore di una formula
- Calcolare il valore di una formula con la clausola della negazione congiunta e ricavare dalle abbreviazioni quello di ogni connettivo definito.
- Dimostrare il lemma di coincidenza e giustificare con esso che basta una tavola con $2^{n}$ righe.
- Classificare formule e insiemi senza confondere $\not\models \varphi$ con la contraddizione, e decidere la validità cercando un’assegnazione che falsifichi.
1. Estensione di un’assegnazione. Ogni assegnazione $v$ si estende in modo unico a tutte le formule con la clausola $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ ; sviluppando le abbreviazioni si calcola il valore di $\neg$ , $\vee$ , $\wedge$ , $\rightarrow$ , $\leftrightarrow$ e $\veebar$ .
  Si appoggia su: A (Leggibilità unica e ricorsione), C (Abbreviazioni ufficiali). Dimostrato in: Semantica della logica proposizionale.
2. Lemma di coincidenza e tavole. Se $v$ e $v'$ coincidono su $V(\varphi)$ , allora $v(\varphi) = v'(\varphi)$ , per induzione sulla complessità; perciò i valori di $\varphi$ in tutte le assegnazioni sono esattamente quelli delle $2^{n}$ righe della sua tavola.
  Usa: 1. Estensione di un’assegnazione. Si appoggia su: B (Induzione). Dimostrato in: Semantica della logica proposizionale.
3. Classificazione e decisione. Ogni formula è esattamente una di tre cose: valida, contingente o contraddizione; $\varphi$ è valida se e solo se $\neg\varphi$ è contraddizione, ed è contraddizione se e solo se $\models \neg\varphi$ . $\top$ e il terzo escluso sono validi, $\bot$ è contraddizione, e la validità e la soddisfacibilità si decidono percorrendo le righe.
  Si appoggia su: D (Valori dei connettivi), E (Lemma di coincidenza). Dimostrato in: Semantica della logica proposizionale.
Tratto 2 Conseguenza ed equivalenza
- Decidere conseguenze a partire da insiemi finiti o infiniti, esibendo un contromodello o dimostrando che non esiste.
- Applicare il teorema di deduzione semantico e la riduzione della conseguenza all’insoddisfacibilità.
- Distinguere la sostituzione di un’occorrenza dalla sostituzione uniforme, e dimostrare entrambe per induzione sulla complessità.
- Stabilire equivalenze mediante catene, nominando correttamente ogni legge.
1. La conseguenza e le sue proprietà. $\Gamma \models \varphi$ se ogni assegnazione che soddisfa $\Gamma$ soddisfa $\varphi$ ; $\emptyset \models \varphi$ se e solo se $\models \varphi$ ; valgono la riflessività, la monotonia, il taglio e la transitività, e un insieme insoddisfacibile ha come conseguenza qualsiasi formula.
  Usa: 3. Classificazione e decisione. Dimostrato in: Conseguenza ed equivalenza semantica.
2. Deduzione semantica e insoddisfacibilità. $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , per l’unica riga falsa dell’implicazione; $\{\varphi_1, \ldots, \varphi_n\} \models \psi \Leftrightarrow\; \models (\varphi_1 \rightarrow (\varphi_2 \rightarrow \cdots (\varphi_n \rightarrow \psi) \cdots))$ ; e $\Gamma \models \varphi$ se e solo se $\Gamma \cup \{\neg\varphi\}$ è insoddisfacibile.
  Usa: 4. La conseguenza e le sue proprietà. Si appoggia su: D (Valori dei connettivi). Dimostrato in: Conseguenza ed equivalenza semantica.
3. Equivalenza semantica. $\varphi \eqsem \psi$ se e solo se $\varphi \models \psi$ e $\psi \models \varphi$ , se e solo se $\models (\varphi \leftrightarrow \psi)$ ; l’equivalenza è riflessiva, simmetrica e transitiva, e due formule equivalenti sono intercambiabili come premesse e come conclusioni.
  Usa: 4. La conseguenza e le sue proprietà. Si appoggia su: D (Valori dei connettivi). Dimostrato in: Conseguenza ed equivalenza semantica.
4. Teorema di sostituzione semantica. Se $\theta \eqsem \theta'$ , sostituire in $\chi$ un’occorrenza di $\theta$ con $\theta'$ , compresa l’occorrenza totale, dà una formula equivalente a $\chi$ ; e lo stesso sostituire insieme tutte le occorrenze.
  Usa: 1. Estensione di un’assegnazione, 6. Equivalenza semantica. Si appoggia su: A (Leggibilità unica e ricorsione), B (Induzione). Dimostrato in: Conseguenza ed equivalenza semantica.
5. Sostituzione uniforme. Se $w(v_n) = v(\sigma(v_n))$ , allora $v(\sigma(\chi)) = w(\chi)$ ; perciò, se $\models \chi$ , anche $\models \sigma(\chi)$ , e la sostituzione uniforme conserva l’equivalenza e la conseguenza, ma non la soddisfacibilità né la contingenza.
  Usa: 1. Estensione di un’assegnazione, 4. La conseguenza e le sue proprietà, 6. Equivalenza semantica. Si appoggia su: A (Leggibilità unica e ricorsione), B (Induzione). Dimostrato in: Conseguenza ed equivalenza semantica.
6. Leggi di equivalenza. Le leggi del catalogo si verificano come identità tra polinomi con $a^{2} = a$ ; con la sostituzione e la transitività, si applicano a sottoformule e si concatenano.
  Usa: 3. Classificazione e decisione, 6. Equivalenza semantica. Si appoggia su: D (Valori dei connettivi), F (Sostituzione semantica). Dimostrato in: Conseguenza ed equivalenza semantica.
Tratto 3 Leggi per un numero qualsiasi di termini
- Sviluppare congiunzioni e disgiunzioni di $n$ termini come stringhe associate a sinistra e calcolarne il valore.
- Dimostrare per induzione sul numero di termini l’associatività generalizzata, l’indipendenza dall’ordine e le leggi di De Morgan generalizzate.
- Dimostrare la distributività generalizzata con un’induzione su due indici, e contare i termini che produce.
1. Lemma del valore e compatibilità. Se $\alpha \eqsem \alpha'$ e $\beta \eqsem \beta'$ , allora $\neg\alpha \eqsem \neg\alpha'$ , $(\alpha \wedge \beta) \eqsem (\alpha' \wedge \beta')$ e $(\alpha \vee \beta) \eqsem (\alpha' \vee \beta')$ ; una congiunzione di $n$ termini vale $1$ se e solo se tutti i suoi termini valgono $1$ , una disgiunzione se e solo se qualcuno vale $1$ , e termini equivalenti danno congiunzioni e disgiunzioni equivalenti.
  Usa: 6. Equivalenza semantica. Si appoggia su: D (Valori dei connettivi), B (Induzione). Dimostrato in: Leggi generalizzate di De Morgan e distributive.
2. Associatività e ordine. La congiunzione delle congiunzioni di due liste è equivalente a quella della loro concatenazione, e ogni raggruppamento è equivalente a quello associato a sinistra; due liste con gli stessi termini danno congiunzioni e disgiunzioni equivalenti, qualunque siano l’ordine e le ripetizioni.
  Si appoggia su: H (Lemma del valore), G (Leggi di equivalenza), B (Induzione). Dimostrato in: Leggi generalizzate di De Morgan e distributive.
3. Leggi di De Morgan generalizzate. $\neg \bigwedge_{i=1}^{n} \varphi_i \eqsem \bigvee_{i=1}^{n} \neg\varphi_i$ e $\neg \bigvee_{i=1}^{n} \varphi_i \eqsem \bigwedge_{i=1}^{n} \neg\varphi_i$ , applicando la legge binaria all’ultima unione e l’ipotesi induttiva a ciò che resta dentro.
  Si appoggia su: H (Lemma del valore), G (Leggi di equivalenza), B (Induzione). Dimostrato in: Leggi generalizzate di De Morgan e distributive.
4. Distributività generalizzata. $\left( \bigvee_{i=1}^{n} \varphi_i \right) \wedge \left( \bigvee_{j=1}^{m} \psi_j \right) \eqsem \bigvee_{i,j} (\varphi_i \wedge \psi_j)$ , con $nm$ termini in ordine lessicografico; e la sua duale, che distribuisce la disgiunzione di due congiunzioni, con De Morgan.
  Usa: 11. Associatività e ordine, 12. Leggi di De Morgan generalizzate. Si appoggia su: H (Lemma del valore), G (Leggi di equivalenza), B (Induzione). Dimostrato in: Leggi generalizzate di De Morgan e distributive.
Tratto 4 Funzioni di verità
- Contare le funzioni di verità e decidere l’equivalenza confrontando le funzioni che due formule rappresentano.
- Costruire la formula di una tavola e scrivere qualunque funzione con la sola negazione congiunta.
- Dimostrare che un insieme di connettivi è adeguato con il criterio della negazione congiunta, o che non lo è con una proprietà che le sue formule conservano.
1. Funzioni di verità. Ci sono $2^{2^{n}}$ funzioni di verità di $n$ argomenti; una formula con variabili tra $v_1, \ldots, v_n$ ne rappresenta esattamente una, $f_\varphi$ , e $\varphi \eqsem \psi \Leftrightarrow f_\varphi = f_\psi$ .
  Usa: 6. Equivalenza semantica. Si appoggia su: E (Lemma di coincidenza). Dimostrato in: Completezza funzionale.
2. Completezza funzionale. La congiunzione di una riga vale $1$ esattamente sulla sua riga; la disgiunzione delle congiunzioni delle righe in cui $f$ vale $1$ , o $(v_{1} \wedge \neg v_{1})$ se non ce n’è nessuna, rappresenta $f$ ; e ogni formula è equivalente alla formula della sua tavola.
  Usa: 14. Funzioni di verità. Si appoggia su: H (Lemma del valore), D (Valori dei connettivi). Dimostrato in: Completezza funzionale.
3. Insiemi adeguati e non adeguati. La negazione congiunta basta, perché le abbreviazioni si sviluppano; se le formule di $K$ esprimono il valore $(1 - a)(1 - b)$ , $K$ è adeguato, e quindi lo sono $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ e $\{\uparrow\}$ ; le formule di $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ valgono $1$ quando tutte le variabili valgono $1$ , e quell’insieme non è adeguato.
  Usa: 15. Completezza funzionale. Si appoggia su: C (Abbreviazioni ufficiali), B (Induzione), D (Valori dei connettivi). Dimostrato in: Completezza funzionale.
Tratto 5 Forme normali
- Riconoscere letterali, clausole e forme normali, distinguendo la forma della stringa dal suo significato.
- Costruire le forme canoniche a partire dalla tavola e dimostrarne l’unicità.
- Dimostrare per induzione l’esistenza delle forme normali, con l’ipotesi induttiva che richiede entrambe.
- Decidere a colpo d’occhio la validità di una forma congiuntiva e la soddisfacibilità di una disgiuntiva.
1. Letterali e dualità. $\neg\ell \eqsem \ell^{*}$ ; una congiunzione elementare è soddisfacibile se e solo se non contiene alcuna coppia complementare, e una clausola è valida se e solo se ne contiene una; la negazione di una forma normale è equivalente alla sua duale, sicché la forma congiuntiva di $\varphi$ è la duale della forma disgiuntiva di $\neg\varphi$ .
  Usa: 12. Leggi di De Morgan generalizzate. Si appoggia su: G (Leggi di equivalenza), F (Sostituzione semantica), H (Lemma del valore). Dimostrato in: Forme normali.
2. Forme canoniche. Se $\varphi$ è soddisfacibile, è equivalente alla sua forma canonica disgiuntiva, e se non è valida, a quella congiuntiva; fissate le variabili $v_1, \ldots, v_n$ , due forme canoniche sono equivalenti se e solo se sono la stessa stringa, e due formule soddisfacibili sono equivalenti se e solo se hanno la stessa forma canonica disgiuntiva.
  Usa: 15. Completezza funzionale, 17. Letterali e dualità. Si appoggia su: H (Lemma del valore), E (Lemma di coincidenza). Dimostrato in: Forme normali.
3. Esistenza per induzione. $(\varphi \downarrow \psi) \eqsem (\neg\varphi \wedge \neg\psi)$ ; le forme normali si conservano per congiunzione e per disgiunzione, la forma disgiuntiva di una congiunzione e la congiuntiva di una disgiunzione per distributività generalizzata; per induzione, con l’ipotesi induttiva per le due forme, ogni formula ha una forma disgiuntiva e una congiuntiva.
  Usa: 17. Letterali e dualità, 11. Associatività e ordine, 13. Distributività generalizzata. Si appoggia su: B (Induzione), F (Sostituzione semantica). Dimostrato in: Forme normali.
4. Ciò che si vede a colpo d’occhio. Una forma congiuntiva è valida se e solo se ogni clausola contiene una coppia complementare; una forma disgiuntiva è soddisfacibile se e solo se qualche congiunzione elementare non ne contiene alcuna.
  Usa: 17. Letterali e dualità. Si appoggia su: H (Lemma del valore). Dimostrato in: Forme normali.
Tratto 6 L’algoritmo e i circuiti
- Applicare l’algoritmo di riscrittura e scegliere l’eliminazione della doppia implicazione che conviene.
- Dimostrarne la correttezza e la terminazione, e spiegare perché la forma congiuntiva può crescere in modo esponenziale.
- Ottenere e semplificare le forme normali di una scatola nera, e progettare con esse circuiti di interruttori.
1. Correttezza e terminazione dell’algoritmo. Sostituire una sottoscrittura con un’altra equivalente dà una scrittura equivalente; ogni regola è un’equivalenza, e una scrittura irriducibile è una forma normale raggruppata in qualche modo; le misure $M_1$ , $M_2$ , con $M_2(\neg\varphi) = 2^{M_2(\varphi)}$ , e $M_3$ , con $M_3(\varphi \wedge \psi) = M_3(\varphi)\,M_3(\psi)$ , decrescono a ogni passo.
  Usa: 19. Esistenza per induzione, 11. Associatività e ordine. Si appoggia su: G (Leggi di equivalenza), D (Valori dei connettivi), B (Induzione). Dimostrato in: L’algoritmo delle forme normali e le sue applicazioni.
2. Crescita esponenziale. $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ è equivalente a una forma congiuntiva con $2^{n}$ clausole, e ogni forma congiuntiva equivalente ha almeno $2^{n}$ clausole non valide.
  Usa: 19. Esistenza per induzione, 17. Letterali e dualità. Si appoggia su: H (Lemma del valore). Dimostrato in: L’algoritmo delle forme normali e le sue applicazioni.
3. Righe vicine e circuiti. $(\kappa \wedge \ell) \vee (\kappa \wedge \ell^{*}) \eqsem \kappa$ e la sua duale; un circuito serie-parallelo conduce nello stato $v$ se e solo se $v(\varphi_C) = 1$ , e ogni funzione di verità è realizzata da qualche circuito.
  Usa: 15. Completezza funzionale, 18. Forme canoniche, 17. Letterali e dualità, 11. Associatività e ordine. Si appoggia su: G (Leggi di equivalenza), F (Sostituzione semantica), D (Valori dei connettivi), B (Induzione). Dimostrato in: L’algoritmo delle forme normali e le sue applicazioni.

Verso la metateoria. La catena si ferma dove la semantica raggiunge un procedimento per ogni domanda sulle formule. Resta da sapere se ciò che è vero in ogni assegnazione è esattamente ciò che si deduce nel sistema: la prossima unità confronterà le due nozioni.