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.[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 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 editar
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,
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 editar
- ↑ Frege, 1879
- ↑ Martin-Löf, 1996, p. 15
- ↑ Unicode standard
- ↑ p.287 of Stanley, Richard P.. Enumerative Combinatorics. 1st ed. Vol. 2. Cambridge: Cambridge University Press, 1999.
Véase también editar
Bibliografía editar
- 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 editar
- 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
