Catraca (símbolo)

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."^[2] A notação de Frege para um julgamento de algum conteúdo A 

$⊢A$

pode ser lida como:

Eu sei que $A$ é verdade".

Na mesma linha de raciocínio:

$P⊢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⊢Q$

significa que $Q$ é derivável de $P$ 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

$⊢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⊢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⊣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 ⊢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

• Predefinição:Citar periódico
• Predefinição:Citar periódico
• Predefinição:Citar periódico Lecture notes to a short course at Università degli Studi di Siena, April 1983.
• Predefinição:Citar periódico
• Predefinição:Citar periódico