Come funziona la sostituzione nelle formule proposizionali e quale importanza ha?

Nella logica proposizionale, uno degli strumenti più potenti per manipolare le formule è la sostituzione di variabili o sottoformule con altre formule. In generale, la sostituzione permette di esplorare la relazione tra diverse proposizioni e la loro equivalenza, una questione fondamentale per comprendere la logica formale in modo profondo.

La sostituzione di una formula proposizionale per una variabile è un passo preliminare utile, che prepara il terreno per affrontare le difficoltà che incontreremo quando ci occuperemo della sostituzione in logica del primo ordine nei capitoli successivi. Per semplificare la notazione, usiamo $A(B/p)$ per indicare la formula che si ottiene da A dopo aver sostituito ogni occorrenza della variabile $p$ con la formula $B$. Se sostituissimo k variabili contemporaneamente, la notazione diventa $A(B_1, \dots, B_k/p_{i_1}, \dots, p_k)$, in cui ogni occorrenza della variabile $p_i$ in A viene sostituita con $B_i$.

Un altro esempio interessante riguarda la sostituzione di una variabile con se stessa. Se prendiamo la formula $A(p_1/p_1)$, otteniamo semplicemente A. Più complesso è il caso in cui si sostituiscono più variabili contemporaneamente, come nel caso in cui A è $(p_2 \land p_3)$ e $D$ è $(p_1 \land p_4)$, quindi $A(C,D/p_1, p_2)$ risulta come $((p_2 \land p_3) \to ((p_1 \land p_4) \to (p_2 \land p_3)))$. In questo caso, le due occorrenze di $p_1$ sono sostituite con $C$, e la variabile $p_2$ viene sostituita con $D$, ma le variabili in $C$ e $D$ rimangono invarianti, poiché la sostituzione avviene in parallelo.

La definizione formale della sostituzione, che fornisce una regola ricorsiva per trattare variabili, connettivi e negazioni, è fondamentale per qualsiasi approfondimento della logica proposizionale. Ogni volta che una formula è sostituita da un’altra, o da un'istanza di una formula, è necessario verificare che la sostituzione non alteri il valore di verità della formula, il che è il cuore della proprietà che permette alle tautologie di rimanere tali anche dopo la sostituzione.

Un teorema cruciale in questo contesto è che, se $B$ e $C$ hanno lo stesso valore di verità, allora anche le formule $A(B/p)$ e $A(C/p)$ avranno lo stesso valore di verità. Questo fatto, che può sembrare intuitivo, è in realtà il fondamento su cui si basano le dimostrazioni più complesse in logica proposizionale, come quelle che trattano l’equivalenza tautologica delle formule.

Un'ulteriore generalizzazione riguarda la sostituzione in sequenza: se due formule $A$ e $B$ sono veri in tutte le assegnazioni di verità, sostituendo una formula $A(C/p_1)$ in una formula $B(C/p_2)$, si ottiene una nuova formula che rimane vera sotto tutte le assegnazioni. Ciò implica che le tautologie sono preservate dalla sostituzione e che ogni istanza di una tautologia è a sua volta una tautologia.

Sebbene questi concetti possano sembrare astratti e formali, sono cruciali per costruire una comprensione robusta della logica formale, specialmente quando si tratta di applicare la logica proposizionale a teoremi più complessi che richiedono sostituzioni o manipolazioni di variabili. L’importanza della sostituzione non può essere sottolineata abbastanza: è la chiave per comprendere il funzionamento interno di molte teorie logiche, sia in contesti matematici che informatici.

Come Funzionano le Variabili Libere e Legate nella Logica del Primo Ordine?

Le variabili legate sono quelle che sono soggette all'azione di un quantificatore, come ∀ (per ogni) o ∃ (esiste). Ad esempio, nella formula ∀x (x > 0), la variabile x è legata dal quantificatore ∀. All'interno di una formula, un'istanza di una variabile legata non può essere modificata o interpretata separatamente, poiché il suo valore è determinato dal quantificatore. La nozione di legame tra variabili e quantificatori è fondamentale per evitare ambiguità nel trattamento delle variabili in formule più complesse.

Le variabili libere, d'altra parte, non sono collegate a nessun quantificatore. Esse sono variabili il cui valore non è determinato dalla struttura formale della formula, e pertanto possono assumere valori arbitrari all'interno del dominio di discussione. Ad esempio, nella formula x > 0, x è una variabile libera, poiché non è legata da alcun quantificatore. È importante sottolineare che una formula può contenere sia variabili libere che legate, e il significato complessivo della formula dipenderà dal contesto in cui vengono utilizzate.

Per comprendere meglio come le variabili libere e legate interagiscono in una formula, consideriamo l'esempio della formula x1 ≠ S(0) ∧ ∀x2 (∃x3 (x2 ⋅ x3 = x1) → x2 = S(0) ∨ x2 = x1). Qui, x1 è una variabile libera, poiché non è legata da alcun quantificatore e rappresenta un valore specifico all'interno dell'espressione. D'altra parte, x2 e x3 sono variabili legate, poiché sono vincolate dai quantificatori ∀ e ∃, rispettivamente. Sebbene la stessa struttura di formula venga ripetuta nelle varianti, l'interpretazione cambia a causa delle diverse variabili libere, come nel caso della formula x4 ≠ S(0) ∧ ∀x5 (∃x6 (x5 ⋅ x6 = x4) → x5 = S(0) ∨ x5 = x4).

La comprensione della differenza tra variabili libere e legate è essenziale anche per evitare errori di interpretazione nelle espressioni logiche. Ad esempio, una formula che contiene una variabile libera può essere interpretata come un'affermazione che dipende dal valore di quella variabile, mentre una formula con solo variabili legate afferma qualcosa di universale o esistenziale, indipendentemente dai valori specifici delle variabili.

Un'altra considerazione importante è che una formula senza variabili libere viene chiamata sentenza o formula chiusa. Una sentenza è una formula che non dipende da alcun parametro esterno e può essere verificata in modo indipendente, rispetto al dominio di discussione. Per esempio, la formula ∀x (0 ≤ x) è una sentenza, poiché afferma che ogni valore di x è maggiore o uguale a zero, indipendentemente da quale sia il valore specifico di x nel dominio.

A questo punto, è importante notare che la corretta distinzione tra variabili libere e legate ha implicazioni significative nella sintassi e nella semantica della logica del primo ordine. La variabile legata perde il suo significato di "individuo specifico" e diventa un elemento che può essere manipolato dalla logica formale senza riferirsi a un valore concreto. Al contrario, le variabili libere continuano a rappresentare entità specifiche, e la loro presenza in una formula può cambiare il tipo di affermazione che la formula esprime.

Oltre a ciò, è fondamentale comprendere come la lettura di una formula possa essere influenzata dalla presenza di variabili libere. In formule più complesse, la sostituzione di variabili o la rinominazione di variabili legate possono alterare profondamente il significato di una formula. L'uso di variabili libere in più di un contesto all'interno della stessa formula può portare a confusioni, come mostrato nell'esempio in cui la variabile x1 è usata sia come variabile legata che libera. In tali casi, è consigliabile evitare ambiguità per garantire una lettura chiara e corretta della formula.

Un altro aspetto importante riguarda la unique readability, un principio che assicura che ogni termine logico possa essere scritto in una forma unica. Ad esempio, ogni termine può essere scritto come una costante, una variabile, o una funzione composta, e la sua struttura deve essere univocamente interpretabile. Questo principio aiuta a mantenere la coerenza e la chiarezza nelle espressioni logiche, evitando fraintendimenti o errori nei passaggi di deduzione.

Le convenzioni stilistiche sono ugualmente significative nella scrittura e lettura di formule logiche. Ad esempio, l'uso delle parentesi può essere impiegato per migliorare la leggibilità, ma deve essere fatto con attenzione. Sebbene alcune convenzioni alternative possano essere comuni in altri testi, l'importante è mantenere una struttura chiara e consistente, che consenta una facile interpretazione della formula da parte del lettore.

Infine, mentre l'introduzione di variabili libere e legate aggiunge una profondità importante alla logica del primo ordine, è essenziale che il lettore acquisisca la consapevolezza di come questi concetti si applicano al contesto più ampio della teoria dei modelli e della semantica logica. Una corretta gestione delle variabili consente di formulare teorie e dimostrazioni precise, oltre a evitare errori concettuali che potrebbero compromettere l'integrità logica delle affermazioni.

La seconda Teoria dell'Incompletezza e la sua applicazione al Teorema di Löb

La Seconda Teoria dell'Incompletezza di Gödel rivela una limitazione fondamentale nei sistemi formali che sono sufficientemente potenti da esprimere l'aritmetica di base, come il sistema T. Questa teoria stabilisce che, se T è un sistema coerente e adeguatamente axiomato, non può provare la propria coerenza, cioè non può dimostrare la verità di ConT, dove ConT rappresenta la coerenza di T. L'importanza di questa conclusione risiede nel fatto che, pur essendo una proposizione vera, la sua verità non è dimostrabile all'interno del sistema T stesso.

Il ragionamento che porta a questa conclusione si sviluppa attraverso una serie di passaggi logici che collegano la dimostrazione della non-provabilità di D alla conclusione finale, ovvero che T non può dimostrare la sua propria coerenza. Si dimostra, in particolare, che la formula ¬D implica ThmT (⌜¬D⌝), e successivamente, tramite il Lemma VII.75(b), si giunge alla conclusione che ¬D implica ¬ConT. Questa serie di passaggi dimostra inequivocabilmente che, per un sistema come T che è coerente, la sua coerenza non può essere provata all'interno di sé.

Inoltre, è interessante notare che esistono altre dichiarazioni indipendenti da PA che non coinvolgono concetti metamatematici espliciti. Queste affermazioni, come il teorema di Paris-Harrington, il teorema dell’idra, e il teorema di Goodstein, sono esempi di affermazioni aritmetiche che non possono essere provate in sistemi formali simili a PA, ma che non fanno uso di metamatematica. L’esistenza di questi teoremi espande la comprensione delle limitazioni insite nei sistemi formali, suggerendo che l'incompletezza non riguarda solo la coerenza di un sistema, ma anche la sua capacità di affrontare affermazioni matematiche in apparenza innocenti ma intrinsecamente non provabili.

Un altro aspetto importante riguarda la domanda se ConT sia sempre indipendente da T. La risposta è negativa. Se T è una teoria coerente e sufficiente, come ogni estensione assiomatica di R, si può definire una nuova teoria T′ che è coerente, ma contiene l'asserzione ¬ConT. In questo caso, T′ è coerente e assiomatizzabile, e quindi la sua indipendenza da ConT può essere messa in discussione solo se vengono applicate condizioni particolari, come la ω-coerenza.

La ω-coerenza è una condizione che garantisce che T non possa derivare contraddizioni tramite la manipolazione di sequenze infinite di numeri naturali. In pratica, la ω-coerenza stabilisce che se una proposizione è falsa per ogni numero naturale, non è possibile che un sistema coerente come T la provi come vera, e viceversa. Quando una teoria è ω-consistente, ciò implica che la sua coerenza non possa essere dimostrata all’interno della stessa teoria, ma è comunque indipendente dalla proposizione di coerenza di T.

Tuttavia, per comprendere pienamente il Teorema di Löb, è necessario prestare attenzione alle implicazioni metamatematiche, poiché l'ipotesi di Löb è legata a un aspetto più profondo della struttura logica di T. Se una teoria può provare che la provabilità di A implica A, allora, data la coerenza della teoria, essa fornirà inevitabilmente una prova diretta della verità di A. Ciò implica che l'autosufficienza della teoria permette a quest'ultima di concludere la verità della proposizione senza dipendere da prove esterne.

Il Teorema di Löb, quindi, non solo rappresenta una manifestazione del limite dell'incompletezza nei sistemi formali, ma anche una delle chiavi per capire come le teorie possono gestire e "riflettere" sulla loro propria struttura di provabilità. La sua applicazione alle teorie coerenti evidenzia come la logica possa essere auto-riflessiva, ma anche come questa riflessività si scontri con i limiti imposti dalla Seconda Teoria dell'Incompletezza.