Sequente

Da Wikipedia, l'enciclopedia libera.

Un sequente è un'entità della logica che permette di esprimere legami tra asserzioni complesse facendo uso dei legami metalinguistici e e 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.\ e\ \dots\ e\ 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.

[modifica] 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'appliccazione 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.

[modifica] 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 \and B \iff \Gamma \vdash A \and \Gamma \vdash B$
∨-equazione: $A \or B \vdash \Delta \iff A \vdash \Delta \and B \vdash \Delta$
→-equazione: $\Gamma \vdash A \rarr 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

[modifica] 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 \and B}$

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

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

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

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

→-riflessione $\frac{\Gamma \vdash A\ \ \ \Gamma ', B \vdash \Delta}{\Gamma, \Gamma ', A \rarr 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 \rarr \perp$ si equivalgono.

[modifica] 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}$

[modifica] 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 x A(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 x A(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 x A(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 x A(x)}$

[modifica] 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.