Dupla carraca

Na lóxica, o símbolo ⊨, $\vDash$ ou $\models$ chámase dupla carraca ou duplo torniquete. Pódese ler como "consecuencia lóxica", "modelo de", "é unha consecuencia semántica de", ou en inglés "is stronger than".^[1] Unha das súas relacións co símbolo da carraca $\vdash$ (que ten unha soa barra polo medio) é o teorema de completude.

Significado

O dupla carraca é unha relación binaria. O significado depende do contexto:

Cando se expresa a consecuencia lóxica (semántica), cun conxunto de sentenzas á esquerda e unha única sentenza á dereita, preténdese indicar que
se toda sentenza da esquerda é verdade (premisas), a sentenza da dereita será verdadeira, e .g. $\Gamma \vDash \varphi$ . Este uso é moi semellante ao da carraca, o que indica unha consecuencia lóxica (sintáctica).
Cando se expresa a satisfacibilidade, cunha estrutura modelo (ou estrutura de verdade) no lado esquerdo e un conxunto de sentenzas no lado dereito, é para indicar que a estrutura é un modelo para (ou satisfai (ten os recursos necesarios para probar valor verdade)) o conxunto de sentenzas e .g. ${\mathcal {A}}\models \Gamma$ .
Cando se expresa tautoloxía, $\vDash \varphi$ . O que indica que a expresión $\varphi$ é unha consecuencia lóxica (semántica) dun conxunto de sentenzas baleiras, é dicir, é válida semanticamente.