Catraca (símbolo)
# Catraca (símbolo)

Na lógica matemática e ciência da computação, o símbolo $\vdash$ recebe o nome de catraca, pela sua semelhança a uma catraca observada de cima. Pode ser lido como "é o que causa", "deduz que", "acarreta em" ou "satisfaz" (sendo este o mais usual). O símbolo foi usado pela primeira vez por Gottlob Frege no seu livro sobre lógica em 1879, Begriffsschrift.
Martin-Löf analisa o símbolo da seguinte forma: "...[A] combinação do Urteilsstrich, da barra de julgamento [ | ], e do Inhaltsstrich, traço de conteúdo, todos de Frege, veio a ser chamado de símbolo de asserção."$^{[2]}$ A notação de Frege para um julgamento de algum conteúdo A
       $\vdash A$
       pode ser lida como:
       Eu sei que $A$ é verdade".
Na mesma linha de raciocínio:
       $P\vdash Q$
       Pode ser lida das seguintes formas:
      * A partir de $P$ , eu sei que $Q$
      * $P$ é o que causa $Q$
      * $Q$ é demonstrável a partir de $P$
No TeX, o simbolo de catraca é obtido do comando \vdash. No Unicode, o simbolo (⊢) é chamado direita tacha e está mapeado no código U+22A2. pode ser reproduzida de forma semelhante com barra vertical (|) e um traço (–).

## Interpretações

A catraca representa uma relação binária. Existe várias interpretações em diferentes contextos:
* Na metalógica, o estudo das linguagens formais; a catraca representa a consequência sintática (ou "derivabilidade"). Ou seja, dada sequência de caracteres, pode ser derivada de outra em um único passo, de acordo com as regras de transformação (regra de inferência) (i.e. a sintática) de dado sistema formal. Dessa forma,
    $P\vdash Q$
    significa que $Q$ é derivável de $P$ no sistema. De acordo com este uso para derivabilidade, o símbolo "$\vdash$" seguido de uma expressão, sem haver sentença precedendo o símbolo, estabelece um teorema, o que significa que essa expressão pode derivar de regras usando um conjunto vazio de axiomas. Logo, a expressão
    $\vdash Q$
    Significa que $Q$ é um teorema no sistema.
* Na Teoria da prova, a catraca é usada para avaliar se é possivel ser provado. Por exemplo, se $T$ é uma teoria formal e $S$ é uma sentença, na linguagem dessa teoria então:
    $T\vdash S$
    Significa que $S$ é demonstrável a partir de $T$.
* No Cálculo lambda simplesmente tipado, a catraca é usada para separar suposições de tipagem de julgamento de tipagem
* Na Teoria das categorias, uma catraca revertida, como no exemplo $F\dashv G$, é usada para indicar que o funtor $F$ é o adjunto à esquerda do funtor $G$.
* Na APL o símbolo é chamado de "tack" à direita e representa a ambivalente função identidade à direita onde ambos X⊢Y e ⊢Y são Y. O símbolo invertido "⊣" é chamado de "tack" à esquerda e representa à análoga identidade à esquerda onde X⊣Y é X e ⊣Y é Y.
* Na Combinatória, $\lambda \vdash n$ significa que $\lambda$ é uma partição do inteiro $n$.

## Notes

* ↑ Frege 1879
* ↑ Martin-Löf 1996, p. 15
* ↑ Unicode standard
* ↑ p.287 of Stanley, Richard P.. Enumerative Combinatorics. 1st ed. Vol. 2. Cambridge: Cambridge University Press, 1999.

## Veja também

* Dupla catraca $\models$
* Sequente
* Cálculo de sequentes
* Lista de símbolos lógicos
* Lista de símbolos matemáticos