Saltar para o conteúdo

Catraca (símbolo)

Origem: Wikipédia, a enciclopédia livre.

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.[1]

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 

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

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.[3] pode ser reproduzida de forma semelhante com barra vertical (|) e um traço (–).

Interpretações

[editar | editar código-fonte]

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 . [4]
  1. Frege 1879
  2. Martin-Löf 1996, p. 15
  3. Unicode standard
  4. p.287 of Stanley, Richard P.. Enumerative Combinatorics. 1st ed. Vol. 2. Cambridge: Cambridge University Press, 1999.