Sequente
Un sequente è un'entità della logica che permette di esprimere legami tra asserzioni complesse facendo uso dei legami metalinguistici e che comporta. Le prime formalizzazioni di sequenti e di calcolo dei sequenti sono dovute al lavoro del logico Gerhard Gentzen, in particolare alle sue scoperte dei primi anni Trenta.
Si dice che lista di asserzioni Ci Δ segue da una lista di asserzioni Di Γ (o equivalentemente che Γ comporta Δ) e si scrive
quando
Nella visione della logica classica (LK) Δ è una lista di m asserzioni (o proposizioni), mentre in logica intuizionista (LJ) in Δ trova posto una sola proposizione. Questo è un fatto di notevole importanza perché condiziona tutta la struttura di regole inferenziali sui due sistemi.
Calcolo dei sequenti in LJ
Tutto quel che riguarda le regole di derivazione in LJ si riconduce alle cosiddette equazioni definitorie dei connettivi, che si costruiscono per deduzione naturale. Il calcolo dei sequenti consiste nell'applicare, partendo da un sequente formato da asserzioni complesse, le regole del sistema per giungere a sequenti riconosciuti validi. Se l'applicazione delle regole di derivazione porta sempre a scritture ambigue o non vere (ad esempio da una proposizione B segue che A non viene di certo considerato un sequente valido) allora si può concludere che quel sequente non è derivabile, o, meglio, che la frase che esprime non è dimostrabile.
Equazioni definitorie
Vengono definiti:
- ⊥ ovvero la proposizione falsa in qualsiasi interpretazione, allora vale che (da falso segue qualsiasi cosa)
- T ovvero la proposizione sempre vera
- Identità: è sempre vero il sequente per qualsiasi proposizione A.
Si formalizzano inoltre le equazioni definitorie dei quattro connettivi e dei due quantificatori come segue:
- ∧-equazione:
- ∨-equazione:
- →-equazione:
- ¬-equazione:
- ∀-equazione:
- ∃-equazione:
Dove D è il dominio della variabile x e A(x) è un predicato
Calcolo proposizionale in LJ
Tenendo presente che regola di identità è vera sempre, si risolvono le equazioni definitorie ottenendo le seguenti regole inferenziali di derivazione per i sequenti.
- ∧-formazione
- ∧-riflessione
- ∨-formazione
- ∨-riflessione
- →-formazione
- →-riflessione
- ¬-formazione
- ¬-riflessione
Appare chiaro che le regole sul ¬ derivano direttamente da quelle su →: infatti le scritture e si equivalgono.
Regole strutturali in LJ
In LJ valgono le due seguenti regole:
- Indebolimento
- Contrazione
Quantificatori
Le regole di derivazione dei quantificatori in LJ sono:
- ∀-formazione o equivalentemente
con non libera in D. Ciò significa che z non deve già comparire in qualche proposizione del sequente altrimenti si avrebbe un sistema inconsistente: asserire che, dato A per una certa variabile, valga A per tutti gli elementi del dominio è assolutamente folle.
- ∀-riflessione o equivalentemente
- ∃-formazione o equivalentemente
con non libera in D.
- ∃-riflessione o equivalentemente
Calcolo dei sequenti in LK
Il calcolo dei sequenti in logica classica si differenzia dal calcolo dei sequenti in logica intuizionista per il fatto che i contesti (le liste di proposizioni) sono presenti anche a destra. Ciò vale per tutte le regole, incluse quelle strutturali di indebolimento e contrazione.
Per questo motivo in logica classica sono considerati veri il principio del terzo escluso e il sequente : avendo a disposizione regole con i contesti a destra è possibile fornirne agilmente una dimostrazione, contrariamente a quanto accade nel sistema LJ, per il quale non sono vere.
Le regole di calcolo applicabili nella logica proposizionale mediante l'uso dei sequenti, sono: regola di assunzione, modus ponendo ponens, modus tollendo tollens, doppia negazione, introduzione della congiunzione, eliminazione della congiunzione, introduzione della disgiunzione, eliminazione della disgiunzione, prova condizionale e reductio ad absurdum. Il formalismo dei sequenti permette di definire quale sottoinsieme delle assunzioni dalle quali dipendono le premesse costituisce anche il sottoinsieme delle assunzioni dalle quali dipende la conclusione da esse derivata. Nel caso degli ultimi tre operatori logici (eliminazione della disgiunzione, prova condizionale e reductio ad absurdum), l'insieme delle assunzioni da cui dipende la conclusione non coincide con l'unione (o somma) degli insiemi delle assunzioni delle rispettive premesse.[1]
Note
- ^ prof. Giuseppe Spolaore, Linguaggi e calcoli formali - Le regole del calcolo proposizionale (PDF), Università di Verona, pp. 13-20. URL consultato il 18 novembre 2020 (archiviato il 18 novembre 2020).
Voci correlate
![](http://upload.wikimedia.org/wikipedia/commons/thumb/a/af/Crystal128-kmplot.svg/25px-Crystal128-kmplot.svg.png)