Símbolo de dedução (catraca) em LaTeX (\vdash)

Onde é usado

Catraca (turnstile), indicando que a fórmula da direita é derivável (demonstrável) a partir das hipóteses da esquerda.

A teoria da prova escreve \Gamma \vdash \varphi para a consequência sintática, e a teoria de tipos o usa em julgamentos de tipagem \Gamma \vdash e : \tau. Ele difere de \models, que expressa a consequência semântica (verdade em todos os modelos); os teoremas de correção e completude dizem que as duas coincidem na lógica de primeira ordem. Negue-o com \nvdash. \vdash é uma relação, então o espaçamento é automático. Para regras de inferência, \frac ou um pacote dedicado a árvores de prova produz o traço horizontal, com julgamentos contendo \vdash acima e abaixo. O símbolo espelhado é \dashv.

Exemplo mínimo compilável

Cole isto em um arquivo .tex vazio e compile com pdfLaTeX, XeLaTeX ou LuaLaTeX.

\documentclass{article}
\begin{document}
Proves: $\vdash$

\[ \Gamma, x : \sigma \vdash e : \tau \]
\end{document}

Símbolos relacionados

• Consequência semântica (catraca dupla)\models
• Equivalência (se e somente se)\iff
• Sinal de “portanto”\therefore
• Implicação\implies
• Sinal de “porque”\because
• Seta dupla para a esquerda e para a direita\Leftrightarrow

Perguntas frequentes

Como escrever Símbolo de dedução (catraca) em LaTeX?

Digite \vdash no modo matemático, por exemplo $\Gamma, x : \sigma \vdash e : \tau$. Funciona no LaTeX padrão sem carregar nenhum pacote.

Qual pacote é necessário para \vdash?

Nenhum. \vdash faz parte do LaTeX padrão, então compila só com a classe do documento no preâmbulo.

Posso usar \vdash no modo texto ou só no modo matemático?

Só no modo matemático. Fora de $...$ o LaTeX para com "Missing $ inserted", então no texto escreva $\vdash$. Se você só precisa do glifo no texto, cole o caractere Unicode ⊢ (com XeLaTeX ou LuaLaTeX e uma fonte que o tenha).