Dupla catraca

Na lógica, o símbolo ⊨, ${\displaystyle \vDash }$ or ${\displaystyle \models }$ é chamado de dupla catraca. Pode ser lido como "consequência lógica" (acarreta em), "modelo de", "é consequência semântica de " ou no inglês "is stronger than".^[1] Uma de suas relações com o símbolo catraca ${\displaystyle \vdash }$(o qual possui uma barra única atravessada no meio) é o teorema da completude.

No TeX, os símbolos de catracas ${\displaystyle \vdash }$ e ${\displaystyle \models }$ são obtidos pelos comandos \vdash e \models respectivamente. No Unicode está mapeado em U+22A8 ⊨ TRUE (⊨, ⊨)

A dupla catraca é uma relação binária. O significado depende do contexto:

• Ao expressar consequencia lógica (semântica), com um conjunto de sentenças a esquerda e uma única sentença a direita, é buscando indicar que
  se toda sentença a esquerda é verdade (premissas), a sentença a direita será verdade, e.g. ${\displaystyle \Gamma \vDash \varphi }$. Esse uso é bastante parecido com o da catraca, o qual indica consequência lógica (sintática).
• Ao expressar satisfabilidade, com uma estrutura modelo (ou do inglês truth-structure) no lado esquerdo e um conjunto de sentenças no lado direito, é para indicar que a estrutura é modelo para (ou satisfaz (possui os recursos necessários para provar valor verdade)) o conjunto de sentença, e.g. ${\displaystyle {\mathcal {A}}\models \Gamma }$.
• Ao expressar tautologia, ${\displaystyle \vDash \varphi }$. ao qual indica que a expressão ${\displaystyle \varphi }$ é consequência lógica (semântica) de um conjunto vazio de sentenças, ou seja, é semanticamente válida.

• Lista de símbolos lógicos
• Lista de símbolos matemáticos