Carraca (símbolo)

En lóxica matemática e informática o símbolo ⊢ ($\vdash$) tomou o nome de carraca ou torniquete pola súa semellanza cun co instrumento musical de percusión ou co aparello de acceso aos licais. Adoita lerse como "demostra", "satisfai" ou "implica".

Interpretacións

A matraca representa unha relación binaria. Ten varias interpretacións diferentes en diferentes contextos:

• En epistemoloxía, Per Martin-Löf (1996) analiza o símbolo $\vdash$ así: "...A combinación do Urteilsstrich de Frege, golpe de xuízo [ | ] e Inhaltsstrich, trazo de contido [—], pasou a chamarse signo de afirmación". Notación de Frege para un xuízo dalgún contido A

$\vdash A$

entón pódese ler

Sei que A é verdade.

Na mesma liña, unha afirmación condicional

$P\vdash Q$

pódese ler como:

Por P, sei que Q

• En metalóxica, o estudo das linguaxes formais; o torniquete representa a consecuencia sintáctica (ou "derivabilidade"). É dicir, que mostra que unha cadea pode derivarse doutra nun só paso, segundo as regras de inferencia (é dicir, a sintaxe) dun sistema formal determinado. Como tal, a expresión

$P\vdash Q$

significa que Q é derivábel de P no sistema.

En consonancia co seu uso para a derivabilidade, un "⊢" seguido dunha expresión sen nada que o precede denota un teorema, é dicir, que a expresión pode derivarse das regras usando un conxunto baleiro de axiomas. Como tal, a expresión

$\vdash Q$

significa que Q é un teorema do sistema.

• Na teoría da proba, o torniquete úsase para denotar "demostrabilidade" ou "derivabilidade". Por exemplo, se T é unha teoría formal e S é unha sentenza particular na linguaxe da teoría, entón

$T\vdash S$

significa que S é demostrábel a partir de T . Este uso demóstrase no artigo sobre cálculo proposicional . A consecuencia sintáctica da demostrabilidade debería contrastarse coa consecuencia semántica, denotada polo símbolo do dobre torniquete $\models$. Dicimos que $S$ é unha consecuencia semántica de $T$, ou $T\models S$, cando todas as valoracións posíbeis nas que $T$ é verdade, $S$ tamén é verdade. Para a lóxica proposicional, pódese mostrar que consecuencia semántica $\models$ e derivabilidade $\vdash$ son equivalentes entre si. É dicir, a lóxica proposicional é sólida ( $\vdash$ implica $\models$ ) e completa ( $\models$ implica $\vdash$ ).

• No cálculo secuencial, a carrraca úsase para denotar unha secuencia. Unha secuencia $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ afirma que, se todos os antecedentes $A_{1},\,\dots ,A_{m}$ son verdadeiros, entón polo menos un dos consecuentes $B_{1},\,\dots ,B_{n}$ debe ser verdadeiro.

• Na teoría de categorías, úsase unha carraca invertida ($\dashv$), como en $F\dashv G$, para indicar que o functor F é adxunto pola esquerdo ao functor G.

• En combinatoria, $\lambda \vdash n$ significa que λ é unha partición do enteiro n.

• En teoría de modelos $\varphi \vdash \psi$ significa que $\varphi$ entails $\psi$, every model of $\varphi$ is a model of $\psi$.

Véxase tamén

Bibliografía

• Dalen, Dirk van (1980). Logic and Structure (en inglés). Springer. ISBN 3-540-20879-8. 
• Frege, Gottlob (1879). Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens (en alemán). 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" (PDF). Nordic Journal of Philosophical Logic (en inglés) 1 (1): 11–60. 
• Stanley, Richard P. (1999). Enumerative Combinatorics (en inglés). Cambridge University Press. 
• Troelstra, A. S.; Schwichtenberg, H. (2000). Basic Proof Theory (en inglés) (2nd ed.). Cambridge University Press. ISBN 978-0-521-77911-1. 

Outros artigos

• Dupla carraca.
• Lóxica proposicional