L’axiomatisation est une opération par laquelle le logicien recherche dans une théorie quelconque des propositions primitives (postulats, axiomes), à partir desquelles les vérités de la théorie seront déductibles (on appelle alors ces vérités des théorèmes).
La formalisation est une opération par laquelle le logicien construit un système formel, c’est-à-dire un ensemble de signes et de règles explicites pour former un sous-ensemble des combinaisons de ces signes qu’il considère comme des « expressions bien formées », puis des règles de déduction à partir desquelles certaines expressions s’enchaînent.

Dans une perspective épistémologique, axiomatiser et formaliser sont des activités de l’intelligence qui n’apparaissent qu’à l’occasion d’un corps de connaissances déjà acquises. Celles-ci se présentent comme un ensemble c de propositions relatives à certains objets, propositions tirées de l’observation et de l’expérience ou reconnues vraies par des méthodes propres aux divers domaines de la science. Dans ces conditions, axiomatiser ou formaliser c, c’est procéder à une reconstruction du savoir acquis qui vise, d’une part, à systématiser les résultats et, d’autre part, à les assurer. Il est commode de distinguer trois niveaux dans ce genre d’élaboration.

Axiomatisation matérielle

Les propositions de c portent sur les diverses notions qui constituent le domaine de la connaissance en question : points, droites, triangles, etc., s’il s’agit de la géométrie ; phrases, syntagmes, verbes, etc., s’il s’agit de la linguistique, et ainsi de suite. Les notions de c ne sont, en général, pas toutes indépendantes les unes des autres, ce qui signifie que certaines d’entre elles peuvent se définir à l’aide des autres. Ainsi la notion de « triangle » peut se définir à partir de celles de « point », de « droite » et de « appartenir à » : un triangle est un objet géométrique formé par trois points qui n’appartiennent pas à une même droite. Axiomatiser c exige de commencer par dresser la liste exhaustive des notions, dites « notions primitives », qui permettront de définir toutes les autres.

D’une manière analogue, les propositions de c ne sont généralement pas toutes indépendantes les unes des autres, ce qui signifie que certaines peuvent se déduire d’autres. Ainsi la proposition « les angles du triangle ABC sont égaux » peut se déduire de la proposition « les côtés du triangle ABC sont égaux ». On appellera axiomes, ou encore propositions primitives, les propositions dont il est possible de déduire toutes les autres, lesquelles seront alors appelées des théorèmes.

L’ensemble N des notions primitives et l’ensemble A des propositions primitives, au sens ci-dessus, constituent une axiomatisation (matérielle) de c. Il faut souligner le fait qu’un même corps de connaissances peut être axiomatisé de diverses façons, c’est-à-dire qu’il est possible de trouver des ensembles de notions primitives N et N′ distincts, des ensembles d’axiomes A et A′ distincts et tels que la réunion de A et de l’ensemble des théorèmes qui en découlent soit identique à la réunion de A′ et de l’ensemble des théorèmes qui en découlent. Cela montre que les notions d’axiome (de proposition primitive) et de théorème sont relatives l’une à l’autre, plus généralement qu’elles sont relatives au système dans lequel elles figurent. Cette relativité n’empêche pas que, à ce niveau d’axiomatisation, axiomes et théorèmes puissent être dits « vrais ». Ils le sont en ce sens naïf qu’ils énoncent des propriétés des objets considérés, des relations entre ces objets et que celles-ci sont reconnues vraies par des méthodes qui ne relèvent pas de la logique. Les Éléments d’Euclide (iii^e s. av. J.-C.) offrent le premier exemple qui nous soit parvenu d’une axiomatisation matérielle d’un corps de connaissances.