Turnstile destro

Segna una conclusione dimostrata a partire da ipotesi. In Γ ⊢ T, Γ (gamma) elenca le ipotesi e T è la conclusione. Se a sinistra non c’è nulla, ⊢ T significa che T si può dimostrare senza ipotesi indicate.

L’antecedente riconoscibile è il segno di asserzione usato dal logico tedesco Gottlob Frege nel 1879. Il lavoro di Gerhard Gentzen del 1934–35 contribuì allo sviluppo della notazione dei sequents: righe formali che separano premesse e conclusioni.

Perché ⊢ cambia significato in base ai segni vicini?

La notazione circostante determina la relazione. Nella teoria della dimostrazione, ⊢ indica derivabilità: una prova che segue le regole di un sistema. In un sequente, le formule a sinistra sono premesse e quelle a destra sono conclusioni. Nella notazione della programmazione con tipi, separa le ipotesi da un giudizio secondo cui un termine ha un certo tipo.