Taquet (symbole) — Wikipédia

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 :

  • peut être lu comme A est prouvable par tout, peut être lu comme tout est prouvable par A. Cependant, ces deux notations sont également descriptibles par la relation initiale, via les formules et .
  • De même, peut décrire 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 : . 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 : .

On peut synthétiser chacun de ces cas en considérant, par convention, l'objet terminal et l'objet initial 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[1] : 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

[modifier | modifier le code]
  • ꜔ (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

Notes et références

[modifier | modifier le code]
  1. (de) Frege, Gottlob (1848-1925), Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, L. Nebert (Halle a/S.), , X-88 p. ; in-8 (lire en ligne), p. 1

Bibliographie

[modifier | modifier le code]