En lógica matemática e informática, el símboloha tomado el nombre de torniquete debido a su parecido con un torniquete típico visto desde arriba. También se conoce como tee y a menudo se lee como "rinde", "prueba", "satisface" o "implica".
En TeX , el símbolo del torniquetese obtiene del comando \ vdash . En Unicode , el símbolo del torniquete ( ⊢ ) se llama virada derecha y está en el punto de código U + 22A2. [1] (El punto de código U + 22A6 se denomina signo de aserción ( ⊦ )). En una máquina de escribir , un torniquete puede estar compuesto por una barra vertical (|) y un guión (-). En LaTeX existe un paquete torniquete que emite este letrero de muchas formas, y es capaz de poner etiquetas debajo o encima de él, en los lugares correctos. [2]
Interpretaciones
El torniquete representa una relación binaria . Tiene varias interpretaciones diferentes en diferentes contextos:
- En epistemología , Per Martin-Löf (1996) analiza lasímbolo así: "... [L] a combinación de Urteilsstrich de Frege , trazo de juicio [|], e Inhaltsstrich , trazo de contenido [-], pasó a llamarse el signo de aserción". [3] Notación de Frege para un juicio de algún contenido A
- luego se puede leer
- Sé que A es verdad . [4]
- En la misma línea, una aserción condicional
- se puede leer como:
- De P , sé que Q
- En metalógica , el estudio de lenguajes formales ; el torniquete representa una 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 . [5] Como tal, la expresión
- significa que Q es derivable de P en el sistema.
- De acuerdo con su uso para la derivabilidad, una "⊢" seguida de una expresión sin nada que la preceda denota un teorema , lo que quiere decir que la expresión puede derivarse de las reglas usando un conjunto vacío de axiomas . Como tal, la expresión
- significa que Q es un teorema en el sistema.
- En la teoría de la prueba , el torniquete se usa para denotar "demostrabilidad" 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
- medios que S es demostrable de T . [6] 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 del doble torniquete.. Uno dice que es una consecuencia semántica de , o , cuando todas las valoraciones posibles en las que es verdad, también es cierto. Para la lógica proposicional, se puede demostrar que la consecuencia semántica y derivabilidad son equivalentes entre sí. Es decir, la lógica proposicional es sólida ( implica ) y completa ( implica ) [7]
- En el cálculo lambda mecanografiado , el torniquete se utiliza para separar las suposiciones de mecanografía del juicio de mecanografía. [8] [9]
- En la teoría de categorías , un torniquete invertido (), como en , Se utiliza para indicar que el funtor F es adjunto izquierdo al funtor G . [10] Más raramente, un torniquete (), como en , Se utiliza para indicar que el funtor G es adjunto derecho a la funtor F . [11]
- En APL el símbolo se llama "tack derecha" y representa la función identidad derecho ambivalente donde tanto X ⊢ Y y ⊢ Y son Y . El símbolo inversa "⊣" se llama "tack izquierda" y representa la identidad análoga izquierda donde X ⊣ Y es X y ⊣ Y es Y . [12] [13]
- En combinatoria ,significa que λ es una partición del entero n . [14]
- En Hewlett-Packard 's HP-41C / CV / CX y HP-42S serie de calculadoras, el símbolo (en el punto de código 127 en el conjunto de caracteres FOCAL ) se llama 'carácter Anexar' y se emplea para indicar que los siguientes caracteres se anexarse al registro alfabético 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 juego de caracteres HP Roman-8 utilizado por otras calculadoras HP.
- En las calculadoras Casio fx-92 Collège 2D y fx-92 + Spéciale Collège, [15] el símbolo representa el operador de módulo ; entrando producirá 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 [16], donde el separador decimal se representa como un punto en lugar de una coma), el operador de módulo está representado por ÷ R en su lugar.
Grafemas similares
- ꜔ (U + A714) Letra modificadora Media barra de tono de la columna izquierda
- ├ (U + 251C) Dibujos de caja de luz vertical y derecha
- ㅏ (U + 314F) Coreano Ah
- Ͱ (U + 0370) Letra griega mayúscula Heta
- ͱ (U + 0371) Letra griega minúscula Heta
- Ⱶ (U + 2C75) Letra mayúscula latina mitad H
- ⱶ (U + 2C76) Letra latina minúscula mitad H
- ⎬ (U + 23AB) Corchete derecho
Ver también
- Torniquete doble
- Consecuente
- Cálculo secuencial
- Lista de símbolos lógicos
- Lista de símbolos matemáticos
Notas
- ^ Estándar Unicode
- ^ http://www.ctan.org/tex-archive/macros/latex/contrib/turnstile
- ^ Martin-Löf 1996 , págs.6, 15
- ^ Martin-Löf 1996 , p. 15
- ^ Capítulo 6, Teoría del lenguaje formal
- ^ Troelstra y Schwichtenberg 2000
- ^ Dirk van Dalen, Lógica y estructura (1980), Springer, ISBN 3-540-20879-8 . Consulte el Capítulo 1, sección 1.5.
- ^ Peter Selinger, Notas de la conferencia sobre el cálculo Lambda
- ^ Schmidt 1994
- ^ functor adjunto en nLab
- ^ @FunctorFact (5 de julio de 2016). "Functor Fact en Twitter" (Tweet) - a través de Twitter .
- ^ Iverson, diccionario APL
- ^ Iverson 1987
- ^ Stanley, Richard P. (1999). Combinatoria enumerativa . Vol. 2 (1ª ed.). Cambridge: Cambridge University Press. pag. 287.
|volume=
tiene texto extra ( ayuda ) - ^ fx-92 Spéciale Collège Mode d'emploi (PDF) . CASIO COMPUTER CO., LTD. 2015. p. 12.
- ^ "Cálculos restantes - Manual del usuario de Casio fx-92B [Página 13] | ManualsLib" . www.manualslib.com . Consultado el 24 de diciembre de 2020 .
Referencias
- Frege, Gottlob (1879). "Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens". Halle. Cite journal requiere
|journal=
( ayuda ) - Iverson, Kenneth (1987). "Un diccionario de APL". Cite journal requiere
|journal=
( ayuda ) - Martin-Löf, Per (1996). "Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas" (PDF) . Revista nórdica de lógica filosófica . 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 mecanografiados". Prensa del MIT . ISBN 0-262-19349-3. Cite journal requiere
|journal=
( ayuda ) - Troelstra, AS ; Schwichtenberg, H. (2000). "Teoría básica de la prueba" (2ª ed.). Prensa de la Universidad de Cambridge . ISBN 978-0-521-77911-1. Cite journal requiere
|journal=
( ayuda )