Torniquete (símbolo)

En lógica matemática y ciencias de la computación, el símbolo ⊢ ( ) ha tomado el nombre de torniquete debido a su parecido con un torniquete típico visto desde arriba. También se lo conoce como tee y a menudo se lee como "cede", "prueba", "satisface" o "implica".${\estilo de visualización \vdash}$

El torniquete representa una relación binaria . Tiene varias interpretaciones diferentes en diferentes contextos:

• En epistemología , Per Martin-Löf (1996) analiza el símbolo de esta manera: "...[L]a combinación del Urteilsstrich de Frege , trazo de juicio [|], y el Inhaltsstrich , trazo de contenido [—], llegó a llamarse el signo de aserción". ^[1] La notación de Frege para un juicio de algún contenido${\estilo de visualización \vdash}$

${\displaystyle \vdash A}$

Luego se puede leer

Sé que A es verdadero . ^[2]

En la misma línea, una afirmación condicional

${\displaystyle P\vdash Q}$

Puede leerse como:

De P , sé que Q

• En metalógica , el estudio de los lenguajes formales , el torniquete representa la consecuencia sintáctica (o "derivabilidad"). Es decir, muestra que una cadena puede derivarse de otra en un solo paso, de acuerdo con las reglas de transformación (es decir, la sintaxis ) de algún sistema formal dado . ^[3] Como tal, la expresión

${\displaystyle P\vdash Q}$

significa que Q es derivable de P en el sistema.

En consonancia con su uso para la derivabilidad, un "⊢" seguido de una expresión sin nada que lo preceda denota un teorema , lo que quiere decir que la expresión se puede derivar de las reglas utilizando un conjunto vacío de axiomas . Como tal, la expresión

${\displaystyle \vdash Q}$

significa que Q es un teorema en el sistema.

• En teoría de la demostración , el torniquete se utiliza para indicar "posibilidad de demostración" o "derivabilidad". Por ejemplo, si T es una teoría formal y S es una oración particular en el lenguaje de la teoría, entonces

${\displaystyle T\vdash S}$

significa que S es demostrable a partir de T . ^[4] Este uso se demuestra en el artículo sobre cálculo proposicional . La consecuencia sintáctica de la demostrabilidad debe contrastarse con la consecuencia semántica, denotada por el símbolo de doble torniquete . Se dice que es una consecuencia semántica de , o , cuando todas las posibles valoraciones en las que es verdadera, también es verdadera. Para la lógica proposicional, se puede demostrar que la consecuencia semántica y la derivabilidad son equivalentes entre sí. Es decir, la lógica proposicional es sólida ( implica ) y completa ( implica ) ^[5]${\displaystyle \modelos}$${\estilo de visualización S}$${\estilo de visualización T}$${\displaystyle T\modelos S}$${\estilo de visualización T}$${\estilo de visualización S}$${\displaystyle \modelos}$${\estilo de visualización \vdash}$${\estilo de visualización \vdash}$${\displaystyle \modelos}$${\displaystyle \modelos}$${\estilo de visualización \vdash}$

• En el cálculo de consecuentes , se utiliza el símbolo torniquete para denotar un consecuente . Un consecuente afirma que, si todos los antecedentes son verdaderos, entonces al menos uno de los consecuentes debe ser verdadero.${\displaystyle A_{1},\,\puntos ,A_{m}\,\vdash \,B_{1},\,\puntos ,B_{n}}$${\displaystyle A_{1},\,\puntos ,A_{m}}$${\displaystyle B_{1},\,\puntos ,B_{n}}$
• En el cálculo lambda tipificado , el torniquete se utiliza para separar las suposiciones de tipificación del juicio de tipificación. ^{[6] [7]}
• En la teoría de categorías , se utiliza un torniquete invertido ( ), como en , para indicar que el funtor F es adjunto por la izquierda del funtor G . ^[8] Más raramente, se utiliza un torniquete ( ), como en , para indicar que el funtor G es adjunto por la derecha del funtor F . ^[9]${\estilo de visualización \dashv}$${\estilo de visualización F\dashv G}$ ${\estilo de visualización \vdash}$${\displaystyle G\vdash F}$
• En APL el símbolo se llama "tachuela derecha" y representa la función identidad derecha ambivalente donde tanto X ⊢ Y como ⊢ Y son Y . El símbolo invertido "⊣" se llama "tachuela izquierda" y representa la identidad izquierda análoga donde X ⊣ Y es X y ⊣ Y es Y . ^{[10] [11]}
• En combinatoria , significa que λ es una partición del entero n . ^[12]${\displaystyle \lambda \vdash n}$
• En las calculadoras de la serie HP-41C / CV / CX y HP-42S de Hewlett-Packard , el símbolo (en el punto de código 127 del conjunto de caracteres FOCAL ) se denomina "carácter de anexión" y se utiliza para indicar que los siguientes caracteres se anexarán al registro alfa en lugar de reemplazar el contenido existente del registro. El símbolo también se admite (en el punto de código 148) en una variante modificada del conjunto de caracteres Roman-8 de HP que utilizan otras calculadoras HP.
• En las calculadoras Casio fx-92 Collège 2D y fx-92+ Spéciale Collège, ^[13] el símbolo representa el operador módulo ; al ingresarlo se obtendrá una respuesta de , donde Q es el cociente y R es el resto . En otras calculadoras Casio (como en las variantes belgas , las calculadoras fx-92B Spéciale Collège y fx-92B Collège 2D ^[14] , donde el separador decimal se representa como un punto en lugar de una coma), el operador módulo se representa con ÷R .${\estilo de visualización 5\dash 2}$${\displaystyle Q=2;R=1}$
• En la teoría de modelos , significa implica , cada modelo de es un modelo de .${\displaystyle \varphi \vdash \psi }$${\estilo de visualización \varphi}$${\estilo de visualización \psi}$${\estilo de visualización \varphi}$${\estilo de visualización \psi}$

En TeX , el símbolo del torniquete se obtiene del comando \vdash . ${\estilo de visualización \vdash}$

En Unicode , el símbolo de torniquete ( ⊢ ) se llama tachuela derecha y se encuentra en el punto de código U+22A2. ^[15] (El punto de código U+22A6 se denomina signo de aserción ( ⊦ ).)

• U+22A2 ⊢ VIRAJE DERECHO ( ⊢, ⊢ )
  • = torniquete
  • = prueba, implica, produce
  • = reducible
• U+22A3 ⊣ VIRTUD IZQUIERDA ( ⊣, ⊣ )
  • = torniquete inverso
  • = no teorema, no produce
• U+22AC ⊬ NO PRUEBA ( ⊬ )
  • ≡ 22A2⊢ 0338$

En una máquina de escribir , un torniquete puede estar compuesto por una barra vertical (|) y un guión (–).

En LaTeX hay un paquete de torniquete que emite esta señal de muchas maneras, y es capaz de poner etiquetas debajo o encima de ella, en los lugares correctos. ^[16]

• ꜔ (U+A714) Letra modificadora barra de tono del extremo medio izquierdo
• ├ (U+251C) Dibujos de Cajas Luz Vertical y Derecha
• ㅏ (U+314F) Letra A del hangul
• Ͱ (U+0370) Letra griega mayúscula Heta
• ͱ (U+0371) Letra griega minúscula Heta
• Ⱶ (U+2C75) Letra latina mayúscula media H
• ⱶ (U+2C76) Letra latina minúscula H media
• ⎬ (U+23AC) Pieza central del corchete derecho

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

• Frege, Gottlob (1879). Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens . Halle.
• Iverson, Kenneth (1987). Un diccionario de APL .
• Martin-Löf, Per (1996). "Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas" (PDF) . Nordic Journal of Philosophical Logic . 1 (1): 11–60.(Apuntes de un curso breve en la Università degli Studi di Siena, abril de 1983.)
• Schmidt, David (1994). La estructura de los lenguajes de programación tipificados . MIT Press . ISBN 0-262-19349-3.
• Troelstra, AS ; Schwichtenberg, H. (2000). Teoría básica de la prueba (2.ª ed.). Cambridge University Press . ISBN 978-0-521-77911-1.