Rechter turnstile

Hij markeert een conclusie die uit aannames bewezen wordt. In Γ ⊢ T geeft Γ (gamma) de aannames weer en is T de conclusie. Staat er links niets, dan betekent ⊢ T dat T zonder vermelde aannames bewezen kan worden.

De herkenbare voorloper is het beweringsteken dat de Duitse logicus Gottlob Frege in 1879 gebruikte. Het werk van Gerhard Gentzen uit 1934–35 hielp de sequentnotatie ontwikkelen: formele regels die premissen en conclusies van elkaar scheiden.

Waarom verandert ⊢ met de tekens eromheen van betekenis?

De omringende notatie bepaalt de relatie. In de bewijstheorie staat ⊢ voor afleidbaarheid: een bewijs met de regels van een systeem. In een sequent zijn formules links premissen en rechts conclusies. In getypeerde programmeernotatie scheidt het aannames van het oordeel dat een term een bepaald type heeft.