Calcolo dei sequenti e presentazione logica proposizionale

[thedarkhero]

Come viene introdotta la logica proposizionale mediante il calcolo dei sequenti?

Solitamente si presenta il calcolo dei sequenti introducendone gli assiomi, le regole logiche e le regole strutturali.
Poi si dice che l'insieme dei sequenti dimostrabili in logica proposizionale classica è il più piccolo insieme contenente gli assiomi e chiuso per applicazione delle regole.

Ma come si definisce la logica proposizionale? Ad esempio si potrebbe dire che la logica proposizionale è l'insieme delle formule $A$ tali che il sequente $\vdash A$ è dimostrabile?

[megas_archon]

Non è chiaro cosa vuoi sapere: il calcolo dei sequenti è una maniera di dimostrare degli asserti della logica proposizionale, e l'insieme delle formule tali che \(\vdash A\) è dimostrabile cambia radicalmente a seconda delle regole del calcolo, ovviamente. Per esempio, c'è un calcolo dei sequenti per la logica implicazionale, e ce n'è uno per logiche piu potenti, ma il calcolo non "introduce" la logica, che gli è antecedente...

[thedarkhero]

Provo a spiegarmi meglio. La mia domanda è: come si definisce la logica proposizionale classica (o intuizionista, o qualsiasi altra logica proposizionale)?

Mi verrebbe da dire che la logica proposizionale classica (ad esempio) è caratterizzata da un insieme di assiomi e di regole, quindi la presenterei elencandone gli assiomi e le regole del calcolo dei sequenti proposizionale classico (oppure potrei utilizzare la deduzione naturale, o il calcolo alla Hilbert, o altro ancora...), e direi poi che l'insieme dei sequenti dimostrabili in logica proposizionale classica è il più piccolo insieme contenente gli assiomi e chiuso per applicazione delle regole.

Poi però quando arrivo a dover dare la definizione di logica proposizionale classica come la definisco? O meglio come la si definisce solitamente?

Si dice che la logica proposizionale classica è l'insieme di tutte le formule $A$ tali che il sequente $\vdash A$ è dimostrabile?

[megas_archon]

Ho capito cosa vuoi sapere, ma la risposta non ha niente a che fare con il calcolo dei sequenti: il calcolo dei sequenti è alla fin fine un tipo specifico di sistema di riscrittura, in cui le regole o gli schemi di regole di derivazione sono enunciati volta per volta indicando come trasformare i sequenti esistenti per derivarne di nuovi.

Le regole possono essere definite in modo sintattico, via pattern matching per la sostituzione delle formule, oppure in modo semantico, specificando le condizioni di validità per l'applicazione delle singole regole. Ad esempio l'eliminazione della congiunzione è una regola del primo tipo, mentre l'introduzione dell'esistenziale è del secondo tipo.

Ora, questo sistema di riscrittura non riesce a definire il linguaggio di cui è un calcolo, perché è definito in termini di esso: sarebbe come chiedere, come si definisce l'integrale di Riemann date le tre regole {integrazione per sostituzione, per parti, per fratti semplici}? La risposta è che non si può, non ha senso farlo: le teorie dell'integrazione sfruttano regole simili tra loro, alcune ne hanno di specifiche (per esempio, quelle che ti permettono di calcolare l'integrale di una funzione Lebesgue-integrabile, ma non Riemann-integrabile), ma le regole sono completamente disaccoppiate dalla teoria che le "genera".

Venendo, ora, alla tua domanda, il mio consiglio è di fare tabula rasa e approfondire la questione su qualche testo: alcuni, di ottimi, che ho leggiucchiato, che seguo per insegnare e che consiglio come approfondimenti sono

1. https://link.springer.com/book/10.1007/ ... -13-7997-0
2. https://www.amazon.com/Lectures-Logic-S ... 0521168465 (vedi in particolare la sezione I.3 e gli esercizi alle pagine 193 e 194)
3. https://www.cambridge.org/core/books/lo ... 0798C62AA1

[thedarkhero]

Innanzitutto grazie per i consigli riguardo i testi.

Nel frattempo ho provato a vedere come presenta i linguaggi proposizionali Wikipedia (qui), si dice che un linguaggio proposizionale è un sistema formale $L(A, \Omega, Z, I)$, dove $A$ è l'insieme delle variabili proposizionali, $\Omega$ è l'insieme dei connettivi logici, $Z$ è l'insieme delle regole di inferenza e $I$ è l'insieme degli assiomi.

Per spiegare chi è il linguaggio (supponendo che $\Omega=\{\wedge, \vee, \rightarrow, \neg\}$) è sufficiente dire che tutte le variabili proposizionali appartengono al linguaggio, che se $A$ e $B$ appartengono al linguaggio allora anche $(A \wedge B), (A \vee B), (A \rightarrow B), \neg A$ e $\neg B$ appartengono al linguaggio e che nient'altro appartiene al linguaggio.

Ma per dire chi sono gli insiemi $Z$ e $I$ non si utilizza ad esempio il calcolo dei sequenti? O alternativamente la deduzione naturale o altri calcoli analoghi?

[megas_archon]

Ma per dire chi sono gli insiemi $Z$ e $I$ non si utilizza ad esempio il calcolo dei sequenti?

Ma certo che no! E' esattamente il contrario, è grazie a $Z$ che definisci cos'è il calcolo dei sequenti: in effetti $Z$ "è" il calcolo dei sequenti.

[thedarkhero]

Ok, ma allora come faccio a descrivere gli insiemi $Z$ e $I$?

Io avrei detto che per quanto riguarda $I$ gli assiomi sono dati dai sequenti nella forma $\Gamma,A \vdash A$.
Per quanto riguarda le regole ho per esempio la regola che dice che se $\Gamma \vdash A$ e $\Gamma \vdash B$ allora $\Gamma \vdash A \wedge B$, poi ho la regola che dice che se $\Gamma,A,B \vdash C$ allora $\Gamma, A \wedge B \vdash C$, e così via...

[megas_archon]

Niente di quel che dici è giusto.

Ok, ma allora come faccio a descrivere gli insiemi $Z$ e $I$?

Non so cosa tu voglia "descrivere". $Z$ è semplicemente un sistema di riscrittura astratto, ossia una relazione binaria su \(\Omega\) con certe proprietà. Per quanto riguarda $I$, cioè l'insieme degli assiomi, non è affatto ovvio quali siano quando ti viene presentata la logica che inducono [né è ovvio che logica induca un determinato set di assiomi], né il modo in cui cambiare gli uni cambia l'altra. D'altra parte, persino l'operazione di cambiare \(\Omega\) si può comportare in modi strani: sai cos'è il segno di Sheffer?

[thedarkhero]

Si, conosco il segno di Sheffer.

Tu però mi stai parlando di una generica logica proposizionale, ovvero di un sistema formale astratto $L(A,\Omega,Z,I)$.

Io ti sto chiedendo:
Come si definisce la logica proposizionale classica?
Come si definisce la logica proposizionale intuizionista?

Immagino che la logica proposizionale classica sia una particolare logica proposizionale, con i suoi connettivi, i suoi assiomi e le sue regole. Lo stesso per la logica proposizionale intuizionista. O mi sbaglio?