Axiomes de ces preuves convenables ?

1) Le ME que j'ai donné est valable pour toute logique (supérieure à l'intuitionniste) et tous ordres et non pas juste la logique propositionnelle. Il est important de comprendre qu'en dehors de considérations recherche/snobisme (les deux n'ont rien à voir), il n'y a pas "d'ordre" à profondément parler en science.

Lorsque tu utilises $R(a)\to [\forall xR(x)]$, aussi pertinent que cela soit vu de l'extérieur, ça n'en est pas moins un admis comme les autres, ce n'est pas à la preuve de "s'apercevoir elle-même" qu'on n'a rien supposé sur $a$. Ca renvoie d'ailleurs aux points 5 et 6 que j'ai conseillé à grthen de reporter sur l'indispensabilité d'être deux. Lorsque le prouveur dit au sceptique je vais te prouver $\forall xR(x)$, choisis $a$, et je te prouve $R(a)$, c'est irréductible au jeu solitaire et il faut avoir l'honnêteté de le dire. L'argument de symétrie qui permet aux "gens de bonne volonté qui brident le sceptique" qui ont reçu un dessous de table du prouveur pour se montrer zentil avec lui ne doit pas tenir lieu de blanc seing.

Quand on est 2, c'est le sceptique (et personne d'autre) qui prendra la charge de se dire que son choix de $a$ (une variable inanalysée auparavant sur laquelle rien n'a été supposée par exemple) est "bon".

A noter que tout ceci n'est pas une faiblesse de la science ni un axiome "à supposer et incontournable". En réalité, quand on fait les choses sérieusement, on n'a pas besoin de passer de "soit x: blabla" à "j'ai prouvé $\forall x:blabla$. Ca n'arrive qu'en pure pratique matérielle pour ne pas en écrire trop long. Fondamentalement, tout est propostionnel et on utilise LES DEUX AXIOMES qui sont SUFFISANT (je l'ai dit 1001 fois):

1/ $\forall ..[(\forall x(A\to B(x)))\to (A\to (\forall xB(x)))]$ (quand $x$ non libre dans $A$)

2/ $(\forall x[A\to B])\to ([\forall xA]\to [\forall xB])$

@grothen: ne peux-tu pas essayer de rédiger sans cabalistique illisible. J'ai bien regardé ta photo, mais elle est décourageante avec des indices, des exposants etc. Essaie de faire sobre et de rédiger les maths sans indices ni exposants, ces compulsions sont de toute façon à proscrire dans un bon texte de maths.

T'es comme Obélix: tombé dans la bassine (de drogue de l'humour) quand tu étais petit toi :-D

Je reprends: ce n'est pas spécifiquement la gestion des variables quantifiées que tu peux accuser de se retrouver recensée avec le label "axiome" par mon recenseur. Ce n'était pas de l'humour. Comme déjà dit, chaque modus ponens se retrouvera recensé par $(A\to \to (A\to $ (ou si le libre-arbitre laissé à l'exécuteur le décide par $A\to ((A\to \to $).

Par contre, dans la réponse que je t'ai faite, tu aurais dû "être content" que j'apporte EN PLUS de ça l'information (que tu connais surement) qu'en plus cette gestion est redondante et ne sert qu'en pratique. Elle n'est nullement nécessaire à la pratique mathématique ou logique.