Torniquete (símbolo)

En lógica matemática y ciencias de la computación, el símbolo $⊢$ 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.

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

$⊢A$

se puede leer como:

Yo se que $A$ es verdad".

En la misma línea de razonamiento:

$P⊢Q$

Se puede leer de las siguientes maneras:

• A partir de $P$ , yo sé que $Q$
• $P$ es lo que causa $Q$
• $Q$ es demostrable a partir de $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. 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,

$P⊢Q$

significa que $Q$ es derivable de $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

$⊢Q$

Significa que $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 $T$ es una teoría formal y $S$ es una sentencia, en el lenguaje de esa teoría entonces:

$T⊢S$

Significa que $S$ es demostrable a partir de $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 $F⊣G$, se utiliza para indicar que el funtor $F$ es el del agente a la izquierda del funtor $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, $\lambda ⊢n$ significa que $\lambda$ es una partición del entero $n$.

Véase también

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

Bibliografía

• Plantilla:Cita publicación
• Plantilla:Cita publicación
• Plantilla:Cita publicación Notas de lectura que un curso corto en Università degli Studi di Siena, abril de 1983.
• Plantilla:Cita publicación
• Plantilla:Cita publicación