Logique et métaphysique de la connaissance

De
Publié par

En s'appuyant sur l'expression "métaphysique de la connaissance", les contributions présentées ici témoignent d'une volonté toujours renouvelée de comprendre et de connaître la connaissance. Comprendre la connaissance, comprendre la logique de la connaissance, comprendre la métaphysique de la connaissance et donc comprendre la relation de conjonction liant la "logique" à la "métaphysique de la connaissance", tel est le défi de ce second volume des Cahiers épistémo-logiques.
Publié le : mercredi 1 octobre 2014
Lecture(s) : 19
Tags :
EAN13 : 9782336357720
Nombre de pages : 254
Voir plus Voir moins
Cette publication est uniquement disponible à l'achat

2
Ce titre qui nomme le second volume des Cahiers épistémo-logiques est révélateur de
la complicité conceptuelle et épistémique que les contributeurs ont essayé de retrouver
et de reconstruire entre la « logique » et la « métaphysique de la connaissance ». Et pour
cause, en s’appuyant sur l’expression « métaphysique de la connaissance » en tant que
ce cadre théorico-épistémique de la logique de chercher à « toujours comprendre »,
les contributions ici présentées témoignent d’une volonté toujours renouvelée de
comprendre et de connaître la connaissance. Elles participent, de ce fait, d’une intention
qui a consisté à réactiver, si ce n’est à nourrir, une « métaphysique de la connaissance ».
Comprendre la connaissance, comprendre la logique de la connaissance, comprendre la Sous la direction demétaphysique de la connaissance – et donc, comprendre la relation de conjonction liant la
« logique » à la « métaphysique de la connaissance » –, tel est le dé dont le relèvement Charles Zacharie Bowao
est, par nature, toujours empreint d’une dimension métaphysique. et Marcel NguimbiC’est dans une telle logique ou philosophie de la logique qu’il convient de saisir le
rôle que Gildas Nzokou assigne aux règles structurelles dans le calcul des séquents ;
tout comme l’opposition que Shahid Rahman formule à l’encontre de l’opposition que
Perelman et Toulmin développent entre le raisonnement juridique et le raisonnement
logique ; ou encore l’argumentation dialogique de Marcel Nguimbi appliquée aux
concepts régulateurs du dialogue chez Popper. CAHIERS
C’est par ailleurs un tel élan de pensée métaphysique qui sous-tend l’argumentation
cognitive que Marina Phanie Mabouania articule autour de la question du continuisme ÉPISTÉMO-LOGIQUESet/ou du discontinuisme chez Bachelard ; ou même celle que Surprise Chéril Ngono
Mbéri déroule autour du concept d’épistémologie naturalisée chez Quine ; ou encore
celle qui fonde le soupçon qu’Edgar Mervin Martial Mba conçoit dans la conception
inavouée de la gnoséologie chez Popper ; ou même celle que Laurent Gankama trouve
au fondement de l’orientation pragmatiste qu’il conçoit dans les diverses applications de
la notion de vérité chez Popper et Habermas. C’est, à tout bien prendre, cette ambition Logique et Métaphysique
de métaphysique de la connaissance qu’Alexis Campaoré trouve sur le principe de
relation dans les recherches scienti ques ; que Michel Wilfrid Nzaba intellige lorsqu’il
cherche à comprendre si, avec Paul Karl Feyerabend, le normativisme est persistant de la connaissanceou pas; ou qui fonde l’anti-empirisme radical qu’Auguste Nsonsissa interprète chez
Quine à propos de la signi cation des énoncés d’observation; ou encore ce que Krishna
Amen Ndounia décèle dans les présupposés ontologiques du théorème de Pythagore
comme fondements de la dialectique entre la construction mythique du monde et le
déploiement rationnel de la pensée.
2 / 2014
Charles Zacharie Bowao est Professeur titulaire de philosophie (depuis 2006) et
coordonnateur de la formation doctorale de philosophie de la FLSH de l’UMNG de Brazzaville,
au Congo (depuis 2001).
Marcel Nguimbi est maître de conférences de philosophie (depuis 2012) et responsable
du master de philosophie au sein de la formation doctorale de philosophie de la FLSH de
l’UMNG de Brazzaville, au Congo.
25,50 €
ISBN : 978-2-343-04504-7
Logique et Métaphysique
Charles Zacharie Bowao et Marcel Nguimbi (dir.)
de la connaissance


































Logique et Métaphysique
de la connaissance





























Cahiers épistémo-logiques


Travaux de logique, d’épistémologie
et d’histoire des sciences

Studies in Logic, Epistemology and History of Sciences





Cahiers épistémo-logiques sont une Revue scientifique à comité de
lecture qui publie des travaux en Logique, en Epistémologie et en Histoire
des Sciences. Elle accueille notamment des études traitant de la logique, de
la philosophie et/ou de l’épistémologie de la logique, de la philosophie et/ou
de l’épistémologie des mathématiques, de la philosophie et/ou de
l’épistémologie de la physique, de la biologie, etc., tout en restant ouverte
aux travaux portant sur les autres disciplines scientifiques.


Revue périodique publiée par le Laboratoire de
Logique, Epistémologie et Histoire des Sciences
–Formation Doctorale de Philosophie–
Faculté des Lettres et des Sciences Humaines
Université Marien Ngouabi
B. P. : 2642, Brazzaville
République du Congo



© L’Harmattan, 2014
5-7, rue de l’Ecole-Polytechnique, 75005 Paris

http://www.harmattan.fr
diffusion.harmattan@wanadoo.fr

ISBN : 978-2-343-04504-7
EAN : 9782343045047

Sous la direction de
Charles Zacharie Bowao
et Marcel Nguimbi



Logique et Métaphysique
de la connaissance



Cahiers épistémo-logiques

Numéro 2, 2014












Directeur : Charles Zacharie Bowao

Rédacteur en chef : Marcel Nguimbi

Comité scientifique :
-Souleymane Bachir Diagne, Columbia University, USA
-Théophile Mwené Ndzalé Obenga, California University, USA et
Université Marien Ngouabi, Brazzaville, Congo
-Shahid Rahman, Université Charles-de-Gaulle Lille 3, UMR-CNRS
8163 STL, Lille, France
-Charles Zacharie Bowao, Université Marien Ngouabi, Brazzaville,
Congo
-Pierre Nzinzi, Université Omar Bongo, Libreville, Gabon
-Yaovi Akakpo, Université de Lomé, Togo
-Abel Kouvouama, Université de Pau et des Pays de l’Adour, France
-Ignace Ayenon Yapi, Université Alassane Ouattara de Bouaké, Côte
d’Ivoire
-Jean Chrysostome Kapumba Akenda, Université Catholique du
Congo, Kinshasa, République Démocratique du Congo
-Ramatoulaye Diagne Mbengue, Université Cheikh Anta Diop, Dakar,
Sénégal
-Emmanuel Malolo Dissakè, Université de Douala, Cameroun
-Jean Luc Aka Evy, Université Marien Ngouabi, Brazzaville, Congo
-André Patient Bokiba, Université Marien Ngouabi, Brazzaville,
Congo
-Jean Luc Dimi, Université Marien Ngouabi, Brazzaville, Congo
-Clobite Bouka Biona, Université Marien Ngouabi, Brazzaville,
Congo
-Charles Thomas Kounkou, Université Marien Ngouabi, Brazzaville,
Congo
-Jean Claude Bayakissa, Université Marien Ngouabi, Brazzaville,
Congo
-Omer Massoumou, Université Marien Ngouabi, Brazzaville, Congo

Comité éditorial :
Marcel Nguimbi, Auguste Nsonsissa, Evariste-Dupont Boboto, Didier
Ngalebaye, Laurent Gankama, Norbert Ampa (Université Marien
Ngouabi, Brazzaville, Congo) ; Mawusse Kpakpo Akue Adotevi,
Université de Lomé, Togo ; Gildas Nzokou, Université Omar Bongo,
Libreville, Gabon. Tout en remerciant les éditeurs et évaluateurs anonymes
pour leur évaluation et leurs précieux conseils,

Nous avons une pensée profonde pour notre Maître,
Monsieur le Professeur Oswald GATORE de qui
–pensons-nous–
L’Eternité a eu trop tôt raison.




























































Première Partie




Logique ou Philosophie de la logique



























Du rôle des règles structurelles
dans le calcul des séquents

Gildas NZOKOU
Faculté des Lettres et Sciences Humaines (FLSH)
Centre d’Études et de Recherches Philosophiques (CERP)
Université Omar Bongo, Libreville (Gabon)

Résumé
Dans cet essai nous présentons une interprétation renouvelée des
règles structurelles du calcul des séquents. Il est question de soutenir
précisément que les règles structurelles, non seulement expriment de
manière directe les propriétés remarquables de la conséquence logique,
mais surtout garantissent la consistance de la logique classique et celle de la
logique intuitionniste des prédicats. Par ailleurs, une compréhension plus
approfondie de ces règles –y incluant toutes les perspectives de lecture (top-
down, bottom-up, à gauche et à droite du séquent)– permet de voir
apparaître plus de propriétés remarquables telles que la compacité et la
clôture disjonctive ; toutes choses que la seule lecture standard de ces règles
ne laisse pas souvent apparaître.

Mots-clés
Consistance, opérateurs logiques, propriétés remarquables, règles de
particules, règles structurelles, séquent.

Introduction

Le système de logique qu’est le « calcul des séquents », présenté par
1Gerhard Gentzen en 1934/35, est une méthode de décision syntaxique,
c’est-à-dire une méthode relevant de l’approche preuve-théorétique de la
logique. Ce système fait partie, avec la méthode de « déduction naturelle »,
2des deux premiers systèmes formels (à une nuance près) non axiomatiques
fonctionnant essentiellement au moyen de quelques règles d’inférence ad

1 G. GENTZEN, « Untersuchungen über das logische Schliessen. » Mathematische
Zeitschrift, 1935, traduction anglaise sous le titre “Investigations into Logical Deduction”
dans M. Szabo; The Collected Papers of Gerhard Gentzen, Amsterdam, North-Holland, 1969,
pp. 68-131.
2 La nuance c’est qu’en dépit du fait que Gentzen ait cherché directement à atteindre un
système formel sans axiome, il se trouve que dans le calcul de séquents il y a un schéma
d’axiome qui sert de boucle à tout processus de preuve et qui fonde donc le caractère
tautologique d’une thèse donnée.
11
hoc qui internalisent le sens de chaque notion logique. Par ailleurs, le calcul
des séquents a la particularité d’être la première méthode véritablement
calculatoire en logique formelle, en tant qu’elle permet de transformer
n’importe quelle preuve en forme normale dite « forme canonique », et ce
par le truchement de l’élimination des coupures dans la structure des
preuves. Ce qui nous amène donc à reconsidérer le sens fonctionnel de ses
règles, et en particulier la règle de coupure.
Le but de cet essai est de montrer que la spécificité des règles du
calcul des séquents –en plus de la symétrie évidente et de la dualité de ces
dernières– réside d’abord dans leur capacité à implémenter de manière
directe les propriétés remarquables de la conséquence logique. Et ici, une
lecture féconde de ces règles (en particulier, les règles structurelles) doit
consister à utiliser toutes les perspectives, en incluant celle du bas vers le
haut des deux côtés du signe de séquent. D’ailleurs, le contraste apparaît vite
lorsqu’on compare ce calcul des séquents à d’autres systèmes de décision
syntaxiques tels que la déduction naturelle, où ces mêmes propriétés des
opérations logiques ne peuvent être mises en évidence qu’au terme d’un
processus de preuve. C’est qu’en principe, la déduction naturelle est un
système de construction des preuves formelles, alors que le calcul des
séquents est plutôt un système conçu pour abstraire les schémas des preuves
formelles. Il sera alors utile d’établir, à quelques endroits, un parallèle avec
3les développements de la « déduction naturelle » qui, comme le calcul des
séquents, est une méthode calculatoire de l’inférence logique.
Toutefois, le point le plus significatif du rôle des règles structurelles
du calcul des séquents demeure le fait que –entre autres propriétés
métathéoriques– ces dernières induisent la consistance de la logique
(classique et intuitionniste) des prédicats.

La notion de « séquent »

On appelle « séquent », un dispositif syntaxique de la forme ?' , où
et sont des ensembles finis de formules non-signées et qu’on nomme
des «contextes propositionnels » (ceux-ci peuvent être vides). On note de
manière usuelle comme suit : ⇒ , où nous lisons : « si tous les éléments
de sont vrais alors au moins un élément de est vrai ». Ce qui veut dire
que, sous une interprétation I quelconque (on parlera de valuation booléenne
si nous sommes en logique propositionnelle) qui rendrait vrais tous les
éléments de , cette même interprétation rendrait au moins un élément de
vrai. Et, si on prend = {X , …, X et = {Y , …, Y , l’on dira que sous 1 n 1 k

3 La déduction naturelle fut elle aussi présentée dans le volume des « Investigations into
Logical Deduction ».
12

'444`'4'4`''
4?I le séquent ⇒ a la même valeur de vérité que la formule ((X ʌ … ʌ X ) 1 n
(Y v … v Y )). Puis, nous disons qu’un séquent est une tautologie si ce 1 k
dernier est vrai sous toutes les interprétations.
Les suites de formules que sont X , …, X et Y , …, Y constituent les 1 n 1 k
« termes du séquent » et portent respectivement les appellations
d’antécédents et de succédents du séquent. Il est possible d’avoir une
écriture avec l’un des côtés du séquent ne comportant aucun symbole comme
suit : ⇒ , (ce qui sous-entend que ⇒ , ). Nous remarquerons que le
séquent ⇒ , est vrai sous toutes les interprétations.
De même on peut avoir : , ⇒ (ce qui sous-entend que , ⇒ ),
où le séquent est vrai si, et seulement si, au moins un des éléments de
l’antécédent est faux.
De ce qui précède, l’on donne une définition synthétique à la notion
de séquent comme étant un atome démonstratif. Un séquent est alors une
structure élémentaire de démonstration.

Des règles d’inférence

Le calcul des séquents fonctionne au moyen de trois groupes de règles
d’inférence : a) le groupe identité ; b) le groupe logique qui se compose des
règles d’introduction des connecteurs logiques ; enfin c) le groupe structurel
qui est constitué des règles structurelles. Les règles d’introduction des
connecteurs au nombre de huit (8), se présentent par sous-groupes de deux,
où l’on a une règle d’introduction à gauche et une autre à droite du séquent,
conservant ainsi la symétrie parfaite du système. Suivant la lecture [du bas
vers le haut ou du haut vers le bas] qu’on fait de ces règles, on les considère
soit comme des réponses quant à la procédure d’introduction/élimination de
ces connecteurs, soit comme des instructions concernant la procédure de
construction des preuves (lecture du bas vers le haut). De manière
informelle, on pourrait comprendre ces règles des connecteurs comme étant
des indications pratiques sur « comment utiliser certains types de formules
en tant qu’hypothèses d’un raisonnement » et aussi « comment une donnée
devrait être utilisée en tant que conclusion d’un raisonnement ».
Concernant les règles structurelles, l’on convient qu’elles ont pour but
principal de mettre en exergue les propriétés de la conséquence logique –
avec l’interprétation additionnelle que soutient le présent essai. Nous allons
présenter, en premier lieu, la version classique du calcul des séquents (notée
LK par Gentzen), ensuite nous verrons la version intuitionniste (LJ).
Généralement, il y a deux formes de présentation de chaque variante :
l’écriture uniforme, où l’on travaille avec des opérateurs multiplicatifs,
13

'44'o''44?4'4?'tandis que la seconde présentation met en exergue les opérateurs additifs.
Nous présenterons les deux formes notationnelles de toutes ces règles.
Il faut d’ailleurs considérer les règles d’inférence comme des briques
fondamentales qui permettent de construire des dérivations ; d’où le fait
corollaire de considérer les preuves comme des arbres dans lesquels les
règles jouent le rôle de nœuds et les formules axiomes –qui bouclent les
preuves– en sont les feuilles terminales.

1. Règles d’introduction des connecteurs multiplicatifs (ou groupe logique
multiplicatif).

1. a. Introduction à gauche du séquent :
, ⇒ Δ
------------ . ⇒ mult
, ⇒ Δ

, ⇒ Δ , ⇒ Δ
------------------? ⇒ mult
, ⇒ Δ

⇒ Δ, , ⇒ Δ
----------------- ⇒ mult
, ⇒ Δ

⇒ Δ,
---------- ⇒
, ⇒ Δ

, ⇒ Δ ⇒ Δ, ,
----------------- ⇒ mult
, ⇒ Δ

, [k ] ⇒ i
--------------------- ⇒
, x ⇒ (à condition que k n’apparaisse pas dans la conclusion du séquent) i

14

Ilo\I6I\\\\66?6\l??6\6)?)I6'\6o6'66\6?666
I
I
I
I
I
I
I1.b. Introduction à droite du séquent :

6 ⇒ Δ ⇒ Δ,
⇒ mult
6 ⇒ Δ ?\ I
⇒ Δ, ,
⇒ mult
6 ⇒ Δ ?\ I

, ⇒ Δ,
----------------------- ⇒ mult
⇒ Δ,

, ⇒ Δ
------------------ ⇒
⇒ Δ,
, ⇒ Δ, , ⇒ Δ,
-------------------------------- ⇒ mult
⇒ Δ,
------------------ ⇒
, x ⇒ Δ

⇒ Δ, [k ] i
----------------------- ⇒
⇒ Δ,
, [k ] ⇒ i
⇒ , [k ] i
-------------------- ⇒
⇒ , x
(à condition que le paramètre k n’apparaisse pas dans la conclusion). i

La présentation au moyen des connecteurs additifs ne varie d’avec la
précédente que sur les règles de conjonction à gauche du séquent et celle de
15

6)'I?6?'\)6?666)6I)66'Io\\IloI)l6I\\66\?I\666

I
I

disjonction à droite, de sorte qu’on se restreint à la seule présentation de ces
lieux de variance sur les règles.

1 ′. Groupe logique additif.

Règles d’introduction à gauche :

, ⇒ Δ , ⇒ Δ
----------------- et ---------------- g g
, ? ⇒ Δ , ? ⇒ Δ

Règles d’introduction à droite :

⇒ Δ, ⇒ Δ,
-------------- et -------------- d d
⇒ Δ, ?\ ⇒ Δ, ?

2. Règles structurelles

Cas de gauche

Weakening (ou Règle d’affaiblissement) :

------------ weak. ⇒
, ⇒

Contraction :
, , ⇒
----------------- Contr. ⇒
, ⇒

Interchange :

, , ⇒
------------------ Interch. ⇒
, , ⇒

16

44I**I6?646\6\\?I\II6I*\II4**4I??6\\III**4*Cas de droite
Weakening


------------ ⇒ weak.
⇒ ,

Contraction :
⇒ ,
----------------- ⇒ Contr.
⇒ ,

Interchange :
⇒ , ,
------------------ ⇒ Interch.
⇒ , ,


3. Groupe identité :

Cut (Règle de coupure): Axiome d’identité :

⇒ , , ⇒ ∏ Ax.
---------------------------------- ----------
, ⇒ , ∏ ⇒ (où est un atome propositionnel)

Remarque à propos de la syntaxe :

** Dans une écriture de séquent de type « , Δ ⇒ , ∏», la virgule à gauche
du séquent se lit comme un « et » –car elle traduit l’opération de réunion des
suites de propositions– tandis qu’une virgule à droite du séquent se lit
comme un « ou ».
Dans le calcul des séquents, on construit les preuves dans le sens
allant du bas vers le haut, c’est-à-dire allant de l’écriture du séquent qu’on
doit prouver jusqu’au schéma d’axiome qui boucle ladite preuve. Et, en plus
de voir les règles d’inférence comme des descriptions mettant en exergue les
processus de dérivations régulières, il faudrait également envisager ces
règles comme étant des sortes d’instructions sur comment construire une
17

DD4'I6I66I4'4I6446II6\I46D444I6\6preuve donnée. C’est ce que soulignent Fontaine et Redmond lorsqu’ils
écrivent que :

« Dans ce cas les règles peuvent être lues du bas-vers-le-haut. Par
exemple, la règle de conjonction à droite dit que, afin de prouver que
A B suit des hypothèses Σ et Δ, il suffit de prouver, respectivement,
que A peut être conclu à partir de Σ et que B peut être conclu à partir
4de Δ» .

Seule petite difficulté dans cette compréhension des règles
d’introduction des connecteurs, c’est que –pour un exemple tel que celui
concernant l’introduction du « ʌ»– dans le cas où l’on n’a qu’un seul
antécédent, l’on ne saurait avec assurance comment déterminer précisément
les contextes propositionnels et Δ. Toutefois, dans la mesure où
l’hypothèse est faite qui considère ces contextes propositionnels comme
étant de grandeur finie, il ressort immédiatement que toute preuve est
obtenue au terme d’un nombre d’étapes fini de raisonnement et ce de
manière combinatoire : ce qui est le comportement naturel de la théorie de la
preuve.
Maintenant, pour revenir au principal point de notre travail, c’est-à-
dire aux règles structurelles, il importe de rappeler brièvement
l’interprétation standard qui est faite de celles-ci, et ce, suivant la perspective
de lecture adoptée.

La lecture du haut vers le bas :

La règle du weakening (affaiblissement) permet d’ajouter une formule
quelconque à droite ou à gauche du séquent.
La règle de contraction permet de ne conserver qu’une seule
occurrence d’une formule qui en avait plusieurs dans un même côté du
séquent.
La règle d’interchange (ou échange, encore appelée : « règle de
permutation ») dit que l’ordre d’occurrence des prémisses et celui des
conséquences est sans pertinence dans une dérivation.
La règle de coupure fixe que : si une formule dérivée sert à son tour
de prémisse pour une autre dérivation, alors cette prémisse transitoire peut
être éliminée de sorte qu’on puisse unifier la dérivation en un seul segment
de preuve.


4 Matthieu FONTAINE & Juan REDMOND, Logique Dialogique. Méthodes et exercices,
King’s College Publications, London : Cahiers de Logique et d’Épistémologie, 2008, Partie
II. 6. 1 : « Calcul des séquents », p. 117.
18

6?La lecture du bas vers le haut (du séquent vers son schéma d’axiome):
Les règles d’affaiblissement autorisent l’élimination (à droite et à
gauche) de certaines formules considérées comme arbitraires, afin d’obtenir
le schéma d’axiome voulu. Ce qui voudrait dire autrement que dans une
dérivation certaines formules sont en fait redondantes.
Les règles de contraction permettent de dupliquer une formule
quelconque (à gauche ou à droite) du séquent. Ce qui veut dire que la
multiplicité d’occurrences d’une même formule est un fait normal.
La règle du cut (coupure) pose une difficulté. En effet, dans la lecture
du bas vers le haut, il faille supposer la formule de coupure, c’est-à-dire la
formule qui a été supprimée lorsqu’on introduisait la règle de coupure du
haut vers le bas. La lecture converse pose la difficulté de supposer avec
pertinence cette formule de coupure.
Gentzen conçut un théorème d’« Élimination des coupures », qui fixe
que la règle de coupure est une règle superflue dans le calcul des séquents.
Cette règle –appelée « Hauptzatz » par Gentzen– dit que toute preuve
utilisant la règle de coupure peut être transformée en une preuve du même
séquent n’utilisant pas la règle de coupure. Ceci conduit évidemment à
considérer les preuves sans coupures comme primitives et celles usant de la
règle du cut comme étant des schémas d’inférence simplement admissibles.
Et, bien que Gentzen ait rangé le cut parmi les règles structurelles, nous la
considérons comme une règle spéciale en raison du fait qu’elle est
foncièrement la règle de calcul du système des séquents.
Maintenant, et par ailleurs, à côté de cette lecture standard qui nous
semble quelque peu sommaire, nous allons exposer une lecture
complémentaire et approfondie de ces règles structurelles du calcul des
séquents en revenant particulièrement sur la compréhension que l’on doit
avoir de la règle de coupure.

Règles de structure et relation aux opérateurs logiques standards

Comme précédemment annoncé dans notre introduction, nous
considérons une interprétation, non pas alternative (de l’interprétation
standard) mais simplement complémentaire et plus explicative des règles
structurelles.

1. a. Règle de contraction à gauche du séquent :

, , ⇒
----------------- Contr. ⇒
, ⇒
19

I6I44I6Cette règle met en exergue la propriété d’idempotence du produit
logique, c’est-à-dire que : ʌ ≡
Et on lit la contraction à gauche comme suit : « si dans une dérivation
l’on a plusieurs occurrences d’une prémisse, alors l’on peut obtenir la même
dérivation en ayant exactement une seule occurrence de ladite prémisse ».

1. b. Contraction à droite du séquent :

⇒ ,
----------------- ⇒ Contr.
⇒ ,

Cette règle exprime l’idempotence de la somme logique ; c’est-à-dire :
≡ I

Nous traduisons cette règle comme disant que : « dans une dérivation,
plusieurs occurrences d’une même alternative/conclusion n’en valent qu’une
seule ».

2. a. Permutation (Interchange) à gauche du séquent :

, , ⇒
------------------ Interch. ⇒
, , ⇒

Cette règle exprime la commutativité du produit logique, ce que l’on
note :
ʌ ≡ ʌ

La présente règle dit que « l’ordre d’occurrence des prémisses dans
5une dérivation importe peu » .

2 b. Permutation à droite du séquent :

⇒ , ,
------------------ ⇒ Interch.
⇒ , ,

5 Ceci est très différent de la pratique dans la déduction naturelle où l’ordre d’occurrence des
prémisses est déterminant dans la construction d’une preuve.
20

6\I6?4\6I4I\I\\II4I6\46I446I
I
I
I
IIci, c’est la commutativité de la somme logique qui est mise en
exergue par cette règle ; ce que l’on note comme suit :


Cette règle de l’échange à droite du séquent dit, au passage, que
« dans une dérivation, l’ordre d’occurrence des conclusions est sans
pertinence particulière ».

Nous abordons maintenant la règle d’affaiblissement qui mérite d’être
éclairée, en la considérant tant des deux côtés du séquent qu’à partir des
deux perspectives de lecture (bas en haut et haut en bas).

3. a. Weakening (affaiblissement) à gauche du séquent :


------------ weak. ⇒
, ⇒

En pratiquant une lecture de haut en bas (top-down), la règle
d’affaiblissement à gauche exprime clairement la propriété de monotonicité
+de la conséquence classique qui fixe que : Si ⊢ , alors { ⊢ avec
une quelconque ebf de LP ou de F-O).

Autrement dit, « l’ajout d’éléments à l’ensemble des prémisses
n’altère en rien une dérivation antérieurement effectuée ».

La lecture du bas vers le haut (bottom-up) nous fait considérer la règle
d’affaiblissement à gauche du séquent comme étant une implémentation
d’une variante de la propriété de compacité via la déductibilité.

Cette dernière fixe que : si ⊢ , alors il existe un sous-ensemble fini
′ ⊆ tel que ′ ⊢ . Ce qui veut dire que « si une dérivation est effectuée,
c’est que cette même dérivation peut être faite à partir d’un ensemble fini de
prémisses. (En somme, toute dérivation s’effectue toujours à partir d’un
ensemble fini de prémisses) ».
3 b. Weakening à droite du séquent :

------------ ⇒ weak.
⇒ ,
21

*I646?*6\\*4I*4?I*\I6II4*
I \`
ILa perspective de haut en bas exprime la clôture de la conséquence
classique sous la disjonction, au sens où : si ⊢ , alors on a ⊢ ,
(avec étant une ebf quelconque). Autrement dit : « si l’on a dérivé une
formule donnée, on peut dériver n’importe quelle disjonction comportant
cette formule comme étant l’une de ses composantes ».

La perspective du bas vers le haut expose les conditionnalités pour la
dérivation d’une disjonction en tant que conclusion d’un raisonnement. La
règle d’affaiblissement à droite du séquent, lue de bas en haut, pose que : « si
une disjonction est dérivée comme conséquence d’un ensemble de prémisses,
alors l’un ou l’autre des disjoints peut être dérivé comme conséquence à
partir des mêmes prémisses ». Autrement dit, la condition pour la dérivation
d’une disjonction revient à la dérivation d’au moins l’un des disjoints.
Une compréhension basique de cette règle à partir de la perspective
“bottom-up” serait de la voir comme la converse de l’opération de clôture
sous la disjonction. Maintenant, nous allons discuter de l’énigmatique règle
de coupure.

Cut (Règle de coupure):

⇒ , , ⇒ ∏
----------------------------------
, ⇒ , ∏

La lecture standard de la règle de coupure dans le sens « top-down »
(du haut vers le bas) dit que : « si une formule est dérivée et que cette
dernière sert de prémisse dans une autre dérivation, alors on peut supprimer
cette formule de sorte à raccourcir la dérivation en une seule étape ». La
formule qu’on supprime est appelée « formule de coupure ».
La lecture du bas vers le haut (bottom-up) fait apparaître la difficulté
qui consiste à supposer la formule de coupure alors que cette dernière n’a
aucune occurrence au premier niveau de la dérivation (i.e. en dessous de la
barre de dérivation). Cette difficulté, de notre point de vue, n’est que
d’apparence puisqu’il suffit de supposer une conséquence de qui, associée
à Δ, permet de déduire ∏.
Mais avant toute chose, l’approfondissement de notre compréhension
de cette règle doit commencer par nous la faire voir comme une sorte de
généralisation du Modus Ponens. On peut également la voir comme une
sorte d’utilisation d’un lemme, c’est-à-dire l’utilisation d’un théorème
transitoire ou intermédiaire, dans un processus d’inférence. Au passage,
22

'64II6'\I*6*\4
I?rappelons-nous de la propriété de la sous-formule caractéristique de toutes
les autres règles mais qui manque à la règle de coupure.
De fait, les formules au-dessus de la ligne de dérivation (i.e. les
formules du séquent-prémisses) sont toutes des sous-formules des formules
qui se trouvent en-dessous de la ligne de dérivation (i.e. les formules du
séquent-conclusion). Seule la règle de coupure –où la formule de coupure
n’apparaît pas dans l’écriture en dessous de la ligne de dérivation– manque
de cette propriété dite de « la sous-formule ». Ce qui suppose un détour via
une formule certainement plus complexe que la formule de coupure elle-
même. D’où la question la plus pertinente revient à se demander : sous
quelles conditions pourrait-on exécuter des dérivations sans utilisation de
cette règle de coupure ?
Ce qui précède nous conduit à considérer que la compréhension la
plus naturelle de la perspective bottom-up consiste à lire cette règle à partir
du « théorème d’élimination des coupures » qui constitue, au passage, l’un
des résultats les plus significatifs que Gentzen ait atteints. À ce propos,
plusieurs versions de ce théorème ont été données, qui toutes ont leurs
avantages et désavantages d’un point de vue pratique. Mais la traduction
globale pose que : « si une preuve de séquents est faite en usant de la règle
de coupure, alors on peut trouver une preuve pour le même séquent sans
usage de la coupure ».
Donnée comme telle, l’élimination de la coupure ne semble
apparemment pas traduire la lecture de bas en haut du cut. Mais, si nous
6considérons la version de Per Martin-Löf , où il conçoit conversement
l’élimination comme étant une sorte d’admissibilité de la coupure, on
7présente alors les choses comme dans Herbelin [1995] :
Si les séquents ⊢ Δ , A et , A ⊢ Δ sont prouvables sans coupure, 1 1 2 2
alors le séquent , ⊢ Δ , Δ est prouvable sans coupure. 1 2 1 2
En somme, nous lisons la règle du cut d’après la perspective bottom-
up comme suit : « Si l’on prouve le séquent , ⇒ , ∏, alors on peut
simultanément prouver les séquents ⇒ , et , ⇒ ∏ », où est une
efb quelconque de LP ou F-O, qui est telle que Δ ⊢ ∏.
Nous arrivons alors au point crucial de notre analyse qui vise à
montrer la réelle spécificité des règles du calcul des séquents : celle de
garantir la consistance tant de la logique classique que de celle intuitionniste.

6 Per MARTIN-LÖF, Notes on constructive mathematics, Almqvist & Wiksell, Stockholm,
1968, §30.
7 Hugo HERBELIN, Séquents qu’on calcule. De l’interprétation du calcul des séquents
comme calcul de λ-termes et comme calcul de stratégies gagnantes, Thèse de Doctorat en
Informatique fondamentale, Université Paris 7, 1995, 127 pages.
23

I'I6**'4*6*`?4
^I
IDe fait, le théorème d’élimination des coupures –en établissant qu’à chaque
preuve de séquent usant du cut on peut associer une dérivation sans usage de
coupures– garantit à chaque preuve de la méthode des séquents l’effectivité
de la propriété de la sous-formule. De-là, il devient impossible de dériver un
séquent vide (i.e. une conclusion contradictoire, du type « ?D »), étant
donné que dans une telle dérivation le séquent-prémisse devrait avoir toutes
les sous-formules du séquent-conclusion, ce qui est impossible.

Version intuitionniste du calcul des séquents L. J. : complément de
présentation

Ici, nous présentons la version intuitionniste en en précisant les lieux
d’écart d’avec la version classique. L’absence, dans le groupe structurel, des
règles de contraction et de permutation (interchange) à droite du séquent,
nous donne des indications précises sur l’articulation idéologique de l’école
intuitionniste.

Calcul des séquents intuitionniste
La version intuitionniste du calcul des séquents s’obtient à partir du
calcul classique, en imposant la restriction suivant laquelle il ne doit
apparaître qu’une seule formule à droite du signe de séquent. Chaque
séquent doit alors avoir la forme suivante : , …, ou , …, 1 n 1 n
Ceci a une incidence profonde sur les capacités de production des
preuves pour le système. Certaines formules qui sont prouvables dans le
calcul classique deviennent non prouvables en calcul intuitionniste en raison
justement de cette restriction sur la présentation des règles. Ainsi, nous
avons la règle d’introduction du « » à droite qui disparaît pour laisser place
à une double-règle, ce qui naturellement nous fait perdre la symétrie que
nous avions en version classique entre la disjonction et la conjonction. De
même, comme nous le verrons ci-dessous, l’introduction de la négation à
gauche et à droite du séquent fait maintenant intervenir « » étant donné
que cet opérateur est défini comme suit : ¬ = . Voyons alors Def.
précisément comment se présentent ces règles :

a- Le groupe logique :

Introduction à gauche :

, ⇒ Δ , ⇒ Δ
add add -------------- ʌ L -------------- ʌ L 1 2
, ʌ ⇒ Δ , ʌ ⇒ Δ
24

AoI*IDII*\I*A\I??IA\\?I*I?

Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.