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$.

Veja também

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

Referências

• Frege, Gottlob (1879). «Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens». Halle 
• Iverson, Kenneth (1987). «A Dictionary of APL» 
• Martin-Löf, Per (1996). «On the meanings of the logical constants and the justifications of the logical laws» (PDF). Nordic Journal of Philosophical Logic. 1 (1): 11–60  Lecture notes to a short course at Università degli Studi di Siena, April 1983.
• Schmidt, David (1994). «The Structure of Typed Programming Languages». MIT Press. ISBN 0-262-19349-3 
• Troelstra, A. S.; Schwichtenberg, H. (2000). «Basic Proof Theory» second ed. Cambridge University Press. ISBN 978-0-521-77911-1