Syntaxe (logique)
En logique, la syntaxe concerne les règles utilisées pour la construction de symboles et des mots d'un langage, par opposition à la sémantique d'une langue qui concerne sa signification. La syntaxe n'a rien à voir avec les langages formels ou les systèmes formels sans tenir compte de l'interprétation ou du sens qui leur est donné.
Les symboles, formules, systèmes, théorèmes, preuves et interprétations exprimées dans un langage formel sont des entités syntaxiques dont les propriétés peuvent être étudiées sans tenir compte du tout sens qu'on peut leur donner.
La syntaxe est généralement associée aux règles (ou grammaire) gouvernant la composition des textes dans un langage formel qui constituent les formules bien formées dans un langage de programmation.
En informatique, la syntaxe (en) est un terme qui se réfère aux règles régissant la composition des expressions bien formées dans un langage de programmation. Comme dans la logique mathématique, elle est indépendante de la sémantique et de l'interprétation.
Entités syntaxiques
modifier
Symboles
modifierUn symbole est une idée, une abstraction ou un concept. Les symboles d'un langage formel ne doivent pas être des symboles de rien. Par exemple, il y a des constantes logiques qui ne se réfèrent pas à une idée, mais servent plutôt comme une forme de ponctuation dans le langage (par exemple les parenthèses). Un symbole ou une chaîne de symboles peut comprendre une formule bien formée si la formulation est compatible avec les règles de formation du langage.
Langage formel
modifierUn langage formel est une entité syntaxique qui se compose d'un ensemble de chaînes finies de symboles qui sont ses mots. Un tel langage peut être défini sans référence à des significations de l'une de ses expressions; il peut exister avant que toute interprétation lui ait été attribué.
Règles de formation
modifierLes règles de formation sont une description précise de quelles chaînes de symboles sont des formules bien formées d'un langage formel. Cependant, il ne décrit pas leur sémantique (ce qu'ils signifient).
Propositions
modifierUne proposition est une phrase qui exprime quelque chose de vrai ou faux. Une proposition est identifiée ontologiquement à une idée, un concept ou une abstraction[1]. Les propositions sont considérées comme des entités syntaxiques.
Théories formelles
modifierUne théorie formelle est un ensemble de phrases dans un langage formel.
Systèmes formels
modifierUn système formel (également appelé système logique) se compose d'un langage formel et d'un appareil déductif. Les systèmes formels, comme les autres entités syntaxiques, peuvent être définis sans aucune interprétation donnée.
Conséquence syntaxique d'un système formel
modifierUne formule A est une conséquence syntaxique[2],[3],[4],[5] au sein d'un système formel d'un ensemble Г de formules s'il y a une dérivation dans le système formel de A à partir de l'ensemble Г.
La conséquence syntaxique ne dépend pas d'une interprétation du système formel[6].
Complétude syntaxique d'un système formel
modifierUn système formel est syntaxiquement complet[7],[8],[9],[10] si et seulement si pour chaque formule A du langage du système, soit A, soit ¬A est un théorème de . Le théorème d'incomplétude de Gödel montre qu'aucun système récursif qui est suffisamment puissant, comme les axiomes de Peano, ne peut être à la fois cohérent et complet.
Interprétation
modifierUne interprétation d'un système formel est l'attribution des significations aux des symboles et aux valeurs de vérité aux phrases d'un système formel. L'étude des interprétations est appelée la sémantique formelle. Donner une interprétation est synonyme de construction d'un modèle. Une interprétation est exprimée dans un métalangage, qui peut être lui-même un langage formel, et en tant que telle une entité syntaxique.
Références
modifier- (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Syntax (logic) » (voir la liste des auteurs).
- Geoffrey Hunter, Metalogic.
- (en) M. Dummett, Frege : Philosophy of Language, Harvard University Press, , 708 p. (ISBN 978-0-674-31931-8, lire en ligne), p. 82.
- (en) J. Lear, Aristotle and Logical Theory, Cambridge University Press, , 136 p. (ISBN 978-0-521-31178-6, lire en ligne), p. 1.
- (en) R. Creath et M. Friedman, The Cambridge Companion to Carnap, Cambridge, Cambridge University Press, , 371 p. (ISBN 978-0-521-84015-6, lire en ligne), p. 189.
- (en) « syntactic consequence from FOLDOC », swif.uniba.it (consulté le ).
- (en) Geoffrey Hunter, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Pres, 1971, p. 75.
- (en) « A Note on Interaction and Incompleteness » [PDF] (consulté le ).
- (en) « Normal forms and syntactic completeness proofs for functional independencies », portal.acm.org (consulté le ).
- (en) J. Barwise, Handbook of Mathematical Logic, Elsevier Science, , 1164 p. (ISBN 978-0-08-093364-1, lire en ligne), p. 236.
- (en) « syntactic completeness from FOLDOC », swif.uniba.it (consulté le ).
