formalisation

Cet article est extrait de l'ouvrage Larousse « Dictionnaire de la philosophie ».

Logique, Philosophie Cognitive

Opération visant à transformer une théorie axiomatique en système formel, et qui consiste (1) à spécifier un langage formel constitué d'un alphabet de symboles primitifs ainsi que de règles de formation permettant d'engendrer à l'aide de ces symboles un ensemble effectivement décidable d'expressions bien formées ; (2) à spécifier, parmi ces expressions, un ensemble décidable d'axiomes ainsi que des règles d'inférence permettant de définir rigoureusement la notion de démonstration dans le système formel considéré.

Alors que l'axiomatisation d'une théorie a pour effet de remplacer, au titre de « théorèmes primitifs », une classe plus ou moins déterminée d'énoncés « évidents » par une liste explicite d'axiomes, la formalisation a pour but de remplacer, au titre d' « inférences immédiates », une classe plus ou moins vague de transitions « intuitivement correctes » par un ensemble bien déterminé de règles qui permettent de conclure de certains énoncés à d'autres en vertu de leur seule forme. Ces règles d'inférence (par exemple le modus ponens, qui de A et de A → B autorise à conclure B) doivent être assez élémentaires pour qu'il soit toujours possible, une liste quelconque d'énoncés étant donnée, de déterminer mécaniquement, sans recourir à la signification éventuellement attribuée aux symboles, si le dernier énoncé de la liste découle ou non d'énoncés qui l'y précèdent en vertu de l'une de ces règles.

Frege, qui fut le premier à avoir mené à bien la formalisation complète d'une discipline, soulignait⁽¹⁾ l'intérêt philosophique de l'entreprise : c'est seulement lorsque l'« on résout les inférences en composants élémentaires » que l'on se trouve contraint d'expliciter sous forme d'axiomes toutes les hypothèses tacites d'un raisonnement, et que l'on peut alors identifier les « sources de connaissance » dont émane une science.

Jacques Dubucs

→ décidabilité, démonstration, effectivité