O símbolo "" apresenta algumas denominações, entre elas "barra de Frege",Este termo foi proposto em agosto de 2007 pelos Professores Jean-Yves Béziau e Décio Krause, na lista acadêmica brasileira dos profissionais e estudantes da área de Lógica. "barra de inferência",Marcus Ritt, Lógica - Notas de Aula. "traço de asserção",John Nolt e Dennis Rohatyn, Lógica, Makron Books e McGraw-Hill, 1991. "martelo",João Branquinho e Desidério Murcho (organizadores), Enciclopédia de Termos Lógico-Filosóficos, Gradiva, Lisboa, 2001. "catraca", e "borboleta de Frege", entre outras.Todos estes termos foram propostos por pesquisadores em Lógica na lista acadêmica brasileira dos profissionais e estudantes da área de Lógica, em agosto de 2007. É lido muitas vezes como "afirma-se" ou "obtém-se". Foi usado pela primeira vez por Gottlob Frege em seu livro publicado em 1879.Gottlob Frege, Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Halle, 1879.
No Unicode, uma das principais formas da barra de Frege é chamada de "right tack" e está em 0x22A2.Unicode standard. Em uma máquina de escrever, a barra de Frege pode ser composta de uma barra vertical (|) mais um ou dois traços (-). Em TeX, a barra de Frege é obtida pelo comando \vdash. Em LaTeX há o pacote turnstile, o qual desenha este sinal de várias formas, e pode colocar, abaixo ou acima deste, dados adicionais, nos lugares adequados. O artigo Uma Ferramenta para Lógicos é um tutorial a respeito do uso deste pacote.
Significado A barra de Frege pode ser vista, em muitos casos, como uma relação binária. Esta tem distintos significados em diferentes contextos: Em teoria da prova, a barra de Frege é usada para denotar provabilidade. Por exemplo, se T é um sistema formal e S é uma fórmula na linguagem deste sistema, então significa que S é provável a partir de T.A. S. Troelstra e H. Schwichtenberg, Basic Proof Theory, segunda edição, Cambridge University Press, 2000. Na teoria dos modelos este símbolo é usado para denotar a relação de conseqüência semântica. Em uma lógica dotada de semântica, temos que uma fórmula nesta lógica é conseqüência semântica de uma dada coleção de fórmulas nesta lógica se toda interpretação nesta lógica que satisfizer esta coleção de fórmulas também satisfaz a fórmula considerada. No estudo das Linguagens Formais, a barra de Frege é usada para dizer que uma samblagem pode ser derivada de outra em um único passo, de acordo com as regras da linguagem formal considerada.
Categoria:Lógica Categoria:Linguagens formais