En lógica , el símbolo ⊨, ⊧ ose llama torniquete doble . A menudo se lee como " implica ", " modelos ", "es una consecuencia semántica de" o "es más fuerte que". [1] Está estrechamente relacionado con el símbolo del torniquete., que tiene una sola barra en el medio y que denota consecuencia sintáctica (en contraste con la semántica ).
Significado
El torniquete doble es una relación binaria. Tiene varios significados diferentes en diferentes contextos:
- Para mostrar una consecuencia semántica , con un conjunto de oraciones a la izquierda y una sola oración a la derecha, para denotar que si todas las oraciones de la izquierda son verdaderas, la oración de la derecha debe ser verdadera, p.. Este uso está estrechamente relacionado con el símbolo del torniquete de una sola barra que denota consecuencia sintáctica .
- Para mostrar satisfacción , con un modelo (o estructura de verdad) a la izquierda y un conjunto de oraciones a la derecha, para denotar que la estructura es un modelo para (o satisface) el conjunto de oraciones, p. Ej..
- En este contexto, la consecuencia semántica de la lista anterior puede expresarse como "Para un modelo dado , Si luego ".
- Para denotar una tautología ,. lo que quiere decir que la expresión es una consecuencia semántica del conjunto vacío.
Tipografía
En TeX , los símbolos del torniquete y se obtienen de los comandos \ vDash y \ models respectivamente. En Unicode está codificado en U + 22A8 ⊨ TRUE (HTML ⊨
· &DoubleRightTee, &vDash
)
En LaTeX existe el paquete torniquete , que emite este letrero de muchas formas, incluido el doble torniquete, y es capaz de poner etiquetas debajo o encima de él, en los lugares correctos. El artículo Una herramienta para lógicos es un tutorial sobre el uso de este paquete.