Prawy turnstile

Oznacza wniosek udowodniony na podstawie założeń. W Γ ⊢ T symbol Γ (gamma) wymienia założenia, a T jest wnioskiem. Jeśli po lewej nic nie ma, ⊢ T oznacza, że T można udowodnić bez podanych założeń.

Rozpoznawalnym poprzednikiem tego znaku jest znak asercji używany przez niemieckiego logika Gottloba Fregego w 1879 roku. Prace Gerharda Gentzena z lat 1934–35 pomogły rozwinąć zapis sekwentów: formalnych wierszy oddzielających przesłanki od wniosków.

Dlaczego ⊢ zmienia znaczenie zależnie od sąsiednich znaków?

Otaczający zapis określa relację. W teorii dowodu ⊢ oznacza wyprowadzalność, czyli dowód zgodny z regułami danego systemu. W sekwencie formuły po lewej są przesłankami, a po prawej wnioskami. W zapisie programowania z typami oddziela założenia od sądu, że term ma określony typ.