Torniquete (símbolo)

En lógica matemática y ciencias de la computación, el símbolo ${\displaystyle \vdash }$ se llama torniquete, por su semejanza con un torniquete o molinillo observado desde arriba. Se puede leer como "es lo que causa", "deduce que", "acarrea en" o "satisfecho" (siendo este el más común). El símbolo fue utilizado por primera vez por Gottlob Frege en su libro sobre la lógica en 1879, Begriffsschrift.[1]​

Martin-Löf analiza el símbolo de la siguiente manera: "... [A] combinación de Urteilsstrich, la barra de ensayo [|], y del Inhaltsstrich, trazo de contenido, todos de Frege, vino a llamarse símbolo de afirmación.."^[2] La notación de Frege para un juicio de algún contenido A

${\displaystyle \vdash A}$

se puede leer como:

Yo se que ${\displaystyle A}$ es verdad".[2]​

En la misma línea de razonamiento:

${\displaystyle P\vdash Q}$

Se puede leer de las siguientes maneras:

• A partir de ${\displaystyle P}$ , yo sé que ${\displaystyle Q}$
• ${\displaystyle P}$ es lo que causa ${\displaystyle Q}$
• ${\displaystyle Q}$ es demostrable a partir de ${\displaystyle P}$

En TeX, el símbolo de torniquete se obtiene de la orden \vdash. En Unicode, el símbolo (⊢) se llama tacha derecha y está mapeado en el código U+22A2.[3]​ Se puede emular en caracteres ASCII con barra vertical (|) y un guion (-).

Interpretaciones

El trinquete representa una relación binaria. Existen varias interpretaciones en diferentes contextos:

• En metalógica, el estudio de los lenguajes formales; el trinquete

representa una consecuencia sintáctica (o "derivabilidad"). Es decir, dada una secuencia de caracteres, se puede derivar otra en un único paso, de acuerdo con las reglas de transformación (regla de inferencia) (es decir, la sintaxis) de un sistema formal dado.

De esa forma,

${\displaystyle P\vdash Q}$

significa que ${\displaystyle Q}$ es derivable de ${\displaystyle P}$ en el sistema.

De acuerdo con este uso para derivabilidad, el símbolo "⊣" seguido de una expresión, sin haber sentencia con ningún símbolo anterior, estableciendo un teorema, lo que significa que tal expresión puede derivar reglas utilizando un conjunto vacío de axiomas. Por lo tanto, la expresión

${\displaystyle \vdash Q}$

Significa que ${\displaystyle Q}$ es un teorema en el sistema.

En teoría de la prueba, el trinquete es usado para evaluar si es posible ser probado.

Por ejemplo, si ${\displaystyle T}$ es una teoría formal y ${\displaystyle S}$ es una sentencia, en el lenguaje de esa teoría entonces:

${\displaystyle T\vdash S}$

Significa que ${\displaystyle S}$ es demostrable a partir de ${\displaystyle T}$

• En el cálculo lambda escrito, el trinquete se utiliza para supuestos de escritura separados de la sentencia a escribir.
• En teoría de las categorías, de trinquete inviertido, como en el ejemplo ${\displaystyle F\dashv G}$, se utiliza para indicar que el funtor ${\displaystyle F}$ es el del agente a la izquierda del funtor ${\displaystyle G}$.
• En símbolo APL es llamado "tack" a la derecha y representa la función identidad ambivalente a la derecha donde tanto X⊢Y y ⊢Y son Y. El símbolo "⊣" Invertido se llama "tack" a la izquierda y representa la identidad análoga a la izquierda donde X⊣Y es X e ⊣Y es Y.
• En Combinatoria, ${\displaystyle \lambda \vdash n}$ significa que ${\displaystyle \lambda }$ es una partición del entero ${\displaystyle n}$.[4]​

Referencias

1. Frege, 1879
2. Martin-Löf, 1996, p. 15
3. Unicode standard
4. p.287 of Stanley, Richard P.. Enumerative Combinatorics. 1st ed. Vol. 2. Cambridge: Cambridge University Press, 1999.

Véase también

• Doble trinquete ${\displaystyle \models }$
• Consecuente
• Cálculo de consecuentes
• Lista de símbolos lógicos
• Lista de símbolos matemáticos

Bibliografía

• Frege, Gottlob (1879). Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens (en inglés). Halle. 
• Iverson, Kenneth (1987). A Dictionary of APL (en inglés). 
• Martin-Löf, Per (1996). «On the meanings of the logical constants and the justifications of the logical laws». Nordic Journal of Philosophical Logic (en inglés) 1 (1): 11-60.  Notas de lectura que un curso corto en Università degli Studi di Siena, abril de 1983.
• Schmidt, David (1994). The Structure of Typed Programming Languages (en inglés). MIT Press. ISBN 0-262-19349-3. 
• Troelstra, A. S.; Schwichtenberg, H. (2000). Basic Proof Theory (en inglés) (2da edición). Cambridge University Press. ISBN 978-0-521-77911-1. 

Enlaces externos

• Esta obra contiene una traducción total derivada de «Catraca (símbolo)» de Wikipedia en portugués, concretamente de esta versión, publicada por sus editores bajo la Licencia de documentación libre de GNU y la Licencia Creative Commons Atribución-CompartirIgual 4.0 Internacional.

• Datos: Q7856108