Trinquete (símbolo)

En lógica matemática y ciencias de la computación, el símbolo se llama trinquete, por su semejanza con un trinquete 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

se puede leer como:
Yo se que es verdad".[2]

En la misma línea de razonamiento:

Se puede leer de las siguientes maneras:
  • A partir de , yo sé que
  • es lo que causa
  • es demostrable a partir de

En TeX, el símbolo de trinquete 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:

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,

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

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

Significa que es demostrable a partir de
  • 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 , se utiliza para indicar que el funtor es el del agente a la izquierda del funtor .
  • 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, significa que es una partición del entero . [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

Bibliografía

Enlaces externos

Este artículo ha sido escrito por Wikipedia. El texto está disponible bajo la licencia Creative Commons - Atribución - CompartirIgual. Pueden aplicarse cláusulas adicionales a los archivos multimedia.