In mathematical logic and computer science the symbol ⊢ () has taken the name turnstile because of its resemblance to a typical turnstile if viewed from above. It is also referred to as tee and is often read as "yields", "proves", "satisfies" or "entails". The turnstile represents a binary relation. It has several different interpretations in different contexts: In epistemology, Per Martin-Löf (1996) analyzes the symbol thus: "...[T]he combination of Frege's Urteilsstrich, judgement stroke [ | ], and Inhaltsstrich, content stroke [—], came to be called the assertion sign." Frege's notation for a judgement of some content A can then be read I know A is true. In the same vein, a conditional assertion can be read as: From P, I know that Q In metalogic, the study of formal languages; the turnstile represents syntactic consequence (or "derivability"). This is to say, that it shows that one string can be derived from another in a single step, according to the transformation rules (i.e. the syntax) of some given formal system. As such, the expression means that Q is derivable from P in the system. Consistent with its use for derivability, a "⊢" followed by an expression without anything preceding it denotes a theorem, which is to say that the expression can be derived from the rules using an empty set of axioms. As such, the expression means that Q is a theorem in the system. In proof theory, the turnstile is used to denote "provability" or "derivability". For example, if T is a formal theory and S is a particular sentence in the language of the theory then means that S is provable from T. This usage is demonstrated in the article on propositional calculus. The syntactic consequence of provability should be contrasted to semantic consequence, denoted by the double turnstile symbol . One says that is a semantic consequence of , or , when all possible valuations in which is true, is also true. For propositional logic, it may be shown that semantic consequence and derivability are equivalent to one-another.

À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.