Informatique
Bonsoir Grothenbiete,
ce livre en particulier non, mais il a écrit des bouquins (que je n'ai pas lus) sur les fondements de l'informatique, à voir.
Sinon, si j'ai 2 neurones, implication ou équivalence ça reste la même chose pouisque l'objet "pizza aux anchois" n'existe que dans le sens (sémantique) de la définition...
Ce qui me chagrine c'est que (littéralement) d'une page à la suivante, on puisse passer d'équivalence à implication, en même temps j'observe que dans l'équivalence ona écrit l'objet désiré AU DEBUT et dans l'implication A LA FIN, serait-ce là la fin de mes soucis???
:-)
merci encore et, contrairement à CC, je ne crois pas les corps de hiérarchies intermédiaires appelés à disparaître, la hiérarchie des grands cardinaux ayant apporté bcp de travail à bcp de monde (et de 3 calembours, je peux aller dormir)
bien amicalement,
F.D.
ce livre en particulier non, mais il a écrit des bouquins (que je n'ai pas lus) sur les fondements de l'informatique, à voir.
Sinon, si j'ai 2 neurones, implication ou équivalence ça reste la même chose pouisque l'objet "pizza aux anchois" n'existe que dans le sens (sémantique) de la définition...
Ce qui me chagrine c'est que (littéralement) d'une page à la suivante, on puisse passer d'équivalence à implication, en même temps j'observe que dans l'équivalence ona écrit l'objet désiré AU DEBUT et dans l'implication A LA FIN, serait-ce là la fin de mes soucis???
:-)
merci encore et, contrairement à CC, je ne crois pas les corps de hiérarchies intermédiaires appelés à disparaître, la hiérarchie des grands cardinaux ayant apporté bcp de travail à bcp de monde (et de 3 calembours, je peux aller dormir)
bien amicalement,
F.D.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
1) déjà le C et le Pascal sont "presque" de bas niveau (ils impressionnent comme ça, mais sont en fait très facile à compiler (y compris les version "++" :-D ), presque autant que l'assembleur. Il ne faut pas oublier que les print, input, etc en tout genre ne sont que des appels aux interruptions toutes faites de l'OS qui garde la main, idem pour les graphiques)
2) Si le hardware n'est pas concerné, ça ne ressemble pas tout à fait à l'assembleur, mais tu peux utiliser le lambda-calcul (version logique combinatoire). Je te donne la définition de l'exécution des processus:
2.1) un processus est un couple $(x,p)$ où $p$ est une suite finie de programmes appelée "pile" et $x$ un programme.
2.2) un programme est un mot parenthésé composé des lettres K,C,W, J (et éventuellement d'autres lettres fournies par le constructeur, qui déclenchent des périphéries hardware. Autrement dit c'est le plus petit ensemble $P$ qui contient les lettres de base, les commodités hardware et stable par couples, ie $P^2\subseteq P$. Un couple de programmes sera appelé un "programme sous forme d'application d'un programme à un autre"
2.3) quand $x$ est un programme, et $p$ une pile, je note $x+p$ le fait d'ajouter $x$ à $p$.
2.4) Un pas d'exécution se fait en respectant les règles suivantes, la flèche représente l'évolution en un pas:
$((x,y), p)\to (x,y+p)$
$(K, x+y+p)\to (x,p)$
$(C,x+y+z+p)\to (y, (x,z)+p)$
$(W, x+y+p)\to (x,y+y+p)$
$(J, x+p)\to (x,p)$
2.5) Quand aucune des règles ne peut être appliquée, le processus s'arrête. Evidemment, le fait d'ajouter des lettres spéciales dans le règlement te permet d'avoir des arrêts significatifs ou des appels d'interruption. Contrairement à un préjugé "sexe des anges", un "bon programme" ne s'arrête jamais (mais il appelle de temps en temps des interruptions pour afficher quelque chose ou autre utilité).
2.6) Théorème: ce paradigme de programmation est universel
2.7) Bon, ça sort un peu de ta demander, mais ça ne me coûte rien de te renseigner. LA grande découverte de la spécialité des 30 dernières années est que "preuves = programmes" (ça s'appelle "correspondance de Curry-Howard", mais elle est souvent très mal énoncée). Chaque instruction réalise un axiome des maths, et le tout est complet. Par exemple, l'instruction $W$ réalise
$$\forall A,B: ((A\to (A\to )\to (A\to $$
L'instruction $C$ réalise
$$\forall A,B,C: (A\to \to ((B\to C)\to (A\to C))$$
et l'instruction $K$ réalise
$$\forall A,B: A\to (B\to A)$$
et l'instruction $J$ réalise
$$\forall A: A\to A$$
Les programmes réalisent les théorèmes. Par exemple
$$((W,J),(W,J))$$
réalise la crise des fondements (il prouve $B$ pour toute phrase $A$ telle que $A=(A\to $)
Pour être tout à fait honnête, ce paradigme ne réalise que la logique intuitionniste. Pour obtenir la logique classique, il faut ajouter une instruction qui permet de "sortir" d'une exécution en cours par la force**. Cette instruction fonctionne comme suit, il y a deux lettres (je prends les lettres T et F (pour "try.. finally" :-D ))
La lettre $F$ n'est jamais seule, elle transporte une suite de programmes (en fait un pointeur vers, mais peu importe), donc je la note $F_p$ pour indiquer que la pile $p$ est attachée à la lettre $F$. L'exécution se fait comme suit:
$((T,u), p)\to (u, F_p +p)$
$(F_p, x+q)\to (x,p)$
La lettre $T$ réalise ainsi l'axiome du raisonnement par l'absurde, énoncé comme suit: $\forall X,Y: ((X\to Y)\to X)\to X$
[small]A noter que j'aurais pu améliorer en disant :
$<<((T,u), p)\to (u, PileAuSeulElement(F_p))>>$
ce qui aurait fait que $T$ aurait réalisé $non(non(X)) \to X$, mais j'ai la flemme de documenter "non" et j'ai eu la flemme d'écrire PileAuSeulElem...[/small]
La traduction avec de l'assembleur direct est très simple:
$W$ exécute: begin pop x; pop y; push y; push y; call x; end
$K$ exécute: begin pop x; pop y; call x; end
$C$ exécute: begin pop x; pop y; pop z; push (x,z); call y; end
sachant que push x empile $x$ sur la pile et pop y dépile le sommet de la pile et le met dans la mémoire y.
edit: j'avais inversé push et pop et je viens de corriger.
** un préjugé veut que la logique intuitionniste serait constructive, mais pas la classique. C'est une erreur assez répandue qui a eu ses heures gloire avant la découverte de ce qui précède (qui date d'environ 30-40ans). En fait, la logique intuitionniste est plus mystérieuse que la classique "l'une est coNP-cmplète" (la classique) alors que l'intuitionniste est carrément PSPACE-complète (c'est beaucoup plus fort).
Beaucoup de gens pensent aussi que les catch (le fait de sortir d'une exécution en cours en jetant tout sauf un petit truc) ne servent que pour le même type d'orientations que les raisonnement par l'absurde. Il n'en est évidemment rien (d'ailleurs, plein de raisonnement par l'absurde sont redondants et pourraient se faire intuinnistement). Pas besoin de faire un dessin pour faire comprendre aux gens que les catchs sont vitaux à l'informatique.
Par exemple, sans catch, il sera difficile de programmer intelligemment la fonction récursive $a$ dont on veut qu'elle satisfasse ($f$ étant donnée): $\forall x: a(x) := f(a(g(x)))$. Si on s'y prend naivement, elle donne l'impression de boucler même si $f$ offre une porte de sortie, puisque semble figurer un appel à $a$ AVANT d'appeler $f$.
Et ça n'a rien à voir avec le RPA. Il en va de même pour simuler séquentiellement la programmation parallèle, par exemple <<if A ou B then action>> dont on voudrait pas attendre la fin de l'exécution de A si on a la chance que B se résolve en vrai en 3 milliardièmes de seconde.
Comment simule-t-on séquentiellement un ou parallèle?
Non, je blague évidemment. Bin comme tu le penses, je ne sous-entendais rien de caché: on hache, ie on exécute un peu de l'un puis un peu de l'autre, puis un peu de l'un, etc. C'est là qu'est important de disposer d'un "raise", pour killer l'un quand l'autre a donné satisfaction.
$$ Step(p,q) \to (q,Step(p))$$
J’ai commencé à lire du coup ça me donne envie de me mettre à l’assembleur, je lirai en détail et réfléchirai dessus demain mais juste avant ça: quand tu écris
((W,J),(W,J))
On est d’accord que l’ordi va faire:
(W,(J,W,J))
(J,(W,W,J))
((W,J),(W,J)) et ça repart pour un tour.
Bon si c’est ça vu que t’as dit que programme = preuve et que preuve = graphe de la dernière fois je vais essayer de comprendre un peu le truc pour voir comment je traduirais un graphe en programme et réciproquement (demain ou après)
Je comprends pas trop le terme « réalise » quand tu dis que W réalise l’axiome bidule mais j’y réfléchirai demain.
Édit: faut que je vois la pile comme une liste d’axiomes et les lettres ce qui permet d’ajouter une phrase à cette liste c’est ça ?
1) D'abord, il faut définir ce qu'est une phrase: c'est un ensemble de piles. On dira que ces piles "agressent" les phrases auxquelles elles appartiennent.
2.1) La phrase $A\to B$ est l'ensemble des piles de la forme (x,p) de la forme $x+p$ telles que $p$ agresse $B$ et $x$ réalise $A$.
2.2) La phrase $\forall xR(x)$ est l'ensemble des piles qui agressent au moins une des phrases $R(a)$, pour un objet mathématique $a$.
3) Ensuite il faut définir un truc (qu'on est presque totalement libre de prendre comme on veut): c'est l'ensemble des processus que l'on considère comme "donnant satisfaction", je le note Paradis. La seule chose qu'on demande (pour tous $p,q$) à cet ensemble c'est d'être stable par "pas inverse", ie si après un pas d'exécution, p devient q et si $q\in Paradis$ alors $p\in Paradis$.
4) pour $x$ programme quelconque et $E$ phrase quelconque, $<<x$ réalise $E>>$ est une abréviation de $<<$ pour toute pile $p$ qui agresse $E: (x, p)\in Paradis>>$.
Avec ça, les annonces que je t'ai faites ne sont plus culturelles, elles deviennent des théorèmes prétendus qu'un exercice que tu peux faire et qui n'est pas très difficile consiste à prouver. Tu peux aussi essayer de réaliser $(A$ ou $(non(A)))$ avec un programme de ta conception.
Je te rappelle la définition du mot $ou$:
$$(A\ ou \ := [\forall X: ((A\to X)\to ((B\to X)\to X))]$$
D'accord, c'est donc ça que tu appelles "simulation séquentielle". Je ne crois pas que ton formalisme soit suffisamment expressif pour pouvoir réaliser ça, je crois qu'on a besoin d'étendre ce paradigme pour pouvoir faire ça, mais c'est peut-être que ce tu voulais dire avec ton "Step".
D'accord, mais je ne comprends pas pourquoi tu dis que "ça n'a rien à voir avec le RPA". Prétends-tu que ton formalisme restreint à la logique intuitionniste permet de réaliser un "raise"?!
Dans 2.1 tu dis que la phrase bidule est l’ensemble des piles (x,p) déjà là tu assimiles bien suite finie à deux éléments et couples on est d’accord ? Et surtout quand tu dis « tel que p agresse B » donc p appartient à B ça veut dire que p est une pile mais dans ta définition de pile c’est une suite finie de programmes donc p est une pile et un programme ? Pour moi c’est possible que si c’est une pile à deux éléments assimilée à un couple parce qu’un couple de programmes est un programme donc tu voulais dire que dans B on prend que les piles-programmes pour constituer les (x,p) ?
L'universalité du petit type de processeur que j'ai évoqué (dû à JLKrivine et non à moi au fait!!!) le prouve d'ailleurs. On n'a pas une classe plus large d'ensembles calculables parce qu'on ajoute un raise. Je ne sais d'ailleurs pas (pour ne jamais y avoir réfléchi) si la raisitude peut augmenter strictement la puissance quand on admet des oracles, des environnements non déterministes ou quantiques, etc. J'essaierai de formaliser cette question de manière précise pour la postre dans "il est facile de".
Et oui oui, mieux vaut ajouter un outil "step" pour le parallélisme, là aussi, que le "simuler de manière empotée" avec des lambda-termes élaborés.
A noter que je ne suis pas un expert, il faudrait que je revisite la page de JLK, car je crois qu'il y a des pdf, peut-être moins "célèbres" qui traînent et parlent de ces "détails".
Ca, ça ne prouve rien du tout. Ce n'est pas parce qu'on n'obtient pas plus de fonctions calculables en ajoutant un ou parallèle ou un raise qu'on peut simuler un ou parallèle ou un raise.
Tu dis qu'on pourrait simuler un ou parallèle avec des lambda-termes. Encore une fois, je demande à voir. Tu dis beaucoup de choses, mais je ne vois ni preuves ni références.
Non, si c'est ta définition de "simuler", elle n'a aucun intérêt et n'importe quoi simule n'importe quoi. Bien sûr, avec une telle définition, le lambda-calcul "simule" tout et tout ce que tu as écrit est complètement vide.
Il existe plein de définitions intéressantes de "simuler" qui sont assez subtiles. Dans le cas du ou parallèle, une question intéressante est la suivante : existe-t-il un programme t tel que pour tous programmes u1 et u2, le programme t appliqué à u1 et à u2 retourne vrai si u1 ou u2 retourne vrai et retourne faux si u1 et u2 retournent faux? On peut montrer qu'il n'existe pas de lambda-terme t qui se comporte ainsi et donc le lambda-calcul ne peut pas simuler le ou parallèle. Et pourtant si on ajoute le ou parallèle au lambda-calcul on n'obtient pas plus de fonctions calculables, puisque le lambda-calcul est Turing complet.
Merci de t'interesser à cette réponse locale que je faisais à grothen et de m'enrichir en connaissances mais ne m'attribue pas des intentions que je n'ai pas. De mon téléphone
Comment prouves-tu cet énoncé en l'absence de constante?
(1) $\forall x P\vdash P[x:=x]$ (élimination de $\forall$)
(2) $\forall x P\vdash \exists x P$ (introduction de $\exists$ avec $x$ qui est un terme).
(3) $\vdash \forall x P \to \exists x P$ (introduction de $\to$).
$$\begin{array}{rcl} P&\vdash_{[x]}&P\\\hline P&\vdash_{[x]}&\exists x\;P\\\hline \forall x\;P&\vdash_{[x]}&\exists x\;P\end{array}$$
Ce séquent à contexte est bien un théorème intuitionniste. Par contre $\forall x\;P \vdash_{[]} \exists x\;P$ ne l'est pas.
Les règles d'introduction de $\exists$ à droite et d'introduction du $\forall$ à gauche ne modifient pas le contexte. Par contre, les règles d'introduction de $\forall$ à droite et d'introduction du $\exists$ à gauche permettent d'enlever la variable quantifiée du contexte (sachant qu'elle ne figure pas comme variable libre dans les autres formules du séquent).
@foys: comme je l'ai dit 1000 fois (au point que ça relève du militantisme) le mieux est d'utiliser des axiomes plutôt que des systèmes "pratiques" de déduction de sorte que le sceptique puisse contester sans partie cachée. Et surtout se rappeler qu'une variable ne peut avoir que 2 statuts: liée ou libre mais dans le cas libre c'est UNE CONSTANTE (au sens : nom propre provisoire, pas "fonction constante")
Dans le cas présent la logique intuitionniste ou la logique classique ne différent que très peu, même si la classique ne donne qu'une seule partie non vide à 1.
Je note A pour "quelque soit" et E pour "il existe". Ce que tu prouves est :
Ax: ( (AyR(y)) => R(x)) ainsi que Ax((AyR(y)) => (EzR(z))).
De manière générale quand P ne dépend pas de x: P=>(AxP) est un théorème mais pas sa réciproque. Bizarrement tout ceci est extrêmement banal avec sup et inf et superbement ignoré avec A et E qui pourtant SONT ni plus ni moins que sup inf dans l'espace ordonné des phrases
D’ailleurs je crois que tu avais inversé pop et push, push empile et pop desempile dépile si je comprends bien.
(W,(J,W,J))
(J,(W,W,J))
(W,(W,J))
(W,(J,J))
(J,(J,J))
(J,(J))
(J,())
Erreur ?
comme tu le fais) ne change pas grand chose.
@GaBuZoMeu: tu as une référence pour le calcul des séquents avec contexte? (dans l'exemple ça reviendrait à montrer
$\forall c [(\forall x P (x) \to \exists xP(x)]$. J'ai l'impression qu'il s'agit de variables locales- en tout cas c'est ce qui se passe si on fait ça en Coq mettons).
@foys. : bien sur que si si. En fait ça ne change pas grand chose en propositionnel mais quand tu as dans variables liées ça change beaucoup car par exemple les séquents inventent des règles de sorciers indiens pour par exemple dire l'usine à gaz " jai prouve ça pour x mais comme j'ai rien supposé sur x, mseiurs dames vous m'accorderez d'en inférer forall x" devant quoi on n'a plus qu'à se mettre à genoux devant msieurs dames pour qu'ils adoubent.
Dans je ne sais plus quel clip une fois j'ai entendu Girard pourtant expert dire la bêtise de sa vie c'était un truc du genre << les gens sont superficiels ils confondent vdash avec une implication>> tout ça parce que travaillant sur la partie calculs automatiques il était tombé amoureux du buffer.
La on n'est pas en CCH. On se demande juste ce qu'on accepte comme axiomes. Et dans ce contexte les séquents sont très mauvais s's induisent l'impression d'une différence entre A;B vdahs C et A=>(B=>C)
Bien entendu que si on automatise on trouve des zolis combinateurs et des zolies inférences rôle bustes qui "font sortir" de l'impression philosophique désuète de "chercher ce qui est vrai". Mais il faut se maitriser. Même en logique pure :-D l'ivresse gauchiste peut jouer des tours :-D
Tu vois bien que tu as identifié l'erreur grâce à "Hilbert" (bien grand mot) même si GBZM a doctement signalé une manière de "NE PAS LA FAIRE qUI S APPREND PAR COEUR " avec un autre système, ton indépendance d'esprit ne peut que regarder des phrases qui ont un sens (îe qui sont closes) et donc , par exemple ici, voir que c'est (forall x A)=> A (quand A ne contient pas d'occurrence de x) qui n'a aucun caractère d'axiome acceptable. Difficile d'exercer son esprit critique sur un vdash puisque le statut d'un sequent est peu assumé comme affirmation.
M. Coste : Logique du 1er ordre dans les topos élémentaires, Séminaire Bénabou 1973-74
Variables locales ? Je ne vois pas trop.
Les régles d'introduction du $\forall$ et du $\exists$ (avec les séquents à contexte) sont les reflets fidèles du fait que $\forall x$ et $\exists x$ sont les adjoints (à droite et à gauche respectivement) de l'image réciproque par la projection qui oublie $x$.
J’avais compris la chose suivante:
Quand tu dis ((W,J),(W,J))
Pour moi la pile c’est celle qui contient le programme W et le programme J et pas la pile qui contient juste le programme (W,J) et pensais que tu te permettais d’ecrire (W,J) sous forme de couple au lieu d’ecrire {(0,W),(1,J)} parce que t’avais dit qu’une pile était une suite finie. Donc en fait quand t’ecris ((W,J),(W,J)) c’est ((W,J),{(0,(W,J))}) c’est bien ça ? Ou quitte à confondre suite finie et uplet c’est Ça : ((W,J),((W,J))) ?
En espérant ne pas me tromper
Pour les variables locales je parle de ça: on peut considérer qu'on déclare les variables $t_1,...,t_d$ ("locales à $\vdash_{[t_1,...,t_d]}$" si on peut dire. Je demande parce que j'ai jamais vu les contextes avant) et si on écrit une preuve $A\vdash_{[t_1,...,t_d]} B$ et on se retrouve in fine avec $\vdash_{[]} \forall t_1\forall t_2...\forall t_d (A\to $.
@Christophe : ce que tu racontes ici est aussi explicite pour moi que ta démonstration de l'irrationalité de $\pi$.
Même pour ceux qui connaissent Coq, il est très difficile de lire une preuve écrite en Coq sans la "jouer". Au minimum, il faut rendre tout explicite; par exemple, tu ne dois pas écrire "intros" mais "intros H", car sinon quand tu utilises H le lecteur doit deviner de quoi tu parles. Et même comme ça...
Est-ce parce que tu avais une pratique de COQ? GBZM avait l'air réservé quand tu lui as demandé.
D'autant que si on ne regarde pas le côté informatique on retrouve e EXACTEMENT le fonctionnement des quantifications bornées (qui font par exemple que "pour tout x dans emptyset: 2+3= 9 est vrai)
Édit: ah ok c’est Bien ça, bah merci pareil pour moi. Je reviendrai poster une preuve de A ou non(A) du coup j’essaierai de le faire en assembleur vu que je vais essayer de m’y mettre au pire si c’est trop dur en python. Mais vraiment merci de tes réponses super complètes et personnalisées !
Quant aux quantifications bornées je ne vois pas ce que ça vient faire là.
Types et ensembles ne sont pas les mêmes choses (deux ensembles différents peuvent ne pas êtres disjoints et si $A,B$ sont des ensembles, $A\cup B$ ou encore la phrase "$A$ est inclus dans $B$" ont du sens sans faire intervenir de considérations catégoriques subtiles ).
La logique du premier ordre est en fait une logique d'ordre supérieur déguisée où il n'y a qu'un seul type: l'univers, qui est supposé non vide (dans ZFC il y a $\emptyset$, dans PA il y a zéro... et de toute façon je mets au défi quiconque d'affirmer en toute bonne foi travailler dans un univers-i.e. tout ce qui peut exister-censément vide et y faire des mathématiques sophistiquées).
En logique du premier ordre on peut faire de la logique d'ordre supérieur en introduisant des symboles de prédicats et en disant comme d'habitude que $\exists x:T$ signifie $\exists x:T(x) \wedge(...)$ et $\forall x:T$ abrège $\forall x:T(x)\to(...)$. Du coup on a $(\forall x P)\to (\exists x P)$ toujours vraie et $(\forall x:T, P)\to (\exists x:T,P)$ peut-être fausse, sans gêne spéciale.
Édit 1: intuitivement en fait c’est l’ensemble vide non ?
Édit 2: ok en fait en réfléchissant un peu plus, si un programme x comme ça existe alors x réalise faux d’ailleurs ce programme n'est pas unique dès qu’il y en a un y en a une infinité il suffit de considérer la suite de programmes (J,J,....(J,x)))))
Et si x réalise faux alors en particulier il réalise « pour tout A A implique faux » bon je sais que cette phrase est censée être fausse mais je vois pas en quoi le fait qu’un programme réalise cette phrase ne soit pas bien mais c’est peut-être parce que je ne vois pas ce que réaliser au fond veut dire.
Édit 3: je crois que je comprends ta phrase faux = tout est vrai
Effectivement l’ensemble des piles = pour tout A, A est bien l’ensemble Faux. C’est ça que tu voulais dire?
Bon allez, j’ai beaucoup trop traîné je pars pour de bon
En tout cas, comme je ne suis pas sûr de beaucoup me connecter, je souhaiterais présenter mes excuses à la fois les plus sincères mais honteuses à GBZM: j'ai l'impression que je lui ai fait un procès d'intention et que j'ai sauté comme un roquet sur l'occasion pour faire de la politique alors que le sujet n'aurait pas dû légitimer ça. en effet, je lui ai fait le procès de défendre le typage alors que bon, même s'il le défend dans d'autres fils, rien n'indiquait que ce fusse le cas (oulala mon subjonctif bof bof) ici.
@foys: je me demande (mais n'ai pas eu le temps de relire vraiment bien le fil d'nu pc, jje 'lavais fait de mon téléphone) si tout simplement, ce ne seraient pas plutôt des "variables ultraglobales" qui seraient ici évoquées. Je m'explique par un exemple:
je suis entrain de faire un raisonnement
.
.
${\color{red}{[\ldots\forall w\forall x]}}$ blabla
${\color{red}{[\ldots\forall w\forall x]}}$ blabla
${\color{red}{[\ldots\forall w\forall x]}}$ $A_1;A_2\ldots\vdash R(x)$
${\color{red}{[\ldots\forall w]}}$ $A_1;A_2\ldots\vdash \forall x: R(x)$
etc,
etc,
(avec du non écrit ou du tacite rouge sur la gauche)
qui est très exactement ce que je passe mon temps à recommander, et ce, comme je l'ai dit moult fois, pour éviter de voir des gens dire (théoriquement, la pratique jela respecte), $<<$ je passe de $R(x)$ à $\forall x: R(x) $ car je n'ai rien supposé sur $x>>$
Avec cette présentation, on voit que l'inférence n'est pas philosophique mais purement technique, ie on utilise (de manière itérée) l'axiome "pur et dur et assumé" : $[\forall x(A\to ]\to [(\forall xA)\to (\forall xB)]$ ce qui est bien évidemment la seule manière respectable de convaincre scientifiquement.
Si GBZM voulait dire àa alors effectivement, j'ai accompli un HS agressif totalement hors sol. Mais je préfère que les $\forall $ d'arrière-plan apparaissent à gauche toute qu'en indice du $\vdash$ pour exprimer un goût.
Mai sil ne voulait peut-être pas promouvoir ça, je ne sais pas. Par contre, le terme "local" pour ces variables ne me semble pas du tout adapté (on les voit au contraire bien global non?)
.
La décoration de séquents avec un contexte permet d'éviter la blague du $\forall x\;P\vdash \exists x\; P$ et d'exprimer correctement le fonctionnement des quantificateurs. Je ne vois pas la nécessité de quantifier universellement systématiquement comme tu le fais (phobie des variables libres ?) et je préfère aux axiomes les règles de déduction qui expriment de manière transparente, pour les quantificateurs, les propriétés d'adjonction que j'ai mentionnées plus haut. J'ai des arguments pour ces choix, mais ça ne fait pas une différence fondamentale.
(Précision: je vais surement m'évader un peu de Paris en voiture, je ne répondrai pas forcément rapidement)
Non, non, ce n'est pas du tout une phobie (d'ailleurs je n'ai même plus la phobie de l'avion et je ne suis plus hypocondriaque :-D soit dit en passant (et je ne suis plus jamais saoul, même quand rarement je bois, je trouve ça inquiétant car je ne bois pas, ou peu) )
En fait, je distingue deux types de discussions:
1) celles "pratiques" où on optimise et économise encre, etc. Dans ce cas, évidemment je suis comme toi, je préfère largement implémenter des règles plutôt que n'user que d'axiomes
2) Celles "philosophico-platoniciennes" disons où on a face à soi la scepticie naturelle émergeant du devoir de la science. Là, plus question de balancer à un sceptique des règles au risque (le sceptique est un roi absolu dans son statut) de le voir tout balancer par dessus bord en disant "je n'ai pas la preuve que vos règles sont acceptables". Dans ce deuxième type de discussion, le sceptique est (par mon choix stratégique) contraint de ne pouvoir rejeter que des affirmations bien carrées et surtout closes.
Je l'ai déjà dit avant, je ne vois pas répondre à un sceptique (à un élève pourquoi pas, mais un sceptique androide): "bin n'ayant rien supposé sur $x$, je me permets de passer de $R(x)$ à $\forall xR(x)$"
Par contre, ça ne me dérange pas de voir le sceptique contester $(\forall x[A\to B])\to [(\forall xA)\to (\forall xB)]$, car là j'assumerai de lui répondre "tant pis, je perds la partie"
$G \vdash_{[x ,y]} B(x)$ donne $G\vdash_{[y]} \forall xB(x)$
$A(x) \vdash_{[x,y]} D $ donne $\exists x A(x) \vdash_{[y]} D$
$$\begin{array}{rcl}
A&\vdash_{L,x}& B(x)\\\hline
A&\vdash_{L}& \forall x\;B(x)
\end{array}$$(où $x$ n'est pas variable libre dans $A$)
me semble tout aussi carrée et close que ton axiome.
Il me semble d'ailleurs que tu ne peux pas t'en tirer avec les quantificateurs sans axiome où tu es obligé de préciser que "$x$ n'est pas libre dans telle sous-formule". Comment fais-tu avec ton axiome pour montrer $A\to \forall x\; A$ quand $x$ n'est pas variable libre dans $A$ ?
PS. C'est une réponse à Christophe. Par ailleurs le message de Foys ne me convainc toujours pas que c'est pertinent d'appeler "variables locales" les variables du contexte.
1°) preuve à laquelle on pense dans le contexte x,y.
2°)$x\neq y \vdash_{[x:\N,y:\N]} x+y \neq 0$
3°) $\vdash_{[x:\N,y:\N]} x\neq y \implies x+y \neq 0$
4°) $\vdash_{[x:\N]} \forall y:\N, (x \neq y \implies x+y \neq 0)$
5°) $\vdash_{[]} \forall x,y:\N, (x \neq y \implies x+y \neq 0)$.
Dans Coq, il s'avère qu'on a ceci:
C'est sur ça que je fonde ma remarque.