Taquet (symbole)

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.

Concepts associés (13)

Séances de cours associées (3)

Logiques sous-structurelles

Les logiques sous-structurelles sont des logiques mathématiques où certaines règles d'inférence ne sont pas utilisées ou ont une utilisation restreinte. En particulier, par rapport à la logique classique ou à la logique intuitionniste, il leur manque la règle de contraction qui dit peu ou prou que si on peut faire un raisonnement avec une même hypothèse invoquée deux fois, on peut faire le même raisonnement sans dupliquer cette hypothèse et la règle d'affaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement.

Taquet (symbole)

En logique mathématique et en informatique le symbole taquet, « ⊢ », désigné ainsi en raison de sa ressemblance au système de blocage des voiles sur un bateau, représente la déduction logique. La formule « x ⊢ y » signifie « y est déductible de x », c'est-à-dire que y est prouvable à partir de x. On peut aussi employer le taquet comme un opérateur unaire : peut être lu comme : Je sais que A est vrai.

Déduction naturelle

En logique mathématique, la déduction naturelle est un système formel où les règles de déduction des démonstrations sont proches des façons naturelles de raisonner. C'est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons : contrairement aux systèmes à la Hilbert fondés sur des listes d'axiomes logiques plus ou moins ad hoc, la déduction naturelle repose sur un principe systématique de symétrie : pour chaque connecteur, on donne une paire de règles duales (introduction/élimination) ; elle a conduit Gentzen à inventer un autre formalisme très important en théorie de la démonstration, encore plus « symétrique » : le calcul des séquents ; elle a permis dans les années 1960 d'identifier la première instance de l'isomorphisme de Curry-Howard.

Coefficients calorimétriques

Couvre les définitions et les relations entre les coefficients calorimétriques dans des gaz parfaits.

Calcul séquentiel: bases et applications

Couvre les bases et les applications du calcul séquentiel en logique et théorie des preuves, y compris l'élimination des coupes et l'analyse des preuves pratiques.

Portes logiques et élimination des dangers

Explore les portes logiques, l'élimination des risques, les ALU, les compteurs et les registres à décalage dans la technologie des semi-conducteurs.