SYSTÈME FORMEL

plètes sont appelées propositions, le point de départ les axiomes, le processus de déduction, une démonstration : effectuée, elle donne une sorte de dessin à ramifications convergentes « les fils de démonstrations * (HILBERT), composés chacun d’une suite de propositions entre lesquelles le passage s’effectue par application d’une règle ; il y a réunion de plusieurs fils, lorsque la règle exige la présence simultanée de plusieurs propositions. Il faut évidemment que fils et dessins entiers puissent être dominés par la pensée finie (1). Grâce à la règle de substitution on obtient cependant une extension infinie de systèmes : elle détermine dans les formules complètes une partie mobile, les signes appelés variables qui peuvent être remplacés par des signes ou formules d’une catégorie déterminée. On l’évite parfois en écrivant au lieu d’axiomes de simples schémas avec des vides remplissables de façon analogue.

Pour présenter un intérêt un système formel doit posséder une sorte de fermeture qui peut se manifester de deux façons différentes, indépendantes mais conjuguées : d’une part, toute formule complète du système ne doit pas y être démontrable ; d'autre part impossibilité d’ajouter au départ une nouvelle formule complète non démontrable sans que toute formule complète devienne démontrable (2). La défnition précise — et l'établissement — de ces deux propriétés

(x) TaRSKkI distingue parmi les systèmes déductifs les systèmes axiomatisables c'est-à-dire comportant un départ fini : il semble que cette distinction soit rendue vaine par la règle de substitution. On peut sans doute concevoir des systèmes à départ irréductiblement infini (c’est-à-dire ne pouvant être fixé en un nombre fini de schémas) : leur considération semble dépourvue de tout intérêt.

(2) Tarskr définit ainsi cette propriété : tout système déductif contenant le système considéré coïncide ou bien avec lui ou bien avec le système de toutes les propositions complètes (la méthode de TARSKtI exclut la notion d'extension successive). Il introduit aussi la notion de système ivréductible, tel que tout sous-système coïncide avec lui ou avec le calcul logique, intersection commune de tous les systèmes déductifs.