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 C_i Δでるた segue da una lista di asserzioni D_i Γがんま (o equivalentemente che Γがんま comporta Δでるた) e si scrive

$\Gamma \vdash \Delta$

quando

$(C_{1}ass.\ e\ C_{2}ass.\ e\ \dots \ e\ C_{n}ass.)\ comporta\ (D_{1}ass.\ o\ \dots \ o\ D_{m}ass.)$

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 $\Gamma ,\perp \vdash \Delta$ (da falso segue qualsiasi cosa)
• T ovvero la proposizione sempre vera $\vdash \top$
• Identità: è sempre vero il sequente $A\vdash A$ per qualsiasi proposizione A.

Si formalizzano inoltre le equazioni definitorie dei quattro connettivi e dei due quantificatori come segue:

• ∧-equazione: $\Gamma \vdash A\land B\iff \Gamma \vdash A\land \Gamma \vdash B$
• ∨-equazione: $A\lor B\vdash \Delta \iff A\vdash \Delta \land B\vdash \Delta$
• →-equazione: $\Gamma \vdash A\rightarrow B\iff \Gamma ,A\vdash B$
• ¬-equazione: $\vdash \neg A\iff A\vdash \perp$
• ∀-equazione: $\Gamma \vdash (\forall x\in D)A(x)\iff \Gamma ,z\in D\vdash A(z)$
• ∃-equazione: $\Gamma ,(\exists x\in D)A(x)\vdash \Delta \iff per\ un\ generico\ z\in D\ si\ ha\ \Gamma ,z\in D,A(z)\vdash \Delta$

Dove D è il dominio della variabile x e A(x) è un predicato

Calcolo proposizionale in LJ

Tenendo presente che regola di identità $A\vdash A$ è vera sempre, si risolvono le equazioni definitorie ottenendo le seguenti regole inferenziali di derivazione per i sequenti.

• ∧-formazione ${\frac {\Gamma \vdash A\ \ \ \Gamma \vdash B}{\Gamma \vdash A\land B}}$

• ∧-riflessione ${\frac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }},{\frac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}$

• ∨-formazione ${\frac {\Gamma ,A\vdash \Delta \ \ \ \Gamma ,B\vdash \Delta }{\Gamma ,A\lor B\vdash \Delta }}$

• ∨-riflessione ${\frac {\Gamma \vdash A}{\Gamma \vdash A\lor B}},{\frac {\Gamma \vdash B}{\Gamma \vdash A\lor B}}$

• →-formazione ${\frac {\Gamma ,A\vdash B}{\Gamma \vdash A\rightarrow B}}$

• →-riflessione ${\frac {\Gamma \vdash A\ \ \ \Gamma ',B\vdash \Delta }{\Gamma ,\Gamma ',A\rightarrow B\vdash \Delta }}$

• ¬-formazione ${\frac {\Gamma ,A\vdash \perp }{\Gamma \vdash \neg A}}$

• ¬-riflessione ${\frac {\Gamma \vdash A}{\Gamma ,\neg A\vdash \Delta }}$

Appare chiaro che le regole sul ¬ derivano direttamente da quelle su →: infatti le scritture $\neg A$ e $A\rightarrow \perp$ si equivalgono.

Regole strutturali in LJ

In LJ valgono le due seguenti regole:

• Indebolimento ${\frac {\Gamma \vdash \Delta }{\Gamma ,\Sigma \vdash \Delta }}$

• Contrazione ${\frac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}$

Quantificatori

Le regole di derivazione dei quantificatori in LJ sono:

• ∀-formazione ${\frac {\Gamma ,z\in D\vdash A(z)}{\Gamma \vdash (\forall x\in D)A(x)}}$ o equivalentemente ${\frac {\Gamma \vdash A(z)}{\Gamma \vdash \forall xA(x)}}$

con $z$ 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 ${\frac {\Gamma \vdash z\in D\ \ \ \Gamma ',A(x)\vdash \Delta }{\Gamma ,(\forall x\in D)A(x),\Gamma '\vdash \Delta }}$ o equivalentemente ${\frac {\Gamma ,A(z)\vdash \Delta }{\Gamma ,\forall xA(x)\vdash \Delta }}$

• ∃-formazione ${\frac {\Gamma ,z\in D,A(z)\vdash \Delta }{\Gamma ,(\exists x\in D)A(x)\vdash \Delta }}$ o equivalentemente ${\frac {\Gamma ,A(z)\vdash \Delta }{\Gamma ,\exists xA(x)\vdash \Delta }}$

con $z$ non libera in D.

• ∃-riflessione ${\frac {\Gamma \vdash z\in D\ \ \ \Gamma '\vdash A(z)}{\Gamma ,\Gamma '\vdash (\exists x\in D)A(x)}}$ o equivalentemente ${\frac {\Gamma \vdash A(z)}{\Gamma \vdash \exists xA(x)}}$

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 $\neg \neg A\vdash A$: 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.

Voci correlate

• Logica intuizionista
• Logica classica
• Gerhard Gentzen
• Teorema di eliminazione del taglio