Ver o código fonte de «Carraca (símbolo)»

En [[lóxica matemática]] e [[Ciencias da computación|informática]] o símbolo ⊢ (<math>\vdash</math>) 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ón (lóxica)|interpretacións]] diferentes en diferentes contextos:

* En [[epistemoloxía]], Per Martin-Löf (1996) analiza o símbolo <math>\vdash</math> así: "...A combinación do {{Lang|de|Urteilsstrich}} de Frege, golpe de xuízo [&nbsp;|&nbsp;] e {{Lang|de|Inhaltsstrich}}, trazo de contido [—], pasou a chamarse signo de afirmación".{{Sfn|Martin-Löf|1996|pp=6, 15}} Notación de Frege para un [[Xuízo (lóxica)|xuízo]] dalgún contido {{Mvar|A}}

:: <math>\vdash A</math>
: entón pódese ler
:: ''Sei que {{Mvar|A}} é verdade''.{{Sfn|Martin-Löf|1996|p=15}}
: Na mesma liña, unha afirmación condicional
:: <math>P \vdash Q</math>
: pódese ler como:
:: ''Por {{Mvar|P}}, sei que {{Mvar|Q}}''

* En [[metalóxica]], o estudo das [[linguaxe formal|linguaxes formais]]; o torniquete representa [[Consecuencia lóxica|a consecuencia sintáctica]] (ou "derivabilidade"). É dicir, que mostra que unha cadea pode [[Proba formal|derivarse]] doutra nun só paso, segundo as [[Regra de inferencia|regras de inferencia]] (é dicir, a [[Sintaxe (loxica)|sintaxe]]) dun sistema formal determinado.<ref>{{Cita web|url=http://dingo.sbs.arizona.edu/~hammond/ling178-sp06/mathCh6.pdf|title=Chapter 6, Formal Language Theory}}</ref> Como tal, a expresión

:: <math>P \vdash Q</math>
: significa que {{Mvar|Q}} é derivábel de {{Mvar|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 [[Axioma|axiomas]]. Como tal, a expresión
:: <math>\vdash Q</math>
: significa que {{Mvar|Q}} é un teorema do sistema.

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

:: <math>T \vdash S</math>
: significa que {{Mvar|S}} é demostrábel a partir de {{Mvar|T}} . <ref>{{Cita Harvard sen parénteses|Troelstra|Schwichtenberg|2000}}</ref> Este uso demóstrase no artigo sobre [[Lóxica proposicional|cálculo proposicional]] . A consecuencia sintáctica da demostrabilidade debería contrastarse coa consecuencia semántica, denotada polo símbolo [[Dupla carraca|do dobre torniquete]] <math>\models</math>. Dicimos que <math>S</math> é unha consecuencia semántica de <math>T</math>, ou <math>T \models S</math>, cando todas [[Valoración (lóxica)|as valoracións]] posíbeis nas que <math>T</math> é verdade, <math>S</math> tamén é verdade. Para a lóxica proposicional, pódese mostrar que consecuencia semántica <math>\models</math> e derivabilidade <math>\vdash</math> son equivalentes entre si. É dicir, a lóxica proposicional é sólida ( <math>\vdash</math> implica <math>\models</math> ) e completa ( <math>\models</math> implica <math>\vdash</math> ).{{Sfn|Dalen|1980}}

* No cálculo secuencial, a carrraca úsase para denotar unha secuencia. Unha secuencia <math>A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n</math> afirma que, se todos os antecedentes <math>A_1,\,\dots,A_m</math> son verdadeiros, entón polo menos un dos consecuentes <math>B_1,\,\dots,B_n</math> debe ser verdadeiro.

* Na [[teoría de categorías]], úsase unha carraca invertida (<math>\dashv</math>), como en <math>F \dashv G</math>, para indicar que o [[functor]] {{ mvar|F}} é [[functor adxunto|adxunto pola esquerdo]] ao functor {{mvar|G}}.<ref>{{Cita web|url=https://ncatlab.org/nlab/show/adjoint+functor|title=adjoint functor in nLab|website=ncatlab.org}}</ref> 

* En [[Combinatoria|combinatoria]], <math>\lambda \vdash n</math> significa que {{Mvar|&lambda;}} é unha partición do enteiro {{Mvar|n}}.{{Sfn|Stanley|1999|p=287}}

* En teoría de modelos <math>\varphi \vdash \psi</math> significa que <math>\varphi</math> entails <math>\psi</math>, every model of <math>\varphi</math> is a model of <math>\psi</math>.

== Notas ==
{{Listaref|30em}} 

== Véxase tamén ==
=== Bibliografía ===
{{Refempeza}}

* {{Cita libro|título=Logic and Structure|apelidos=Dalen|nome=Dirk van|ano=1980|editorial=Springer|isbn=3-540-20879-8|lingua=en|ref=harv}}
* {{cita libro |author-last=Frege |author-first=Gottlob |author-link=Gottlob Frege |title=Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens |publisher=Halle |date=1879|lingua=de|ref=harv}}
* {{cita libro |author-last=Iverson |author-first=Kenneth |author-link=Kenneth E. Iverson |title=A Dictionary of APL |date=1987|lingua=en|ref=harv}}
* {{cita revista |author-last=Martin-Löf |author-first=Per |author-link=Per Martin-Löf |url=http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf |title=On the meanings of the logical constants and the justifications of the logical laws |journal=[[Nordic Journal of Philosophical Logic]] |volume=1 |issue=1 |date=1996 |pages=11–60 |lingua=en |ref=harv |data-acceso=26 de decembro de 2024 |data-arquivo=08 de decembro de 2023 |url-arquivo=https://web.archive.org/web/20231208203042/http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf |url-morta=yes }}
* {{Cita libro|apelido=Stanley|nome=Richard P.|título=Enumerative Combinatorics|editorial=Cambridge University Press|ano=1999|lingua=en|ref=harv}}
* {{cita libro |author-last1=Troelstra |author-first1=A. S. |author-link1=A. S. Troelstra |author-last2=Schwichtenberg |author-first2=H. |author-link2=H. Schwichtenberg |title=Basic Proof Theory |url=https://archive.org/details/basicprooftheory0000troe_l1x1 |edition=2nd |publisher=[[Cambridge University Press]] |date=2000 |isbn=978-0-521-77911-1|lingua=en|ref=harv}}

{{Reftermina}}

=== Outros artigos ===
* [[Dupla carraca]].
* [[Lóxica proposicional]]

{{Control de autoridades}}

[[Categoría:Símbolos matemáticos]]
[[Categoría:Lóxica matemática]]
[[Categoría:Informática]]