Sequente

Da Wikipedia, l'enciclopedia libera.
Se riscontri problemi nella visualizzazione dei caratteri, clicca qui.

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 Ci Δ segue da una lista di asserzioni Di Γ (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[modifica | modifica sorgente]

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

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

Calcolo proposizionale in LJ[modifica | modifica sorgente]

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 B}{\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.

Regole strutturali in LJ[modifica | modifica sorgente]

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

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)}

Calcolo dei sequenti in LK[modifica | modifica sorgente]

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.

Voci correlate[modifica | modifica sorgente]