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 :
- 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
modifierVoir aussi
modifier- Par conséquent (symbole : « ∴ »)
- Liste des symboles logiques
- Table des symboles mathématiques
Notes et références
modifier- (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- (en) Kenneth E. Iverson, « A Dictionary of APL », APL Quote Quad, vol. 18, no 1, (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, no 1, , 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, , 367 p. (ISBN 0-262-19349-3, lire en ligne)
- (en) Anne S. Troelstra et Helmut Schwichtenberg, Basic Proof Theory, Cambridge University Press, , 417 p. (ISBN 978-0-521-77911-1, lire en ligne)