Carraca (símbolo)

En lóxica matemática e informática o símbolo ⊢ ($⊢$) 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 $⊢$ así: "...A combinación do Modelo:Lang de Frege, golpe de xuízo [ | ] e Modelo:Lang, trazo de contido [—], pasou a chamarse signo de afirmación".Modelo:Sfn Notación de Frege para un xuízo dalgún contido Modelo:Mvar

$⊢A$

entón pódese ler

Sei que Modelo:Mvar é verdade.Modelo:Sfn

Na mesma liña, unha afirmación condicional

$P⊢Q$

pódese ler como:

Por Modelo:Mvar, sei que Modelo:Mvar

• 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⊢Q$

significa que Modelo:Mvar é derivábel de Modelo:Mvar 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

$⊢Q$

significa que Modelo:Mvar é un teorema do sistema.

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

$T⊢S$

significa que Modelo:Mvar é demostrábel a partir de Modelo:Mvar . 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 $⊢$ son equivalentes entre si. É dicir, a lóxica proposicional é sólida ( $⊢$ implica $\models$ ) e completa ( $\models$ implica $⊢$ ).Modelo:Sfn

• No cálculo secuencial, a carrraca úsase para denotar unha secuencia. Unha secuencia $A_1,\dots ,A_m⊢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 ($⊣$), como en $F⊣G$, para indicar que o functor Modelo:Mvar é adxunto pola esquerdo ao functor Modelo:Mvar.

• En combinatoria, $\lambda ⊢n$ significa que Modelo:Mvar é unha partición do enteiro Modelo:Mvar.Modelo:Sfn

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

Véxase tamén

Bibliografía

• Modelo:Cita libro
• Modelo:Cita libro
• Modelo:Cita libro
• Modelo:Cita revista
• Modelo:Cita libro
• Modelo:Cita libro

Outros artigos

• Dupla carraca.
• Lóxica proposicional