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. ⊢ est une relation agissant sur les formules elles-mêmes, sans pour autant en engendrer une : faisant partie du métalangage, les phrases du type « [formule] ⊢ [formule] » ayant alors le statut distinct de séquent. Le taquet s'emploie parfois sur plus ou moins de deux formules, bien qu'on puisse toujours se ramener à deux formules, comme suit :

• $\vdash A$ peut être lu comme A est prouvable par tout, $A\vdash$ peut être lu comme tout est prouvable par A. Cependant, ces deux notations sont également descriptibles par la relation initiale, via les formules $\top \vdash A$ et $A\vdash \bot$.
• De même, $\vdash$ peut décrire $\top \vdash \bot$ si employé comme séquent. La validité de cette formule serait logique syntaxiquement équivalente au trivialisme, car tout serait prouvable par tout via la règle de coupure.
• Enfin, il arrive souvent d'utiliser plusieurs formules à la suite, d'un côté comme de l'autre du taquet : $A_{1},\cdots ,A_{n}\vdash B_{1},\cdots ,B_{n}$. Cependant, on peut utiliser les opérations de conjonction et de disjonction pour se ramener à une seule formule de part et d'autre du taquet : $A_{1}\wedge \cdots \wedge A_{n}\vdash B_{1}\vee \cdots \vee B_{n}$.

On peut synthétiser chacun de ces cas en considérant, par convention, l'objet terminal $\top$ et l'objet initial $\bot$ comme étant, respectivement, la conjonction vide et la disjonction vide.

C'est le philosophe allemand Gottlob Frege qui introduisit le symbole ⊢, dans son Idéographie (Begriffsschrift) de 1879 : le trait horizontal signifiant l’affirmation d’une proposition, le trait vertical l’affirmation de sa véracité, la déduction fut représentée comme la combinaison de ces deux notions. Le symbole fut repris par Whitehead et Russell dans leurs Principia mathematica (1910).

Symboles d'apparence similaire

• ꜔ (U+A714) 
• ├ (U+251C) 
• ㅏ (U+314F) Ah coréen
• Ͱ (U+0370) lettre grecque heta majuscule
• ͱ (U+0371) lettre grecque heta minuscule
• Ⱶ (U+2C75) lettre latine demi-H majuscule
• ⱶ (U+2C76) lettre latine demi-H minuscule
• ⎬ (U+23AB) Demi parenthèse droite

Voir aussi

• Par conséquent (symbole : « ∴ »)
• Liste des symboles logiques
• Table des symboles mathématiques

Bibliographie

• (en) Kenneth E. Iverson, « A Dictionary of APL », APL Quote Quad, vol. 18, n^o 1,‎ septembre 1987 (lire en ligne)
• Martin-Löf, « On the meanings of the logical constants and the justifications of the logical laws », Nordic Journal of Philosophical Logic, vol. 1, n^o 1,‎ 1996, p. 11–60 (lire en ligne) (Lecture notes to a short course at Università degli Studi di Siena, April 1983.)
• (en) David A. Schmidt, The Structure of Typed Programming Languages, Cambridge, MIT Press, 1994, 367 p. (ISBN 0-262-19349-3, lire en ligne)
• (en) Anne S. Troelstra et Helmut Schwichtenberg, Basic Proof Theory, Cambridge University Press, 2000, 417 p. (ISBN 978-0-521-77911-1, lire en ligne)