Vai al contenuto
Topos Uranos

Riepilogo

Le due unità precedenti hanno costruito sullo stesso linguaggio due nozioni di ciò che segue da premesse date: la deduzione, Γ⊢φ\Gamma \vdash \varphi, che ottiene stringhe da altre stringhe con assiomi e regole senza chiedersi che cosa significhino, e la conseguenza semantica, Γ⊨φ\Gamma \models \varphi, che percorre assegnazioni senza scrivere alcuna deduzione. Questa lezione dimostra che entrambe le nozioni coincidono per insiemi finiti di premesse. La correttezza (Γ⊢φ⇒Γ⊨φ\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi) si dimostra per induzione forte sul numero di righe della deduzione, con un caso per ogni assioma e per ogni regola, compresa la sostituzione della doppia negazione; ne seguono la coerenza del sistema e un metodo per dimostrare che una formula non è deducibile. Il converso, la completezza, richiede uno strumento nuovo: il lemma di Kalmár, che trasforma ogni riga della tavola di verità di una formula in una deduzione e la cui induzione sulla complessità ha un solo caso composto, perché la negazione congiunta è l’unico connettivo primitivo; per quel caso si deducono nel sistema due lemmi sulla negazione congiunta. Eliminando poi con la dimostrazione per casi, una a una, le ipotesi che fissano la riga, si ottiene che ogni tautologia è un teorema e, con i due teoremi di deduzione, che ogni conseguenza di un insieme finito di premesse è deducibile da esso. Ne seguono la decidibilità della deducibilità da un numero finito di premesse e la coincidenza tra l’equivalenza dimostrabile e quella semantica. Il caso di infinite premesse resta per la lezione successiva, perché richiede il teorema di compattezza.

Obiettivi di apprendimento

  1. Enunciare la correttezza e la completezza nelle forme debole, finita e forte, distinguerle come proprietà indipendenti e spiegare perché è circolare l’argomento che ottiene la completezza «per la correttezza».
  2. Dimostrare la correttezza per induzione forte sul numero di righe, compreso il caso della regola di sostituzione della doppia negazione, e usarla per dimostrare la coerenza del sistema e la non deducibilità di formule concrete.
  3. Dedurre nel sistema del corso i due lemmi sulla negazione congiunta e, con essi, dimostrare il lemma di Kalmár per induzione sulla complessità.
  4. Dimostrare la completezza debole eliminando ipotesi con la dimostrazione per casi, e la completezza per insiemi finiti di premesse con i due teoremi di deduzione.
  5. Applicare la coincidenza tra deduzione e conseguenza per decidere deducibilità, equivalenze dimostrabili e coerenza, e per analizzare che cosa accade quando si aggiungono regole al sistema.

Due domande sul sistema del corso

L’unità sulla deduzione ha fissato il sistema del corso: gli schemi di assioma A1, A2 e A3 di Łukasiewicz e due regole, il modus ponens (MP) e la sostituzione della doppia negazione (SDN), che la lezione sulle quattro tecniche di deduzione ha aggiunto dopo aver dimostrato la doppia negazione. Una deduzione da un insieme Γ\Gamma è una successione finita di formule in cui ciascuna è un assioma, un elemento di Γ\Gamma, il risultato del modus ponens applicato a due formule precedenti o il risultato della SDN applicata a una precedente; Γ⊢φ\Gamma \vdash \varphi significa che esiste una deduzione da Γ\Gamma la cui ultima formula è φ\varphi. L’unità sulla semantica, a sua volta, ha definito nella lezione su conseguenza ed equivalenza semantica la relazione Γ⊨φ\Gamma \models \varphi: ogni assegnazione che soddisfa tutte le formule di Γ\Gamma soddisfa φ\varphi. Entrambe le relazioni si scrivono con lo stesso schema, un insieme a sinistra e una formula a destra; ma la loro natura è opposta. La prima è sintattica ed esistenziale: afferma che esiste un oggetto finito, una deduzione, che si può controllare segno per segno. La seconda è semantica e universale: afferma qualcosa su tutte le assegnazioni, che sono infinite e ciascuna delle quali dà valore a infinite variabili.

Sul sistema si pongono quindi due domande. La prima: deduce soltanto ciò che deve? Il sistema si dice corretto se, per ogni insieme Γ\Gamma e ogni formula φ\varphi, da Γ⊢φ\Gamma \vdash \varphi segue Γ⊨φ\Gamma \models \varphi: ciò che si deduce da premesse date è vero sotto ogni assegnazione che rende vere le premesse. La seconda: deduce tutto ciò che deve? Il sistema si dice completo se da Γ⊨φ\Gamma \models \varphi segue Γ⊢φ\Gamma \vdash \varphi. La completezza ammette tre gradi, secondo gli insiemi di premesse che comprende:

  • completezza debole: se ⊨φ\models \varphi, allora ⊢φ\vdash \varphi; ogni tautologia è un teorema;
  • completezza per insiemi finiti di premesse: se {γ1,…,γk}⊨φ\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi, allora {γ1,…,γk}⊢φ\{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi;
  • completezza forte: se Γ⊨φ\Gamma \models \varphi, allora Γ⊢φ\Gamma \vdash \varphi, per un insieme Γ\Gamma qualsiasi, anche infinito.

Questa lezione dimostra la correttezza e i primi due gradi della completezza. Il terzo si dimostra nella lezione sul teorema di compattezza, e la ragione di questa ripartizione si spiega alla fine della lezione.

Che cosa non dire

In spagnolo la correttezza si chiama talvolta «solvencia», un calco dell’inglese soundness; il termine spagnolo è «corrección», ed è quello che il corso usa in spagnolo. Né va definita come la proprietà del sistema di «inferire un’espressione da un insieme di espressioni», perché questa è la deducibilità stessa e non una proprietà del sistema. Gli errori di contenuto, però, sono altri due.

Il primo consiste nell’affermare che correttezza e completezza «si inferiscono l’una dall’altra». Sono proprietà indipendenti: il sistema di Łukasiewicz senza la regola SDN è corretto (lo mostra la dimostrazione di questa lezione, togliendo un caso) e non è completo (la lezione sui sistemi deduttivi formali ha esibito una tautologia che non deduce); e un sistema che ammettesse tutte le formule come assiomi sarebbe completo senza essere corretto. Il problema risolto 2 studia entrambi gli esempi.

Il secondo errore è più grave, perché presenta un argomento circolare come dimostrazione della completezza. Dice, in sostanza: se φ⊬ψ\varphi \nvdash \psi, allora per il teorema di deduzione ⊬(φ→ψ)\nvdash (\varphi \rightarrow \psi); «per la correttezza» ⊭(φ→ψ)\not\models (\varphi \rightarrow \psi); e per il teorema di deduzione semantico φ⊭ψ\varphi \not\models \psi. Ora, la correttezza afferma che ciò che è deducibile è valido, e la sua contrapposizione che ciò che non è valido non è deducibile:

⊢χ  ⇒  ⊨χ,⊭χ  ⇒  ⊬χ\vdash \chi \;\Rightarrow\; \models \chi, \qquad \not\models \chi \;\Rightarrow\; \nvdash \chi

Il passo dell’argomento va nella direzione opposta, da ⊬χ\nvdash \chi a ⊭χ\not\models \chi, e questa è la contrapposizione di ⊨χ⇒⊢χ\models \chi \Rightarrow \vdash \chi, cioè della completezza debole. Se è così, l’argomento presuppone ciò che vuole dimostrare. Ne segue che la completezza non «si inferisce in modo semplice»: è il risultato più profondo del corso, e la sua dimostrazione occupa la maggior parte di questa lezione. Infine, è impreciso riassumere la completezza dicendo che «tutte le espressioni vere hanno una dimostrazione»; ha una dimostrazione ciò che è valido, vero sotto ogni assegnazione, non ciò che è vero sotto qualcuna: la variabile v1v_{1} è vera sotto molte assegnazioni e non è un teorema.