Qui peut le plus peut le moins ?

Déjà répondu souvent: tout théorème est un cas particulier d'évidence. Il existe donc pour chaque théorème P une preuve de la forme " E donc P " où E est une évidence (au sens strict et formel) et où P est un cas particulier de E. Fais une recherche j'ai donne plein de détails dans plein de fils ces dernières années.

De mon téléphone : j'essairai de te trouver des liens d'un PC. Pour les évidences, non, par définition "éthique" il suffit de lire l'énoncé pour dire s'il est évident ou pas. Idem je te mettrai des détails d'un PC. Pour l'instant retiens qu'un énoncé est évident s'il est un axiome ou s'il est d'une forme telle que sa conclusion s'obtient par modus ponens consommant*** à partir de ses hypothèses étant entendu que les hypothèses de A=> B sont les hypothèses de B auxquelles on ajoute A.

*** chaque hypothèse n'est utilise qu'une et une seule fois (ie une fois qu'on a échangé X=>Y et X contre Y on n'a plus X ni X=>Y)

Décidément ta compréhension est rudimentaire et trop expédiée. Prends le temps de réfléchir à ce qu'on te dit sinon tu ne progresseras pas

Et voilà: tu es encore incordial ... Je regrette presque de t'avoir répondu. À supposer que CG soit un cas particulier de l'énoncé "L=>L" où L est une certaine phrase contenant 10^30 lettres tu crois vraiment que l'humain peut deviner facilement l'existence d'un tel L?

Tu confonds arbitrer et trouver. J'ai répondu à ta question initiale. J'ignore si ça vaut le coup vu ce que tu en fais de te donner l'autre direction bien connue: l'élimination des coupures fait que tout théorème s'obtient AUSSI comme cas particulier d'évidence (courte cette fois) avec chemin concret qui descend de l'évidence au CP qu'est le théorème. Mais dans cette deuxième approche le chemin est parfois long. Par ailleurs l'absence de linéarité des logiques classiques peut le rendre très très long.

Je n'étais pas incordial je parlais de ta compréhension MANIFESTÉE par ta réponse et tes modifications négligées . Chaque mot renvoyait à des point très précis: tu remplaces cas particulier par suite de, tu ne lis pas le post, tu réponds de manière agressive sur le fond (OK prouve que CG est évident), etc. Bref tu ne produites pas de la réponse qui t'a été faite.

@PE: il y a une chose dont Gérard n'est pas suspect, c'est d'être complaisant à mon égard. il lui arrive souvent de s'opposer à moi. Cela devrait t'indiquer deux angles de vue très différents qui te renvoient la même couleur. Cela dit, à toi d'y réfléchir, je ne vais pas deviser pour que tu comprennes.

Comme je suis sur un PC, je vais te donner des précisions techniques, mais tu en feras bien ce que tu voudras. Je ne traites que la situation propositionnelle puisque la situation "au premier ordre" comme on dit s'extrapole trivialement (il s'agit essentiellement de compléter la structure ordonnée).

Les phrases scientifiques peuvent essentiellement être considérées syntaxiquement, ou quasi-syntaxiquement comme formant une structure $(P, \leq, +, -)$ où $+,-$ sont deux opérations commutatives et associatives (ne pas confondre avec le signe moins habituel, ce sont deux "additions" à leur façon), croissantes des deux côtés, avec chacune un élément neutre ($1$ pour $-$ et $0$ pour plus disons) et une involution que je noterai "non" qui est décroissante et telle que $\forall x,y: non(x+y)=non(x)-non(y)$.

La seule autre "grande propriété" qu'elles sont est que $a+(b-c) \leq (a+b)-c$ et $a+(non(a) = 0$ et $a-non(a)= 1$.

Les théorèmes que je qualifierai "d'initiaux", sont tout bêtement les expressions de la forme $a-non(b)$ qui sont telles que $b\leq a$. Dans la spécialité officielle, ce sont d'autres signes qui sont utilisés, et la logique obtenue est appelée "logique linéaire".

Pour obtenir les autres logiques (plus fortes), que sont l'affine, l'intuitionniste et la classique, on n'a pas besoin d'ajouter des propriétés à cette structure, il suffit de supposer l'ordre complet et de trouver pour chacune de ces logiques la conjonction de ce qu'on considère comme devant en faire partie comme axiomes.

Le point important est le suivant. Si une expression ne contient que deux occurences pour chaque lettre, alors elle est évidente "à l'oeil nu" ssi elle est un théorème (linéaire***)

On obtient tous les théorèmes en particularisant, c'est à dire en remplaçant $\forall x,y: R(x,y)$ par exemple par $\forall x: R(x,x)$.

Par aillleurs, tous les théorèmes DE MATHS (ie obtenus en logique classique) P sont telles qu'il existe une suite finie $H_1,..,H_n$ telle que $H_1\to (H_2\to (...\to (H_n\to P)...)$ est une évidence particularisée (ie un théorème linaire) et chaque $H_i$ est d'un des 4 formes suivantes:

1) A=> (A et A)
2) (A et =>A
3) no(no(A)) =>A
4) un axiome non logique assumé fermement

qui eux ne peuvent être considérés comme "des évidences pures" car ils constituent de véritables pétitions de principe sur l'immuabilité des vérités scientifiques (la 1 qu'on peut les cloner, la 2 qu'on peut jeter des hypothèses, la 3 le raisonnement par l'absurde)

Je te laisse faire l'exercice (édifiant pour toi, même si pas facile) de définir "et", "=>" et "no" à l'aide des primitives.

Mais celui qui est facile est de prouver l'assertion rouge. Ca te fait deux activités pour lesquelles, je ne pense pas que je me fatiguerai à te proposer une solution si tu ne trouves pas , sauf si tu avances avec un réel effort dans l'investigation en posant des questions bien précises et contextuées.

*** qui peut se prouver en exploitant chaque hypothèse une seule fois et en n'en jetant aucune (ie en les utilisant toute une et une seule fois). Par exemple : (A=>A)=>(B=>B) n'est pas un théorème linéaire.