# 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
### Symboles

Un 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

Un 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

Les 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

Une 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. Les propositions sont considérées comme des entités syntaxiques.

### Théories formelles

Une théorie formelle est un ensemble de phrases dans un langage formel.

### Systèmes formels

Un 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

Une formule A est une conséquence syntaxique$^,$$^,$$^,$ au sein d'un système formel ${\mathcal {FS}}$ d'un ensemble Г de formules s'il y a une dérivation dans le système formel ${\mathcal {FS}}$ de A à partir de l'ensemble Г.
    $\Gamma \vdash _{\mathrm {F} S}A$
La conséquence syntaxique ne dépend pas d'une interprétation du système formel.

#### Complétude syntaxique d'un système formel

Un système formel ${\mathcal {S}}$ est syntaxiquement complet$^,$$^,$$^,$ si et seulement si pour chaque formule A du langage du système, soit A, soit ¬A est un théorème de ${\mathcal {S}}$. 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

Une 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.