Système formel

Un système formel est une modélisation mathématique d'un langage en général spécialisé. Les éléments linguistiques, mots, phrases, discours, etc., sont représentés par des objets finis (entiers, suites, arbres ou graphes finis...). Le propre d'un système formel est que la correction au sens grammatical de ses éléments est vérifiable algorithmiquement, c'est-à-dire que ceux-ci forment un ensemble récursif. Les systèmes formels s'opposent aux langues naturelles pour lesquels les algorithmes de traitement sont extrêmement complexes et surtout doivent évoluer dans le temps pour s'adapter aux transformations du langage. Les systèmes formels sont apparus en logique mathématique afin de représenter mathématiquement le langage et le raisonnement mathématique, mais peuvent se trouver également dans d'autres contextes : informatique, chimie... Le calcul des prédicats, système logique modélisant le langage mathématique. Le lambda-calcul, langage de programmation théorique utilisé pour étudier les liens entre logique et informatique ; plus généralement tout langage de programmation est par définition un système formel. La théorie des ensembles, système formel dont les axiomes définissent la notion d'ensemble. La nomenclature des molécules organiques est un système formel. Logique mathématique#Système logiqueLogique mathématique Les systèmes formels ont été conçus par les logiciens afin de poser et étudier mathématiquement certains problèmes liés au langage mathématique. De ce point de vue on peut les considérer comme des métathéories générales, des théories sur les théories (mathématiques). Les systèmes logiques visant à modéliser le langage mathématique résolvent trois problèmes : Comment formalise-t-on les énoncés mathématiques (théorèmes, lemmes, définitions, etc.