Conditions de garde

Logique et preuves

Une façon de résumer la logique mathématique est de dire qu’elle est l’étude des formules. Cela est très vague et prend évidemment plusieurs directions possibles dont l’une d’entre elles, la théorie de la démonstration, concerne les façons d’obte-nir des formules à partir d’autres via des règles d’inférence et ce que cela signifie sémantiquement. Ce sujet est traité en détails dans (Girard, 2006) ou encore dans (David et al., 2004) et on ne fait ici qu’en brosser un portrait très sommaire afin d’établir des définitions appropriées pour nos besoins.
On suppose que l’ensemble F des formules est donné d’avance (on pourrait prendre, par exemple, les formules du premier ordre, avec les symboles logiques habituels : _, ^, !, :, 8 et 9). Un séquent simple est une expression formelle de la forme “A ‘ B”, où A; B 2 F. Le symbole ‘ représente l’implication logique, à un niveau métalinguistique (dit structurel). Autrement dit, A ‘ B n’est pas une formule et se lit « La formule A entraîne logiquement la formule B ». Les séquents simples sont les seuls qui seront considérés dans cette thèse, mais il faut savoir que la notion usuelle de séquent permet de placer plusieurs formules de chaque côté du
symbole ‘, modélisant ainsi la conjonction (à gauche) ou la disjonction (à droite) au niveau structurel. On dénote par SEQF l’ensemble des séquents sur F.
La barre horizontale représente une implication logique d’encore un niveau mé-talinguistique par rapport au niveau structurel. Par exemple, la règle R^ se lit comme suit : « Si la formule A entraîne logiquement la formule B et si la formule A entraîne logiquement la formule C, alors la formule A entraîne logiquement la formule B ^ C. »
Un système déductif est une paire S = hF; i où F est un ensemble de formules et est une signature, c’est-à-dire un ensemble de (noms de) règles d’inférence sur ces formules, avec une fonction d’arité ar : ! N. Les règles d’inférence sont alors les briques qui composent les preuves du système.
Définition. Une preuve dans un système S est un triplet = hG; Règ; Seqi où G est un graphe étiqueté déterministe sur l’alphabet N et Règ : G ! et Seq = (SeqL ‘ SeqR) : G ! SEQF sont deux fonctions de sorte que pour chaque u 2 G.
Le graphe G s’appelle le support de et sera dénoté j j. On se permettra également un léger abus de langage en écrivant u 2 pour signifier u 2 G. Enfin, on dit que est une preuve de A ‘ B s’il existe u 2 tel que Seq(u) = A ‘ B.
Fait à remarquer sur cette définition : les preuves, pour nous, sont des graphes quelconques et non pas spécifiquement des arbres finis comme c’est généralement le cas dans les systèmes déductifs usuels. Cela ne change, en pratique, rien pour un système comme LK car les règles sont conçues de façon à ce que les chemins infinis soient impossibles à cause de la syntaxe des formules. Ce ne sera pas le cas dans le système qu’on étudiera dans cette thèse, d’où la possibilité des preuves circulaires.
Il s’agit des systèmes déductifs. Un système déductif S engendre une catégorie S dont les objets sont les formules et les flèches f : A ! B sont les preuves du séquent A ‘ B,
En fait, dans (Lambek et Scott, 1988), cette famille d’exemples constitue la défi-nition des catégories. Notons que la propriété des éléments neutres est une règle d’élimination des coupures : elle permet de diminuer le nombre d’occurrences de la règle de coupure dans certaines preuves. On dit qu’un système déductif a la propriété d’élimination des coupures si chaque preuve est égale à une preuve qui n’utilise pas la règle de coupure.
Enfin, quant à la règle d’hypothèse (manquante dans le Tableau 3.2), elle peut sembler surpuissante car elle permet de prouver n’importe quel séquent directe-ment, mais il faut plutôt la voir comme un outil technique nous permettant de décomposer les preuves en morceaux. Les sommets marqués de la règle H consti-tuent des sortes de variables qu’on se permettra de substituer par n’importe quelle flèche déjà définie (pourvu qu’elle ait le bon domaine et le bon codomaine). L’in-terprétation des preuves circulaires dépendra donc de ces variables.

Exemples

Avant de faire les détails sur l’interprétation des preuves circulaires en général, il importe de faire quelques exemples qui illustrent de quelle façon on peut les uti-liser. Tous ces exemples vivent dans la catégorie des ensembles et les pré-preuves circulaires peuvent donc être vues comme des programmes qui dénotent des fonc-tions.
Exemple 1. Souvenons-nous du chapitre précédent que l’ensemble des nombres naturels est le support N de l’algèbre initiale du foncteur F (X) = 1 + X, avec la f0;sucg structure 1 + !N N. Pour décrire des fonctions numériques f : N ! N à l’aide des pré-preuves circulaires, il faut donc au moins se donner le système à une seule équation S = fN =1 1 + Ng, de façon à avoir JNK = N.