Syntaxe (logique)

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.

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

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

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

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

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.

Une formule A est une conséquence syntaxique[2] - [3] - [4] - [5] au sein d'un système formel ${\displaystyle {\mathcal {FS}}}$ d'un ensemble Г de formules s'il y a une dérivation dans le système formel ${\displaystyle {\mathcal {FS}}}$ de A à partir de l'ensemble Г.

${\displaystyle \Gamma \vdash _{\mathrm {F} S}A}$

La conséquence syntaxique ne dépend pas d'une interprétation du système formel[6].

Un système formel ${\displaystyle {\mathcal {S}}}$ 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 ${\displaystyle {\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.

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.