• Istituto
    • Chi Siamo
    • La nostra storia
  • Magazine
    • Agenda
    • Atlante
    • Il Faro
    • Il Chiasmo
    • Diritto
    • Il Tascabile
    • Le Parole Valgono
    • Lingua italiana
    • WebTv
  • Catalogo
    • Le Opere
    • Bottega Treccani
    • Gli Ebook
    • Le Nostre Sedi
  • Scuola e Formazione
    • Portale Treccani Scuola
    • Formazione Digitale
    • Formazione Master
    • Scuola del Tascabile
  • Libri
    • Vai al portale
  • Arte
    • Vai al portale
  • Treccani Cultura
    • Chi Siamo
    • Come Aderire
    • Progetti
    • Iniziative Cultura
    • Eventi Sala Igea
  • ACQUISTA SU EMPORIUM
    • Arte
    • Cartoleria
    • Design & Alto Artigianato
    • Editoria
    • Idee
    • Marchi e Selezioni
  • Accedi
    • Modifica Profilo
    • Treccani X

sequenti, calcolo dei

Enciclopedia della Matematica (2013)
  • Condividi

sequenti, calcolo dei


sequenti, calcolo dei calcolo logico introdotto da G. Gentzen negli anni Trenta del xx secolo i cui elementi sono i sequenti, vale a dire espressioni del tipo Γ ⊢ Δ in cui Γ e Δ sono sequenze finite di formule ben formate di un linguaggio logico (→ enunciati, linguaggio degli; → predicati, linguaggio dei) e il simbolo Γ ⊢ Δ corrisponde alla seguente implicazione: «se tutte le formule di Γ (premesse) sono vere allora almeno una delle formule di Δ (conseguenze) è vera». Così definito, il sequente A1, ..., An ⊢ B1, ..., Bn equivale all’enunciato A1 ∧ ... ∧ An ⇒ B1 ∨ ... ∨ Bn. Il sequente rappresenta una relazione di deducibilità fra le premesse e le conclusioni; l’espressione Γ ⊢ Δ equivale quindi all’esistenza di una deduzione che porti dalle premesse Γ alle conseguenze Δ. Come negli altri calcoli logici, anche in questo caso sono presenti assiomi e regole di derivazione che consentono lo sviluppo del calcolo fornendo delle regole per la costruzione di una deduzione. In questo caso l’unico assioma è l’assioma identità che assicura la validità del sequente A ⊢ A, dove A è una qualsiasi formula ben formata e le regole di derivazione si dividono in regole logiche, regole strutturali e regola del taglio.

Regole logiche

Le regole logiche sono utilizzate per introdurre, a destra o a sinistra del simbolo di sequente, i → connettivi e i → quantificatori. Per esempio, la regola di introduzione del connettivo ∨ (disgiunzione) a destra del simbolo di sequente può essere rappresentata nel modo seguente:

formula

La linea orizzontale indica che il sequente Γ ⊢ A ∨ B, Δ è stato dedotto dal sequente Γ ⊢ A, Δ. Di seguito sono riportate le regole logiche del calcolo dei sequenti, dove Π indica anch’esso una sequenza finita di formule.

• Congiunzione

introduzione della congiunzione a destra

formula

introduzione della congiunzione a sinistra 1

formula

introduzione della congiunzione a sinistra 2

formula

• Disgiunzione

introduzione della disgiunzione a destra 1

formula

introduzione della disgiunzione a destra 2

formula

introduzione della disgiunzione a sinistra

formula

• Negazione

introduzione della negazione a destra

formula

introduzione della negazione a sinistra

formula

• Implicazione

introduzione dell’implicazione a destra

formula

introduzione dell’implicazione a sinistra

formula

• Quantificatore universale

introduzione del quantificatore universale a destra

formula

(in questa regola la variabile x non è una variabile libera nelle formule di Δ e Γ)

introduzione del quantificatore universale a sinistra

formula

(in questa regola t rappresenta un qualsiasi termine del linguaggio e A[x] rappresenta la sostituzione della variabile x al posto del termine t)

• Quantificatore esistenziale

introduzione del quantificatore esistenziale a destra

formula

(in questa regola t rappresenta un qualsiasi termine del linguaggio e A[x] rappresenta la sostituzione della variabile x al posto del termine t)

introduzione del quantificatore esistenziale a sinistra

formula

(in questa regola la variabile x non è una variabile libera nelle formule di Δ e Γ).

Regole strutturali

Le regole strutturali sono la regola di indebolimento, che permette di aggiungere formule a sinistra o a destra del simbolo di sequente, indebolendo in tal modo le premesse o le conseguenze, la regola di scambio, che permette di permutare l’ordine delle formule che compaiono nelle premesse o nelle conseguenze, e la regola di contrazione, che permette di passare da due occorrenze della stessa formula nelle premesse o nelle conseguenze a una occorrenza sola di tale formula.

• Indebolimento

indebolimento a destra

formula

indebolimento a sinistra

formula

• Scambio

scambio a destra

formula

scambio a sinistra

formula

• Contrazione

contrazione a destra

formula

contrazione a sinistra

formula

Per esemplificare l’applicazione di alcune di queste regole si riporta la deduzione del sequente ⊢ (corrispondente a una tautologia nel calcolo degli enunciati) a partire dall’assioma A ⊢ A:

formula

Particolare importanza riveste nel calcolo dei sequenti la regola del taglio che permette di eliminare, nel corso di una deduzione, una formula che appare sia nelle conseguenze di un sequente sia nelle premesse di un altro sequente.

• Regola del taglio

formula

La regola del taglio è l’unica regola che consente l’eliminazione di una formula da un sequente: nel sequente risultante non c’è infatti più traccia della formula A. Da ciò discende che una deduzione di un sequente Γ ⊢ Δ in cui venga fatto uso della regola del taglio è una dimostrazione “non meccanicistica” in quanto non è possibile stabilire in modo automatico i passaggi necessari per dedurre il sequente Γ ⊢ Δ a partire dall’assioma identità. Tuttavia, grazie al teorema di eliminazione del taglio (→ taglio, regola del) è possibile associare a ogni deduzione di un sequente Γ ⊢ Δ una deduzione dello stesso sequente in cui non si faccia uso della regola di taglio. Questa possibilità rende le deduzioni del calcolo dei sequenti paragonabili a procedure algoritmiche e stabilisce un legame fra la teoria della dimostrazione e l’informatica teorica. Tale legame è sancito dall’isomorfismo di → Curry-Howard.

Il calcolo dei sequenti è stato applicato non soltanto alla logica classica, ma anche ad altri tipi di logica quali la → logica intuizionista, la → logica minimale e la → logica lineare, effettuando opportune modifiche sulla struttura dei sequenti ed eliminando alcune regole strutturali.

Tag
  • TEORIA DELLA DIMOSTRAZIONE
  • QUANTIFICATORE UNIVERSALE
  • LOGICA INTUIZIONISTA
  • INFORMATICA TEORICA
  • LOGICA CLASSICA
Vocabolario
sequènte
sequente sequènte s. m. [dall’ingl. sequent, nel sign. di «conseguente»]. – In logica matematica, coppia di insiemi di formule, dette rispettivam. premesse e conclusioni; il sequente è valido se dalla congiunzione delle premesse si deduce...
càlcolo¹
calcolo1 càlcolo1 s. m. [dal lat. calcŭlus, propr. «pietruzza» (cfr. càlcolo2), attrav. il sign. di «gettone per fare i conti»]. – 1. a. Successione più o meno lunga di operazioni atte a fornire la soluzione di un dato problema aritmetico,...
  • Istituto
    • Chi Siamo
    • La nostra storia
  • Magazine
    • Agenda
    • Atlante
    • Il Faro
    • Il Chiasmo
    • Diritto
    • Il Tascabile
    • Le Parole Valgono
    • Lingua italiana
    • WebTv
  • Catalogo
    • Le Opere
    • Bottega Treccani
    • Gli Ebook
    • Le Nostre Sedi
  • Scuola e Formazione
    • Portale Treccani Scuola
    • Formazione Digitale
    • Formazione Master
    • Scuola del Tascabile
  • Libri
    • Vai al portale
  • Arte
    • Vai al portale
  • Treccani Cultura
    • Chi Siamo
    • Come Aderire
    • Progetti
    • Iniziative Cultura
    • Eventi Sala Igea
  • ACQUISTA SU EMPORIUM
    • Arte
    • Cartoleria
    • Design & Alto Artigianato
    • Editoria
    • Idee
    • Marchi e Selezioni
  • Accedi
    • Modifica Profilo
    • Treccani X
  • Ricerca
    • Enciclopedia
    • Vocabolario
    • Sinonimi
    • Biografico
    • Indice Alfabetico

Istituto della Enciclopedia Italiana fondata da Giovanni Treccani S.p.A. © Tutti i diritti riservati

Partita Iva 00892411000

  • facebook
  • twitter
  • youtube
  • instagram
  • Contatti
  • Redazione
  • Termini e Condizioni generali
  • Condizioni di utilizzo dei Servizi
  • Informazioni sui Cookie
  • Trattamento dei dati personali