Na lógica matemática e ciência da computação, o símbolo 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." A notação de Frege para um julgamento de algum conteúdo A 

pode ser lida como: Eu sei que é verdade".

Na mesma linha de raciocínio:

Pode ser lida das seguintes formas: A partir de , eu sei que é o que causa é demonstrável a partir de

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.Unicode standard 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,

significa que é derivável de no sistema. De acordo com este uso para derivabilidade, o símbolo "" 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

Significa que é um teorema no sistema. Na Teoria da prova, a catraca é usada para avaliar se é possivel ser provado. Por exemplo, se é uma teoria formal e é uma sentença, na linguagem dessa teoria então:

Significa que é demonstrável a partir de . 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 , é usada para indicar que o funtor é o adjunto à esquerda do funtor . 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, significa que é uma partição do inteiro . p.287 of Stanley, Richard P.. Enumerative Combinatorics. 1st ed. Vol. 2. Cambridge: Cambridge University Press, 1999.

Notes

Ver também

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

Referências

Lecture notes to a short course at Università degli Studi di Siena, April 1983.

Categoria:Símbolos matemáticos Categoria:Lógica matemática