Calcul des séquents

Et j'ajoute que le signe "équivalent" ne devrait jamais être utilisé dans ce genre de chapitre car il embouteille contradictoirement les polarités***.

Et pour finir, ces règles embouteillent sans le dire les contractions. Normalement (par exemple):

$$ \frac{(L\vdash A)+(M;B\vdash N)}{L;M;(A\to \vdash N} $$

est plus honnête et si $L=M$, on peut par une série de :

$$ \frac{L;X;X\vdash M}{L;X\vdash M}$$

récupérer ce qu'il raconte.

J'ai mis les négatives en rouge et les positives en vert. Le signe $\iff$ n'écrit qu'une fois la lettre $A$ qui perd donc sa polarité.

Et ce n'est pas tout :-D , les droits de poubelle (ie $A\to (B\to A)$, ils sont où ?

Pour moi, c'est un drôle de système LK :-D

Bon cela dit, j'ai peu de temps, mais je te donne un "tuyau" psy.

Ta règle $g$ te dit que si tu disposes d'une fonction $f$ qui t'envoie $E\to (A\to (B\to F))$ dans $G$, alors tu disposes d'une fonction $g$ qui enverra $E\to ((A\times \to F$ dans $G$, et je pense que tu devines laquelle.

Ta règle $d$ te dit que si tu as deux objets $a,b$ alors à partir d'eux, tu as le couple $(a,b)$.

Mais dans ce cas, pourquoi ne pas le dire franchement? en outre, il se trompe assez gravement à cause de ses contractions non assumées. Dans le premier cas, c'est le produit tensoriel, comme tu peux le voir en passant de :

$$L(E, L(A,L(B,F)))$$

dans

$$L(E, L((A\otimes ,F))$$

de manière naturelle.

Ca c'est pour g. Hélas, pour $d$, comme il fait une contraction, il t'envoie $E\times F$ dans $E\oplus F$ et non pas dans $E\otimes F$.

Donc il se mélange les pinceaux.

Par contre, il "est vrai" que dans les 2 situation g, comme d, tu as la curryfication et la décurryfication de l'argument de la fonction supposée déjà gagnée:

$$ \phi \to [f\mapsto \phi ( [x\mapsto (y\mapsto f(x,y)] )] $$

et dans l'autre sens

$$ \phi \to [f\mapsto \phi ( (x,y)\mapsto f(x)(y) ) ] )] $$

Je me déconnecte, précision: $L(X,Y)$ (notation que j'ai utilisée) signifie espace des applications linéaires de $X$ dans $Y$.

Titi le curieux a écrit:

parce que si la déduction de ce truc comme règle dérivée dans le système que j'utilise me paraît évidente (parce que je me suis habitué à ce système), je me suis emmêlé les pinceaux lorsque j'ai essayé de déduire le modus ponens de ce truc (ben ouais, l'intuition, c'est beaucoup composée d'habitude...).

Si ce système ressemble au calcul des séquents, il est possible que la preuve du modus ponens passe par une version adaptée du théorème d'élimination des coupures (google vite!) or celui-ci n'est pas trivial (récurrence sur taille de la preuve et de la formule sur laquelle est appliquée la dernière règle).

@Titi le curieux, $A_1,...,A_n \vdash B_1,...,B_m$ exprime que "si tous les énoncés $A_1,..,A_n$ sont vrais alors au moins un des énoncés $B_1,...,B_m$" est vrai (bref on prouve $[A_1 \wedge A_2 \wedge ...\wedge A_n] \Rightarrow [B_1 \vee B_2 \vee ... \vee B_m]$). Les règles du calcul des séquents sont élaborées dans ce but.
Traditionnellement, dans la littérature française, $\Gamma$ (G) désigne la liste de gauche, $\Delta$ (D) celle de droite.

Le vdash est superfétatoire de toute façon. Il s'agit d'une liste.

C'est comme en programmation: pas besoin de fonctions, les procédures suffisent, tu leur passes en paramètres supplémentaires les @variables si besoin. Exemple plus(e,s,@z) mettra dans z la somme des valeurs présentes dans e,s.

Si tu as compris le dernier message de Christophe, tant mieux pour toi. ;-) Moi, pas.

Un petit point à propos du $\Delta$. Sa présence, plus exactement le fait qu'on autorise plus d'une formule dans la partie droite du séquent, est le point crucial de la différence entre logique intuitionniste et logique classique, dans le formalisme des séquents.
$$\begin{array}{rcl}
\hline
A&\vdash& A\\
\hline
&\vdash& \neg A,\;A\\
\hline
&\vdash&\neg A \vee A
\end{array}$$est une déduction du tiers exclus bannie en calcul des séquents intuitionniste parce qu'il y a deux formules à droite dans le deuxième séquent. Le calcul intuitionniste n'autorise qu'au plus une formule à droite du séquent.

D'accord, tu remplaces le $\vdash$ par un @ devant toutes les formules qui sont à droite et tu dis que ça montre que le $\vdash$ est superfétatoire.
Je ne suis pas très convaincu.

Je suis sur un pc wifi, mais hélas je n'ai pas de souris (je l'ai oubliée, n'ai pris que mon clavier), donc je vais être un peu approximatif.

Pour ce qui concerne les preuves de maths, il semble le plus utile et naturel de comprendre qu'on n'a que des procédures (elles ne retournent pas de résultat, mais "agissent")

Dans le cas précis des maths, en fait, elles n'agissent pas, elles mènent directement au paradis.

En d'autres termes, une preuve de maths est un chemin qui dit comment aller au paradis (que je vais noter $\perp$) à partir de certaines ressrouces (ou en partant de certains endroits)

On peut donc voir une procédure comme une FONCTION à valeurs dans $\perp$, avec une liste d'arguments.

C'est une des raisons pour lesquelles il faut atteindre des logiques très faibles pour renoncer à l'axiome $\perp \to Tout$, qui en gros dit, "si je suis au paradis alors je suis tout-puissant".

On retrouve là d'ailleurs un "fondement psychanalytique" de la confusion entre bonheur et puissance. Il est validé par TROIS des quatre logiques célèbres, seule la plus faible, la linéaire ne le validant pas, et j'ajoute, que sa manière de NE PAS le valider a une nature qui reste extrêmement timide puisqu'il s'agit juste de se retreindre aux applications linéaires PARMI les applications affines, autrement dit, de "pas bouger le zéro" (on eût pu rêver moins timide comme renoncement à "pouvoir = bonheur")

Le calcul des séquents peut donc à bon droit être vu comme signalant comment à partir de procédures déjà acquises, on en obtient de nouvelles.

Mais il ne faut rien cacher sous le tapis (la TQuantique nous a puni d'avoir oublié d'expliciter certains principes)

Par exemple, d'une <<Function (a,b: X; var Z:Balneo)>>, prétendre qu'on saura en fabriquer une
<<Function (a: X; var Z:balneo)>>

est tout sauf un acte inoffensif

La présence du vdash représente une séparation (artificielle) entre les mémoires dont on dipose de la valeur (accessibles en lecture) et les mémoires dont on dispose de l'adresse (accès en écriture)

Ce n'est qu'une métaphore (qui a sa valeur) car le paradis devient alors le fait d'avoir acès en lecture et écriture à une même mémoire, et donc l'aspect paradisaique est caché dans cette métaphore partielle

La "GROSSE REGLE" de la science (l'abstraction), réalisée par le fait que disposer de:

<<FunctionToParadise Toto(a: A; @b:B; paramsAutres)>>

permet, au prix d'une "petite" manipulation TOUJOURS POSSIBLE! DE DISPOSER DE

<<FunctionToParadise Bibi(f: @(A=&gt;B); parmaAutres)>>

provient de ce que vous pourrez écrire dans la mémoire $f$ la VALEUR:

$$Bibi: a \mapsto Toto (a,b,etcetc) $$

Je laisse les lecteurs "deviner l'intendance" qui fait suite à ces remarques.

Exercice: prouve A ou (A =>

Exercice: prouve A ou (A =>

Même preuve que $A\vee \neg A$.

Oups GBZM tu te tirer u e balle dans le pied je l'ai mis justement pour titi pour voir s'il avait vu que le "non" n'y est pour rien :-D. Bof c'est pas grave mais si tu as le temps tu px ptet mettre en blanc sur blanc?

En logique classique supposer un truc dans l'avenir fait gagner le prouveur même aux dates du passé où il devait prouver ce truc supposé.

@Christophe c: Déjà fait, il y a un bout de temps, c'est une tentative pour me convertir à l'intuitionnisme?

Comme le dit GaBuZoMeu, vu ce qu'on a déjà dit, il ne reste plus qu'à faire cela: $A,\neg A \vdash \bot$ donc $A,\neg A \vdash B$ et du coup $\neg A \vdash A\rightarrow B$, je sais faire, et ça ne me dérange pas plus que ça, parce que j'utilise la notion d'implication de manière très pragmatique (je suis une grosse buse en philo, je ne cherche pas à mettre du sens partout, la mécanique me convient mieux).
Du coup, pour l'intuitionnisme, c'est nope! Et quant aux histoires de d'INTU de CLASS et de temps, je ne sais pas de quoi il s'agit (ne cherche surtout pas pas à m'expliquer, ça me gonfle, j'ai un système qui fait l'affaire, j'en suis très content!).
J'ai peut-être un peu trop parlé de moi, on commence à être très très loin du sujet, là, je fais une tentative:

@Beauget, le système proposé par ton prof est juste pas classique, mais si il y a des règles surnuméraires dedans, le mieux est probablement de se débarrasser des "règles d'équivalences" c'est pas parce qu'un symbole est pratique qu'on a besoin de règles redondantes pour le définir. Désolé, je n'avais lu que très rapidement ta réponse à Maxtimax et j'étais passé à côté de la pièce-jointe.

@foys ce qui est chouette c'est que ça ne donne que des tautologies quand même. Pas "tout".

$$\begin{array}{rcl}
\hline
A&\vdash& A\\
\hline
A&\vdash& A,\;B\\
\hline
&\vdash& A,\;A\Rightarrow B\\
\hline
&\vdash&A \vee (A\Rightarrow
\end{array}$$

@titi: la signification derrière c'est AVANT TOUT le fait de déduire une contradiction de la liste des machins. Quand s sont à droite c'est leur négation qui est supposée c'est tout. C'est en cela que le vdash est superfétatoire. Ici de l'axiome À et non À tu contrededuis** (droit de poubelle)

À et non À et non B

puis passe à À et non (À=>B)

Bon :-X contre mon téléphone obsede par les accents juste quand j'en veux pas. Je me déconnecte!

** sens inverse de déduire disons. Faut mettre "non" devant.

@titi : la tradition est le tutoiement. J'essaierai de me rappeler qu'il ne faudra plus que je t'aide puisque ça te déplaît. Et tu as des ressentis étonnants. Je ne vois pas comment tu peux parvenir à ressentir des piques lancées (à GBZM si je te comprends) ans ce que j'ai raconté.

Mon objectif était de "combattre" le préjugé qui veut voir de grosses différences entre INTU et CLASS, particulièrement en exhibant le théorème CLASSE: [A ou (A=>B)]

C'est une approche erronée. Car il ne s'agit pas du tout du même "ou".

le "ou" de CLASS est un opérateur PARFAITEMENT définissable même si peu utilisé dans INTU, c'est:

$$ (x,y)\mapsto non(non(x)\ et\ non(y))$$

Je me détends (après ces vacances et retours tumultueux et surtout coûteux, en redonnant les différentes logiques (avec le même code latex). Les lettres grecques représentent des listes quelconques de phrases. $$

\begin{array}{rcl}
\hline \\

A\vdash A \\

\end{array}

$$ est l'axiome de toutes les logiques.
Les règles suivantes, que l'on pourrait appeler "commutativité" sont aussi utilisées par toutes les logiques. $$

\begin{array}{rcl}

\Gamma; A;B; \Delta \vdash \Psi \\

\hline \\

\Gamma;B;A; \Delta \vdash \Psi \\

\end{array}

$$
Voici une règle PROFONDE que j'appelle "l'abstraction" : $$

\begin{array}{rcl}

\Gamma; A \vdash B; \Psi \\

\hline \\

\Gamma \vdash (A\to ; \Psi \\

\end{array}

$$
La suivante est un modus ponens "assumé" : $$

\begin{array}{rcl}

\Gamma \vdash A; \Psi & + & \Gamma \vdash (B\to C); \Delta \\

\hline \\

&\Gamma ; (A\to \vdash C; \Delta; \Psi

\end{array}

$$
Mais la plupart du temps elle n'est utilisée qu'avec $A=B$, sous la forme : $$

\begin{array}{rcl}

\Gamma \vdash A; \Psi & + & \Gamma \vdash (A\to C); \Delta \\

\hline \\

&\Gamma ; (A\to A) \vdash C; \Delta; \Psi

\end{array}

$$ Et les gens écrivent en encre blanche sur papier blanc le $(A\to A)$ de gauche. Mais c'est problématique car dans un programme, les phrases apparaissent sous forme de pointeur, et la vérification que $A=A$ est une chose ultracomplexe (pour les phrases contenant des cycles par exemple).

On peut donc, pour "bien faire" ajouter la règle : $$

\begin{array}{rcl}

\Gamma; A\to A & \vdash \Psi \\

\hline \\

\Gamma & \vdash \Psi\\

\end{array}

$$ qui fournit un caractère assumé au modus ponens qui NE PEUT PAS être informatiquement implémenté. ainsi on appelle une procédure qui vérifie "A=A".
*Viennent enfin les quatre dernières règles : $$

\begin{array}{rcl}

\neg A ; \Gamma \vdash \Psi \\

\hline \\

\Gamma \vdash A; \Psi \\

\end{array}

\qquad\text{ ainsi que }\qquad

\begin{array}{rcl}

\Gamma \vdash \neg A; \Psi \\

\hline \\

\Gamma; A \vdash \Psi \\

\end{array}

$$ ainsi que $$

\begin{array}{rcl}

A ; \Gamma \vdash \Psi \\

\hline \\

\Gamma \vdash \neg A; \Psi \\

\end{array}

\qquad\text{ ainsi que }\qquad

\begin{array}{rcl}

\Gamma \vdash A; \Psi \\

\hline \\

\Gamma; \neg A \vdash \Psi \\

\end{array}

$$ Avec ça, on a le CŒUR ACTIF des raisonnements scientifiques (je vous laisse trouver les redondances). Je recommande d'ajouter explicitement, non pas sous forme de règles, mais sous forme d'axiomes, les 5 gros:

1/ $A\to (B\to A)$
2/ $(A\to (A\to ) \to (A\to $
3/ $(\neg A) \to (A\to \perp)$
4/ 3/ $(A\to \perp)\to (\neg A) $
5/ $\perp \to A$

Bon en espérant avoir apporté quelque chose à d'autres que moi-même, à qui j'ai apporté d'utiliser avec un peu de courage "begin array"

Ce sont les 4 dernières règles qui font disparaître l'utilité du vdash, puisqu'on peut tout mettre du côté qu'on veut.
Et merci GBZM, je t'ai volé le latex ;-) mais ce n'est pas encore "de la grande présentation". (J'ai quand-même fait l'effort de mettre un roman correct, enfin j'espère).

Pour ne pas proposer un produit "avec tout à deviner", je précise juste comment "retrouver ses petits" par rapport aux systèmes habituels.

1/ Vous voulez faire une modus ponens (les listes seront notées avec des lettres majuscules à partir de "L"):

$$ \begin{array}{ccc}

& L_1\vdash A; M & + & L_2\vdash (A\to ;N\\

\hline \\

& L_1;L_2; (A\to A)\vdash B;M;N\\

\hline \\

& L_1;L_2\vdash B;M;N

\end{array} $$

2/ Vous voulez permuter les hypothèses: bé, je rappelle que les transpositions $(n\ n+1)$ engendrent le groupe symétrique concerné

3/ Vous voulez faire une contraction:

$$ \begin{array}{ccc}

& L;A;A\vdash B;M\\

\hline \\

& L\vdash (A\to (A\to )\to (A\to ;M & + & L\vdash (A\to (A\to );M \\

\hline \\

& L'\vdash (A\to ; M \\

\hline \\

& L'\vdash (A\to ; M & + & A\vdash A \\

\hline \\

& L';A\vdash B;M \\

\end{array} $$

en abrégeant par $L'$ la liste $L;(A\to (A\to )\to (A\to $

4/ Vous souhaitez jeter une hypothèse:

$$ \begin{array}{ccc}

& L\vdash B;M\\

\hline \\

& L\vdash A;M & + & A\to (B\to A) \vdash A\to (B\to A) \\


\hline \\

& L; A\to (B\to A) \vdash (B\to A) ; M\\

\end{array} $$

On peut remarquer qu'on a éternellement une sorte de retour des mêmes problématiques, qui vont du CP jusqu'au niveau de la recherche. Par exemple, dans ce que je décris, on a une mise en blanc de certains axiomes et non pas une disparition. De la même manière, en cinquième, on a une mise en blanc de certaines parenthèses toujours présentes et non, comme le disent manuels et mouvement pédago un "retrait des parenthèses".

Au CE1, le symbole $\forall$ est mis en blanc dans $\forall a,b: a\times b = b\times a$

En bref, nous avons une matière (ou un domaine assez fascinant) par sa conservation des éternels écueils. Je m'émerveille de "me disputer" avec des gens qui refusent d'écrire le $\forall$ au CE1 (même en blanc), refusent la présence des parenthèses en 5ième, et ... ont décidé de "fondre dans les règles des axiomes parmi les plus offensifs des maths (ce sont eux qui leur donnent leur indécidabilité).

Bon évidemment, je ne dis pas ça très sérieusement, car les règles logiques sont parfaitement explicites et on n'a rien qui soit camouflé, à part peut-être le modus ponens, mais c'est une erreur involontaire et excusable due à l'absence de prise de conscience qu'à un moment ou un autre, dans un traitement industriel, il est TOTALEMENT exclus de revendiquer que le jeu de pointeurs de l'implémentation des phrases soit "par miracle" sans cycle. On peut même dire qu'il FAUT des cycles. En effet, c'est un "vrai égal physique" qu'il FAUT voir dans

$$(u\in \{x\mid x\notin x\}) = (u\notin u)$$

Si on ne veut pas passer à côté du platonisme qui fonde la science.

Bon, j'ai écrit tout ça, en espérant surtout réussir à centrer mes contenus de séquents, mais snif, le centrage n'est pas terrible, mais AD, surtout ne gaspille des minutes de ta vie pour les recentrer, sauf si ça te procure une certaine satisfaction, je pense que c'est lisible, même pas "trop centrée".

Précision, je n'ai rien inventé (à part ces règles un peu inhabituelles), cette logique s'appelle "logique linéaire".

J'attends demain pour corriger les coquilles présentes dans http://www.les-mathematiques.net/phorum/read.php?16,1805490,1808312#msg-1808312