Metateoria: sintesi e sfide

Riepilogo

Questa lezione chiude l’unità dedicata alla metateoria e, con essa, il contenuto del corso. Ricostruisce la catena deduttiva che va dalla validità degli assiomi alla correttezza del sistema; dai due lemmi della negazione congiunta al lemma di Kalmár e alla completezza per insiemi finiti; dal lemma dei due testimoni al teorema di compattezza e, attraverso di esso, alla completezza forte; e dalla forma a clausole alla correttezza e alla completezza refutazionale del metodo di risoluzione, indicando a ogni anello quali risultati usa e in quale lezione si dimostra. Mostra come le tre parti precedenti del corso, linguaggio, deduzione e semantica, convergano nella coincidenza di $\vdash$ e $\models$ , e che cosa ciascuna vi apporti; distingue ciò che il corso ha dimostrato da ciò che ha supposto e da ciò che lascia aperto. 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à, individuando i risultati precedenti su cui ciascuno si appoggia e la lezione in cui si dimostra, e giustificare l’ordine della compattezza e della completezza forte.
Spiegare come linguaggio, deduzione e semantica convergano nella coincidenza di $\vdash$ e $\models$ , e quale risultato di ciascuna unità del corso vi sia indispensabile.
Distinguere ciò che il corso ha dimostrato da ciò che ha supposto (gli schemi di assiomi, le regole primitive e l’induzione) e da ciò che lascia aperto (il costo di decidere la soddisfacibilità e la logica con quantificatori).
Risolvere problemi che combinano marcature, lemma di Kalmár, sostituzione uniforme, compattezza e risoluzione, usando in ciascun caso il lato facile della coincidenza.

Che cosa ha ottenuto l’unità

L’unità si era proposta di confrontare le due relazioni che le unità precedenti avevano costruito sullo stesso linguaggio, la deducibilità $\Gamma \vdash \varphi$ e la conseguenza semantica $\Gamma \models \varphi$ , e di dimostrare che coincidono. Lo scopo è stato raggiunto senza riserve negli enunciati: le due relazioni sono la stessa per ogni insieme di premesse, finito o infinito, e la risoluzione offre una terza via, ugualmente corretta e completa, per decidere la conseguenza. Le riserve stanno nei metodi, e ciascuna è stata dichiarata al suo posto: la completezza della prima lezione è costruttiva ma non pratica, perché produce deduzioni lunghe quanto la tavola; la compattezza assicura che un’assegnazione esiste, ma non insegna a trovarla; e la risoluzione decide, ma il suo costo nel caso peggiore è una questione aperta. Con queste riserve, il cammino percorso si legge come un’unica catena deduttiva in quattro tratti.

Correttezza

La lezione su correttezza e completezza cominciò col fissare il vocabolario: il sistema è corretto se $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ , e completo se vale l’inverso, in tre gradi (debole, per insiemi finiti e forte). Smontò un argomento circolare che pretende di ottenere la completezza «per la correttezza» passando da $\nvdash \chi$ a $\not\models \chi$ , un passo che è la contronominale della completezza debole, e mostrò che le due proprietà sono indipendenti. Dimostrò poi che ogni istanza di A1, A2 e A3 è valida, supponendo un’assegnazione che la refutasse e arrivando, attraverso la riga falsa dell’implicazione, a valori impossibili; e, per induzione forte sul numero di righe, la correttezza, con un caso per gli assiomi, un altro per le premesse, il modus ponens semantico e, per la regola di sostituzione della doppia negazione, l’equivalenza $\theta \eqsem \neg\neg\theta$ con il teorema di sostituzione semantica. La proprietà che si trasmette di riga in riga non è la validità, ma la soddisfazione da parte di un’assegnazione fissata che soddisfa le premesse, ed è per questo che la correttezza vale con premesse, anche infinite. Ne seguirono la coerenza di ogni insieme soddisfacibile, in particolare quella del sistema, e il metodo che mancava all’unità sulla deduzione: un contromodello dimostra che una deduzione non esiste.

Kalmár e la completezza finita

La stessa lezione dimostrò l’inverso in due passi. Il primo è il lemma di Kalmár: se le variabili di $\varphi$ sono tra $u_{1}, \ldots, u_{n}$ , allora $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ per ogni assegnazione $v$ , dove $\psi^{v}$ è $\psi$ se $v(\psi) = 1$ e $\neg\psi$ altrimenti; il sistema deduce da ogni riga ciò che la riga dice della formula. La sua induzione sulla complessità ha un unico caso composto, $(\alpha \downarrow \beta)$ , perché la negazione congiunta è l’unico connettivo primitivo, e al suo interno tre sottocasi, che chiedono due lemmi del sistema, il secondo in due forme: $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ , dedotto con l’introduzione della congiunzione, la doppia negazione e due applicazioni della regola SDN, e $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ e $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , dedotti con l’introduzione della disgiunzione. Il secondo passo elimina le premesse: se $\varphi$ è una tautologia, si deduce dalle premesse di ciascuna delle $2^{n}$ righe, e la dimostrazione per casi elimina il letterale dell’ultima variabile, poi quello della penultima, fino ad arrivare a $\vdash \varphi$ , la completezza debole. Con il teorema di deduzione semantico e l’inverso di quello sintattico, la completezza si estese agli insiemi finiti di premesse; da cui, con premesse finite, deduzione e conseguenza coincidono, l’equivalenza dimostrabile coincide con quella semantica e la deducibilità è decidibile, perché la tavola ne risponde.

Compattezza e completezza forte

La lezione su il teorema di compattezza affrontò il caso infinito, che il lemma di Kalmár non raggiunge, perché infinite premesse non si scaricano in un’implicazione. Dimostrò, senza menzionare alcuna deduzione, che un insieme è soddisfacibile se e solo se lo è ciascuno dei suoi sottoinsiemi finiti. Una successione di valori per $v_{1}, \ldots, v_{n}$ è buona se ogni sottoinsieme finito dell’insieme è soddisfatto da qualche assegnazione che la prolunga; il lemma dei due testimoni assicura che una successione buona si prolunga in una buona, perché, se nessuno dei due prolungamenti fosse buono, l’unione dei due testimoni finiti contraddirebbe che la successione è buona; e l’assegnazione che risulta dal preferire sempre il valore $1$ quando è possibile soddisfa ogni formula, per il lemma di coincidenza, perché ogni formula ha un numero finito di variabili. La costruzione non ha bisogno dell’assioma della scelta, perché le variabili sono numerate e ogni passo ha una regola. Dalla compattezza seguirono le sue forme equivalenti, la forma dell’insoddisfacibilità e la forma della conseguenza; da quest’ultima, dalla completezza per insiemi finiti e dalla monotonia, la completezza forte; e da questa e dalla correttezza, la coincidenza piena: $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ per ogni $\Gamma$ , e un insieme è coerente se e solo se è soddisfacibile. La lezione avvertì che quest’ordine non è una questione di preferenza: ottenere la compattezza da una completezza forte non ancora disponibile sarebbe circolare. Terminò con la colorazione dei grafi numerabili, che traduce un problema infinito in un insieme di formule le cui parti finite sono soddisfacibili, e con i limiti di ciò che un insieme di formule può esprimere.

Risoluzione

La lezione su il metodo di risoluzione sostituì gli insiemi di formule con insiemi di clausole, ciascuna un insieme finito di letterali, con due rappresentazioni: la forma a clausole, che ha gli stessi modelli, e la forma definizionale, che introduce una variabile nuova per ogni sottoscrittura composta, conserva soltanto la soddisfacibilità e cresce come la formula, non come una potenza di due. Un’unica regola agisce sulle clausole: da $C$ e $D$ , con $\ell \in C$ e $\ell^{*} \in D$ , si inferisce $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ , e una refutazione è una derivazione che arriva a $\Box$ . La correttezza si dimostrò come quella del sistema, per induzione sulla derivazione e con il risolvente come conseguenza delle sue premesse; la completezza refutazionale, per induzione sul numero di variabili, con l’eliminazione di una variabile, che conserva la soddisfacibilità e la cui dimostrazione costruisce un modello; e per insiemi infiniti, di nuovo con la compattezza. Ne seguì che $\Gamma \models \varphi$ se e solo se una forma a clausole di $\Gamma \cup \{\neg\varphi\}$ ha una refutazione, e che la saturazione, finita perché con $n$ variabili non ci sono più di $4^{n}$ clausole, decide la soddisfacibilità senza tavole. La lezione presentò il problema della soddisfacibilità, il cui costo nel caso peggiore nessuno conosce, e due casi che si decidono rapidamente, le clausole di Horn e quelle di due letterali.

La figura seguente riunisce i quattro tratti in un’unica catena. Ogni nodo della colonna è un risultato, numerato secondo l’ordine logico e unito 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 una volta dopo l’altra, ciascuno unito con una linea continua agli anelli che si appoggiano su di esso e con una tratteggiata all’anello in cui si stabilisce, tranne quelli che vengono dalle unità precedenti, che si disegnano come corone circolari. Fare clic su un sostegno evidenzia tutti gli anelli che lo usano, e ogni anello rimanda alla lezione in cui si dimostra. Si osservi che la correttezza e la compattezza, stabilite l’una nel primo tratto e l’altra nel terzo, ricompaiono nei tratti seguenti, e che il sostegno più visitato dell’unità è quello delle assegnazioni e coincidenza, seguito dall’induzione, nelle sue tre forme: sulle righe di una deduzione, sulla complessità di una formula e sul numero di variabili di un insieme di clausole.

Sostegni della catena

AInduzione e ricorsione. Induzione forte sui naturali, induzione sulla complessità delle formule, con l’unico caso composto $(\alpha \downarrow \beta)$ , e definizione per ricorsione. Si dimostrarono nella prima unità. Ammesso senza dimostrazione in questa unità.
BSistema del corso. A1, A2 e A3, il modus ponens e la regola SDN; riflessività, monotonia, modus ponens tra deduzioni, finitezza e $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ . Si stabilirono nella seconda unità. Ammesso senza dimostrazione in questa unità.
CTecniche derivate. Doppia negazione, dalla lezione sulle quattro tecniche; introduzione della congiunzione e della disgiunzione e dimostrazione per casi (se $\Gamma \cup \{\psi\} \vdash \chi$ e $\Gamma \cup \{\neg\psi\} \vdash \chi$ , allora $\Gamma \vdash \chi$ ), dalla lezione sulle tecniche della logica classica. Si dimostrarono nella seconda unità. Ammesso senza dimostrazione in questa unità.
DAssegnazioni e coincidenza. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ; se due assegnazioni coincidono su $V(\varphi)$ , danno a $\varphi$ lo stesso valore; la validità si decide con $2^{n}$ righe. Si dimostrarono nella terza unità. Ammesso senza dimostrazione in questa unità.
EConseguenza semantica. Riga falsa dell’implicazione, monotonia, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , $\Gamma \models \varphi$ se e solo se $\Gamma \cup \{\neg\varphi\}$ è insoddisfacibile, e il teorema di sostituzione semantica. Si dimostrarono nella terza unità. Ammesso senza dimostrazione in questa unità.
FForme congiuntive. Lemma del valore; ogni formula equivale a una forma normale congiuntiva, che può richiedere $2^{n}$ clausole; una disgiunzione di letterali è valida se e solo se contiene una coppia complementare. Si dimostrarono nella terza unità. Ammesso senza dimostrazione in questa unità.
GCorrettezza. Se $\Gamma \vdash \varphi$ , allora $\Gamma \models \varphi$ , per ogni insieme $\Gamma$ ; un contromodello dimostra che una deduzione non esiste. Stabilito in: 2. Correttezza.
HCompattezza. Un insieme di formule è soddisfacibile se e solo se ogni suo sottoinsieme finito è soddisfacibile; da cui ciò che è insoddisfacibile lo è già in una parte finita. Stabilito in: 11. Teorema di compattezza.

Tratto 1 Correttezza
- Verificare che ogni istanza degli schemi è valida senza costruirne la tavola.
- Dimostrare la correttezza per induzione forte sul numero di righe, con il caso della regola di sostituzione della doppia negazione.
- Dimostrare con un contromodello che una formula non si deduce, e ottenere la coerenza dalla correttezza.
1. Validità degli assiomi. Ogni istanza di A1, A2 e A3 è valida: un’assegnazione che la refutasse richiederebbe, attraverso la riga falsa dell’implicazione, valori impossibili.
  Si appoggia su: E (Conseguenza semantica). Dimostrato in: Correttezza e completezza.
2. Correttezza. Se $\Gamma \vdash \varphi$ , allora $\Gamma \models \varphi$ , per ogni $\Gamma$ : per induzione forte sul numero di righe, con un caso per gli assiomi, un altro per le premesse, il modus ponens semantico e, per la regola SDN, $\theta \eqsem \neg\neg\theta$ con la sostituzione semantica.
  Usa: 1. Validità degli assiomi. Si appoggia su: A (Induzione e ricorsione), B (Sistema del corso), E (Conseguenza semantica). Dimostrato in: Correttezza e completezza.
3. Coerenza e contromodelli. Ogni insieme soddisfacibile è coerente; il sistema è coerente e $\nvdash v_{1}$ ; se un’assegnazione soddisfa $\Gamma$ e refuta $\varphi$ , allora $\Gamma \nvdash \varphi$ , e la tavola certifica che ciò che non è valido non è un teorema.
  Si appoggia su: G (Correttezza), D (Assegnazioni e coincidenza). Dimostrato in: Correttezza e completezza.
Tratto 2 Kalmár e la completezza finita
- Dedurre nel sistema i due lemmi della negazione congiunta, con la regola di sostituzione della doppia negazione dove serve.
- Dimostrare il lemma di Kalmár per induzione sulla complessità, con un unico caso composto.
- Eliminare con la dimostrazione per casi le premesse delle righe, e scaricare premesse finite con i due teoremi di deduzione.
- Decidere con la tavola la deducibilità, l’equivalenza dimostrabile e la coerenza a partire da premesse finite.
1. Introduzione della negazione congiunta. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ e $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ : la congiunzione delle negazioni è $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ; la doppia negazione toglie quella esterna, e la regola SDN le due interne.
  Si appoggia su: B (Sistema del corso), C (Tecniche derivate). Dimostrato in: Correttezza e completezza.
2. Negazione della negazione congiunta. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ e $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , perché $\neg(\alpha \downarrow \beta)$ è $(\alpha \vee \beta)$ e basta l’introduzione della disgiunzione.
  Si appoggia su: B (Sistema del corso), C (Tecniche derivate). Dimostrato in: Correttezza e completezza.
3. Lemma di Kalmár. Se $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ , allora $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ per ogni assegnazione $v$ ; il passo induttivo ha un unico caso, $(\alpha \downarrow \beta)$ , con tre sottocasi secondo i valori di $\alpha$ e di $\beta$ .
  Usa: 4. Introduzione della negazione congiunta, 5. Negazione della negazione congiunta. Si appoggia su: A (Induzione e ricorsione), D (Assegnazioni e coincidenza), B (Sistema del corso). Dimostrato in: Correttezza e completezza.
4. Completezza debole. Se $\models \varphi$ , allora $\vdash \varphi$ : il lemma di Kalmár deduce $\varphi$ da ogni riga, e la dimostrazione per casi elimina i letterali dall’ultima variabile alla prima, con $2^{n}$ usi del lemma e $2^{n} - 1$ della dimostrazione per casi.
  Usa: 6. Lemma di Kalmár. Si appoggia su: C (Tecniche derivate). Dimostrato in: Correttezza e completezza.
5. Completezza per insiemi finiti. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ : il teorema di deduzione semantico porta a una tautologia, la completezza debole la deduce e l’inverso del teorema di deduzione restituisce le premesse.
  Usa: 7. Completezza debole. Si appoggia su: E (Conseguenza semantica), B (Sistema del corso). Dimostrato in: Correttezza e completezza.
6. Coincidenza finita e decisione. Per $\Gamma$ finito, $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ , e $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ; da cui la deducibilità a partire da premesse finite è decidibile, con la tavola.
  Usa: 8. Completezza per insiemi finiti. Si appoggia su: G (Correttezza), D (Assegnazioni e coincidenza). Dimostrato in: Correttezza e completezza.
Tratto 3 Compattezza e completezza forte
- Dimostrare la compattezza fissando uno a uno i valori delle variabili, con l’invariante delle successioni buone e l’argomento dei due testimoni.
- Passare tra la forma della soddisfacibilità, quella dell’insoddisfacibilità e quella della conseguenza.
- Ottenere la completezza forte dalla compattezza, senza circolarità, e da essa la coincidenza della coerenza con la soddisfacibilità.
- Codificare in insiemi di formule problemi su oggetti infiniti e risolverli con la compattezza.
1. Lemma dei due testimoni. Se la successione $s$ di valori fissati è buona (ogni sottoinsieme finito dell’insieme è soddisfatto da un’assegnazione che la prolunga), lo è anche $(s, 1)$ oppure $(s, 0)$ : se nessuna lo fosse, l’unione dei due testimoni finiti contraddirebbe che $s$ è buona.
  Si appoggia su: D (Assegnazioni e coincidenza). Dimostrato in: Il teorema di compattezza.
2. Teorema di compattezza. $\Gamma$ è soddisfacibile se e solo se lo è ogni sottoinsieme finito: si fissa $v_{n + 1}$ a $1$ se $(s_{n}, 1)$ è buona e a $0$ altrimenti, e l’assegnazione risultante soddisfa ogni formula per il lemma di coincidenza. Non serve l’assioma della scelta, perché le variabili sono numerate.
  Usa: 10. Lemma dei due testimoni. Si appoggia su: A (Induzione e ricorsione), D (Assegnazioni e coincidenza). Dimostrato in: Il teorema di compattezza.
3. Forme equivalenti. $\Gamma$ è insoddisfacibile se e solo se lo è qualche parte finita; $\Gamma \models \varphi$ se e solo se $\Gamma_{0} \models \varphi$ per qualche $\Gamma_{0} \subseteq \Gamma$ finito; e quest’ultima forma implica a sua volta il teorema.
  Usa: 11. Teorema di compattezza. Si appoggia su: E (Conseguenza semantica). Dimostrato in: Il teorema di compattezza.
4. Completezza forte. Se $\Gamma \models \varphi$ , allora $\Gamma \vdash \varphi$ , per ogni $\Gamma$ : la forma della conseguenza dà un $\Gamma_{0}$ finito, la completezza per insiemi finiti dà $\Gamma_{0} \vdash \varphi$ , e la monotonia $\Gamma \vdash \varphi$ .
  Usa: 8. Completezza per insiemi finiti, 12. Forme equivalenti. Si appoggia su: B (Sistema del corso). Dimostrato in: Il teorema di compattezza.
5. La deduzione è la conseguenza. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ per ogni $\Gamma$ ; i teoremi sono esattamente le tautologie, e un insieme è coerente se e solo se è soddisfacibile.
  Usa: 13. Completezza forte. Si appoggia su: G (Correttezza). Dimostrato in: Il teorema di compattezza.
6. Colorazione di grafi numerabili. Con una variabile $x_{i,c}$ per ogni vertice e colore, e formule che dicono che ogni vertice ha un colore e uno solo e che i vicini differiscono, un grafo numerabile ammette una colorazione con $k$ colori se ogni sottografo finito la ammette.
  Si appoggia su: H (Compattezza), F (Forme congiuntive). Dimostrato in: Il teorema di compattezza.
Tratto 4 Risoluzione
- Rappresentare un insieme di formule come insieme di clausole, tramite la forma congiuntiva o tramite quella definizionale.
- Costruire refutazioni senza eliminare due coppie complementari in un solo passo.
- Dimostrare la correttezza e la completezza refutazionale della risoluzione, per insiemi finiti e, con la compattezza, per insiemi qualsiasi.
- Decidere conseguenze per saturazione e riconoscere i casi che si decidono rapidamente.
1. Forma a clausole. Una clausola è un insieme finito di letterali, soddisfatta se qualche letterale assume il valore $1$ , e $\Box$ è insoddisfacibile; una forma a clausole di $\Gamma$ ha gli stessi modelli, e $\Gamma \models \varphi$ se e solo se una forma a clausole di $\Gamma \cup \{\neg\varphi\}$ è insoddisfacibile.
  Si appoggia su: F (Forme congiuntive), E (Conseguenza semantica). Dimostrato in: Il metodo di risoluzione.
2. Forma a clausole definizionale. Con una variabile nuova per sottoscrittura e le sue clausole di definizione, $T(\varphi)$ è equisoddisfacibile con $\varphi$ e ha al più $4k + 1$ clausole di al più tre letterali; le forme definizionali decidono la conseguenza a partire da premesse finite.
  Usa: 16. Forma a clausole. Si appoggia su: A (Induzione e ricorsione), D (Assegnazioni e coincidenza). Dimostrato in: Il metodo di risoluzione.
3. Correttezza della risoluzione. $\{C, D\} \models R_{\ell}(C, D)$ , per casi sul valore di $\ell$ ; per induzione forte sulla derivazione, $S \models C$ per ogni clausola $C$ derivata da $S$ , e se $S$ ha una refutazione, è insoddisfacibile.
  Usa: 16. Forma a clausole. Si appoggia su: A (Induzione e ricorsione). Dimostrato in: Il metodo di risoluzione.
4. Eliminazione di una variabile. $E_{p}(S)$ , che conserva le clausole senza $p$ né $\neg p$ e aggiunge i risolventi su $p$ , non contiene $p$ ed è equisoddisfacibile con $S$ ; da un suo modello si ottiene un modello di $S$ scegliendo il valore di $p$ .
  Usa: 18. Correttezza della risoluzione. Si appoggia su: D (Assegnazioni e coincidenza). Dimostrato in: Il metodo di risoluzione.
5. Completezza refutazionale finita. Ogni insieme finito insoddisfacibile di clausole ha una refutazione, per induzione sul numero di variabili: si elimina l’ultima e si inseriscono le premesse di ogni risolvente.
  Usa: 19. Eliminazione di una variabile. Si appoggia su: A (Induzione e ricorsione). Dimostrato in: Il metodo di risoluzione.
6. Completezza refutazionale. Un insieme di clausole, finito o infinito, è insoddisfacibile se e solo se ha una refutazione; da cui $\Gamma \models \varphi$ se e solo se una forma a clausole di $\Gamma \cup \{\neg\varphi\}$ ha una refutazione.
  Usa: 16. Forma a clausole, 18. Correttezza della risoluzione, 20. Completezza refutazionale finita. Si appoggia su: H (Compattezza). Dimostrato in: Il metodo di risoluzione.
7. La saturazione decide. Con $n$ variabili, l’insieme delle clausole derivate ha al più $4^{n}$ elementi; la saturazione termina e decide la soddisfacibilità senza tavole, anche se non sempre più rapidamente di esse.
  Usa: 18. Correttezza della risoluzione, 20. Completezza refutazionale finita. Dimostrato in: Il metodo di risoluzione.

La fine del corso. La catena termina dove le due facce del corso si riconoscono come un’unica relazione e si dispone di un metodo per deciderla. Ciò che resta aperto non è più una domanda sulla logica proposizionale, ma sul suo costo e sulla sua estensione ai quantificatori.