Raisonnement par l'absurde (repetita)

christophe c

Comme ça donne des serpents de mer régulièrement, je refais un fil court sur ces questions. J'évite de parler des quantificateurs, ajout ultérieur si besoin.

1/ Quand on prétend donner des noms à des raisonnements, c'est un abus de langage populaire. On donne en fait des noms à des axiomes ou des logiques.

2/ Je rappelle donc la hiérarchie des logiques.

3/ Comme je veux éviter de ne m'adresser qu'à des logiciens, qui n'ont pas besoin de lire ça, je présente la structure.

4.1/ Les phrases sont munis d'un ordre naturel $\leq $ et d'un élément, que j'appelle $1$ qui joue un rôle proche de la neutralité. Pour simplifier, tout ensemble de phrase a une borne inférieure (et donc aussi une borne supérieure).

4.2/ Pour toute phrase $x: (1\to x)=x$.

4.3/ Pour toutes phrases $x,y: ( [1\leq (x\to y)]$ ssi $x\leq y$.

4.4/ L'opération $\to$ est décroissante à gauche et croissante à droite.

Je viens de décrire le fondement le plus en amont. Viennent aussitôt après la commutativité d'un certain "et" qui s'exprime comme suit:

4.5/ Pour tous $x,y,z: (x\to (y\to z))=(y\to (x\to z))$

Jusqu'à présent on est dans les logiques extrêmement faibles. Je ne précise pas les noms, peu importe.

4.6/ Deux axiomes AUDACIEUX:

4.6.1/ Le fait de pouvoir jeter des hypothèses: $\forall x,y: x\leq (y\to x)$

4.6.2/ Le fait de pouvoir DUPLIQUER des hypothèses: $\forall x,y: [x\to (x\to y)] \leq [x\to y]$

Si vous admettez pour votre structure tout ce qui précède, vous avez ce qu'on appelle "la logique intuitionniste". Je note maintenant $0$ le plus petit élément de la structure (appelons-le "le faux", même si je préfère l'appeler "tout", car c'est l'abréviation de "tout est vrai" en quelque sorte).

4.7/ Exercice: on admet que la structure vérifie tous les axiomes précédents (ceux de la logique intuitionniste).

Notons $\wedge$ l'opération $(x,y)\mapsto \inf(x,y)$.
Notons $+$ l'opération $(x,y)\mapsto $ la borne inférieure des $(x\to (y\to t)) \to t$ quand $t$ parcourt $S$ (ie la structure).

4.7.1/ Prouver que $+=\wedge$.

Je recommande de "prendre son temps et déguster" (4.7). C'est ça la seule grande découverte qu'on peut qualifier de récente. La distinction dont je vais parler maintenant intuitionnisme/classique est beaucoup moins profonde et beaucoup plus ancienne. Elle est grande, mais elle n'est pas pertinente. Cependant, elle est basé sur le droit ou pas qu'on se donne de faire des raisonnements dits par l'absurde.

4.8/ Donner des exemples de structures intuitionnistes où on n'a pas: $ \forall x: ((x\to 0)\to 0) = x$

4.9/ On dira qu'une structure vérifie le RPA (raisonnement par l'absurde) quand on a la propriété (4.8).

A la louche et à vue de nez, j'ai pu remarquer ces dernières décennies sur le forum qu'une forme de "fatigue" des débutants s'incerne au moment où ils "acceptent" (mais mal et de manière traumatisée) que $non(x) = (x\to 0)$.

Ca leur pose un problème au moment de "comprendre" (enfin je dirais plutôt d'accepter) que les preuves (par exemple) de l'irrationalité de racine de 2 ou de l'absence de surjection de $E$ sur $P(E)$ sont parfaitement intuitionnistes.

Je rappelle donc pour la millième fois que $(non (A))=(A\to 0)$ est essentiellement un théorème et non une convention. En voici une preuve:

Supposons non $A$.
On en déduit $1\to (non(A))$, puis $non(non(A)) \to non(1)$, donc $A\to 0$.

Réciproquement, supposons $A\to 0$.
On en déduit $non(0)\to non(A)$, puis finalement $non(A)$

via des axiomes acceptés par 100% des êtres humains comme vous pouvez le lire.


Pour les gens qui en ont marre de réexpliquer 500 fois la même chose, n'hésitez pas à mettre ce post en lien et balancer le lien quand besoin (il faut s'adresser tout de même à des diplômés, car j'ai choisi un exposé abstrait non logicien. Mais en gros, avec un peu d'effort...

PelucheCanard

Qu'est-ce que "non(x)" en logique intuitionniste ?

Foys

Modèles de Kripke:

@PelucheCanard: soit $(T,\leq)$ un ensemble ordonné (le "temps" ?). Soit $\Omega$ l'ensemble de toutes les parties $X$ de $T$ telles que pour tout $a\in X$ et $b\in T$, si $a\leq b$ alors $b\in X$ (on pourrait appeler $\Omega$ l'ensemble des "parties définitives" de $T$).

"$A$ est vraie à partir de $t$" := $t\in A$

$\Omega$ est clairement stable par union et intersection quelconques.

-Si $A,B\in \Omega$ on pose $A\wedge B:= A \cap B$ et $A \vee B:= A \cup B$ (ce sont aussi des éléments de $\Omega$) ).

-On pose $A\Rightarrow B:=$ la réunion de tous les éléments de $\Omega$ contenus dans $(T\backslash A) \cup B$ (c'est aussi un élément de $\Omega$). On a pour tous $A,B,C\in \Omega$, $A\cap C \subseteq B$ si et seulement si $C \subseteq A \Rightarrow B$.

-en fait pour tous $P,Q\in \Omega$, $P\subseteq Q$ si et seulement si $(P\Rightarrow Q) = \Omega$.

- On pose $\perp := \emptyset$ et $\neg A:= A \Rightarrow \perp$.

-Si $f$ est une application d'un ensemble $E$ dans $\Omega$, on pose $\forall x\in E, f(x) := \bigcap_{x \in E} f(x)$ et $\exists x \in E, f(x) := \bigcup_{x \in E} f(x)$.

On peut vérifier qu'avec ces conventions, $\neg \neg A \neq A$ pour certains choix de $A$ et de $(T,\leq)$ (contre-exemples avec $T$ de cardinal 2 !!).

PelucheCanard

@Foys Je ne comprends pas la relation de comparaison : pour moi $(T, \le)$ signifie que $\le$ est définie sur $T\times T$, on peut comparer un élément de $T$ avec une partie de $X$ ? Est-ce que la notation $a\le b$ signifie que cette relation est vérifiée pour tous les éléments de $a$ ?

christophe c

@PC: j'ai répondu dans mon post à ta question du post2 du fil (post1 de ta part).

Si tu veux des détails "vraiment fins", il n'y a qu'à partir de la logique linéaire et celles plus faibles que tu n'as plus cette égalité (la LL est décrite dans mon post en s'arrêtant à 4.5).

Je ne détaille pas plus puisque je ne crois pas désireux de descendre plus bas que l'intuitionnisme, mais si je me trompe dis-le, je développerai.

PelucheCanard

@christophe c

Je ne comprends pas dans ton post initial, tu dis que $non(x) = (x\to 0)$ est un théorème et non une convention. Mais dans ce cas quelle est la définition de $non$ ? Je pensais que c'était par définition que $\neg A$ est par définition $A \vdash \bot $.

christophe c

De mon téléphone. Dans le dernier paragraphe avant la barre horizontale de mon premier post je "justifie" la définition. Ça te permet autant de voir ça comme une définition si tu veux pas te prendre la tête que comme un théorème si t'as envie. All inclusive IS my club.

Dom

Christophe,
Tu es bizarre.

N’est-il pas possible d’avoir en un message le plus court possible ta définition de $non(A)$ quel que soit $A$ ?

Dans un autre fil, comme le suggère PelucheCanard, tu avais écrit :
Définition : quel que soit $P$, $non(P):=(P\Rightarrow tout)$.

Mais là, tu dis que c’en est une autre. Ça ne gêne personne mais on voudrait savoir ce qu’est alors cette satanée définition du $non$. Si je l’ai loupée, qu’on me pardonne.

Thierry Poma

Selon Jacques Duparc, page 198 de son livre La logique, pas à pas, l'on a ceci en logique minimale :

PelucheCanard

Je vois la règle $\neg i$ qui a l'air de stipuler que si on a $\phi \vdash \bot$ alors on a $\neg \phi$ dans cet extrait.

Thierry Poma

C'est pas faux ! Bien vu... Pour l'instant, l'on a $\neg\,\phi\rightarrow(\phi\rightarrow\perp)$.

Thierry Poma

Erratum :

L'on a affaire à la règle de l'introduction de la négation :\[\dfrac{\Gamma\cup\{\phi\}\vdash\perp}{\Gamma\vdash\neg\,\phi}\]règle logique valable en logique minimale, qu'il ne faut surtout pas confondre avec la règle d'absurdité classique [\dfrac{\Gamma\cup\{\neg\,\phi\}\vdash\perp}{\Gamma\vdash\phi}\]

Finalement, $\vdash_m\,\neg\,\phi\leftrightarrow(\phi\rightarrow\perp)$, comme attendu.

Thierry Poma

Voici un texte que j'ai déjà posté, où l'on reconnaîtra sans peine l'usage (en logique intuitionniste) de la règle de l'introduction de la négation :

Dom

Pardonnez-moi, vous êtes mieux à même de comprendre ces lignes « codées » pour moi.
« Il faut considérer que ... » n’est pas satisfaisant pour moi.

Si l’on décèle dans ces papiers cette équivalence entre la négation et « implique tout » puis-je savoir ce qu’est la négation ?

En fait je ne comprends pas pourquoi on tourne autour du pot. Qu'est-ce qui est tabou bord.. de m.... ? :-X

(Je ne suis pas fâché malgré mon langage et le smiley, mais très intrigué)

Dom

Question pour ma culture générale :
Quel genre de raisonnement permet de démontrer qu’un théorème ne peut pas être démontré sans RPA ?
C’est une digression rapide, je ne vais pas en générer des tartines de messages.
Est-ce une histoire de « meta-langage » (notion que je balance sans la maîtriser du tout) ?

PelucheCanard

Je pense que pour démontrer qu'un théorème a besoin du RPA, il faut prendre pour hypothèse que le théorème est vrai, et en déduire le RPA.

Dom

Je traduis ce que tu dis (j’essaye...)

Soit $T$.
Si on a : $T\Rightarrow (\forall X, non(non(X)\Rightarrow X))$,
Alors $T$ n’est pas démontrable sans RPA.

Attention au lecteur hâtif. C’est une suggestion. Pas forcément quelque chose de valide.

Maxtimax

Par exemple, mais ce ne sera pas forcément le cas. On peut aussi aller regarder des modèles (comprendre "univers mathématique" en quelque sorte) où le tiers exclu n'est pas vrai, mais tout le reste, si, et regarder ce que deviennent nos énoncés.
Si l'un des deux devient pas vrai, il ne peut être démontré sans tiers exclu (plus précisément : il ne peut être démontré en logique intutionniste)

christophe c

Un exemple d'énoncé non démontrable en LI et qui n'implique pas prouvablement le RPA :

Le buveur. (Il existe une personne qui si elle boit alors tout le monde boit)

Je détaillerai de mon téléphone comment on prouve sa situation. C'est probablement le plus célèbre des entre deux parmi les puissants

christophe c

D'un PC, c'est plus simple de te répondre dom. Exceptionnellement, je ne le fais pas d'habitude, je vais utiliser des notations totalement neutres.

Soit $E$ un ensemble ordonné complet (tout ensemble a une borne inf), $\phi: E^2\to E$ et $f: E\to E$. De plus, on note $1$ le plus grand élément de $E$ et on suppose que $\phi$ est décroissante à gauche et croissante à droite, que $f$ est involutive et que :

$$ \forall x,y: \phi(x,y) \leq \phi(f(y),f(x))$$

Dernière supposition: $\forall x: x=\phi(1,x)$.

Exercices:

1/ Prouver que $0:=f(1)$ est le plus petit élément de $E$.
2/ Prouver que $\forall x: f(x)=\phi(x,0)$

Ce paysage posé est celui de ce qu'on pourrait appeler "la prélogique", c'est à dire les axiomes que personne ne songerait à discuter car ils sont tout simplement des règles de commodité langagière scripturales et rien d'autre; Bien entendu, il faut voir $\phi$ comme l'implication et $f$ comme une sorte de négation qui sert surtout à symétriser le paysage syntaxique, à savoir "reconnaitre" à deux personnes se contredisant un rôle symétrique.

Ces propriétés ne suffisent pas à déduire la plus basique des propriétés langagières attendus dans les preuves scientifiques comme n'étant pas à justifier, à savoir l’innocuité de l'ordre dans lequel on fait les hypothèses. Or tu vois déjà que ce post est long. En plus je l'ai raccourdi en commençant directement à la logique affine (qui a consisté à dire non pas que $1$ est donné, mais qu'il est défini comme le plus grand élément)

En outre, il introduit la "difficulté", qui peut amener à une confusion ou perplexité, que $f$ est involutive.

A partir de là, pour passer de la "prélogique" à la logique, tu as deux choix bien distincts possibles.

Le premier choix consiste à ECRASER l'adversité en supposant "tout le reste de ce qu'on estime logiquement incontestable", ce qui en gros consisterait à :

- affirmer que $\phi(a,\phi(b,c)) = \phi(b,\phi(a,c))$ (commutativité)
- affirmer que $\phi(a, \hi(a,b)) = \phi(a,b)$ (duplication possible des hypothèses, ie supposer $a$ deux fois ou ne le supposer qu'une fois ne change rien
- etc (tiers exclus, autre)


Le deuxième choix consiste à ne rien supposer de plus (à part éventuellement la commutativité qui est difficile à gérer) et identifier ce qu'on pourrait appeler les phrases classiques, les phrases intuitionnistes, qui constitueraient des cas particuliers de phrases (phrases:=éléments de $E$) parmi toutes les phrases.

Ce DEUXIEME CHOIX est bien plus pertinent et fructueux car il permet une compréhension plus fine de ce qu'est une phrase SANS L'INVENTER ARBITRAIREMENT SOI MEME MAIS PLUTOT EN LE DECOUVRANT. C'est ce choix qui a été + ou - tacitement fait dans les recherche récentes fines sur la correspondances de Curry Howard and co.

Pour bien t'approprier tous ces trucs, tu aurais en quelque sorte un "manuel entier à étudier dans la paix et à feu doux". Je ne te présente dans la suite que les conclusions qui ont émergé de tout ceci. Vois-les comme des conclusions heuristiques profondes difficiles à justifier courtement.

Conclusions "like-racontées-par-Huber-Reeves-likre"

1/ Il n'y a bien qu'une seule implication et elle n'a pas d'adjoint. L'usage est de la noter $\multimap$ même si quand je vulgarise sur le forum, je ne le fais pas.

2/ Ce n'est pas celle qu'on utilise habituellement. Celle qu'on utilise habituellement en est en quelque sorte assez proche, et voilà la relation qu'elles entretiennent entre elles:

$$ (a\to b) = (a^\infty \multimap b) $$

3/ Une phrase $a$ est dite intuitionniste quand $a^\infty = a$. Dès lors, si on s'en fiche des logiques plus faibles, on peut les identifier.

4/ Il y a deux "et" profondément différents.

4.1/ Le "et" de "avec un euro tu peux t'acheter, au choix, un café, un petit chocolat, ou croissant". Ce "et" est la borne inférieure toute bête, je le noterai $\wedge$, et on a :

$$ (a\wedge b):= inf(a,b) $$

4.2.1/ Le "et" en quelque sorte additif de "dans mon sac, je possède un lingo d'or PLUSSS une montre en bois PLUSSS un billet de 50 euros".

Ce deuxième "et", que je vais noter $+$ (la notation est littéralement hérétique, c'est le cas de le dire) a une relation harmonieuse qui ressemble à une adjonction avec l'implication première, qui est la suivante:

$$ [(a+b) \multimap c] = a\multimap (b\multimap c) $$

4.2.2/ Une remarque "sympa" est qu'il est définissable: $(a+b):=$ la borne inférieure quand $x$ parcourt $E$ des $(a\multimap (b\multimap x))\multimap x$.

5/ Par dualité, en utilisant $f$, tu as donc deux "ou" qui sont profondément différents.

6/ La terminologie est souvent multiplicative, c'est pourquoi j'ai notée $a^\infty$. $a^3$ voudrait dire $a+a+a$. Un sac dans lequel tu as 3 garanties de $a$.

7/ Dans ce contexte l'involution $f$ qui ressemble à vue de nez à la négation ne doit pas être confondue avec ce que les raisonnements mathématiques considèrent comme telle. Cela provient de ce que $f(x)$ est juste $x$ vu par l'adversaire de celui qui le défend alors que $x$ est $x$ vu par son défenseur.

8/ Mais les raisonnements ne sont pas du tout symétriques puisque le sceptique y est presque le roi absolu, tandis que le prouveur y accomplit un rôle d'esclave tel que défini dans l'allégorie de Hegel


9/ Tout ceci nous amène au fait qu'il y a deux "non". Il y a la fonction primordiale $f$, qui ne joue en fait aucun rôle célèbre dans les logiques fortes, car on ne l'évoque même pas. Et il y'a le "non(x)" défini en quelque sorte comme le plus grand des $y$ tel que X+Y fait monter au paradis. Ce "non" est très facile à définir, c'est :

$$ (non(x)) := f(x^\infty) $$

pour qui , évidemment, si $x$ est intuitionniste, tu as l'égalité $f(x) = non(x)$. Sauf que ATTENTION:

10/ Est-ce que d'après toi, il est obligatoire que si une phrase est intuitionniste, c'est à dire si $x^\infty=x$ alors sa négation, ou l'une des deux négations envisagées l'est? (Exercice).

11/ Voilà, j'ai essayé de t'introduire à l'ampleur et le subtilité des réflexions qui peuvent t'occuper une année. J'en viens maintenant à ta question à un niveau plus "populaire":

P1/ La définition consensuelle de "non" est que $non(x)$ est le plus grand $y$ tel que $x\to (y\to Tout)$ est SUPERVRAI . Je reprends ici, puisque j'ai repris l'ascenseur pour descendre au 1er, la notation $\to$ et je n'utilise plus $\multimap$.

P2/ De manière générale, $(a\to b)$ est le plus grand $x$ tel que $a\to (x\to b)$ est SUPERVRAI

P3/ Dans ces deux définitions, tu vois qu'on renvoie toujours à une sorte de notion première qui est ou bien qu'il y a un ordre (où on dirait que $(a\to b)$ est supervrai ssi $a\leq b$), ou bien qu'il y a une valeur "supervraie"

P4/ C'est un exercice élémentaire de voir que dans ce cas, tu as $non(x)=(x\to [Superfaux])$

P5/ Tu peux avoir l'impression qu'il y a des trous. Et bien sache que non, ces trous sont des LIBERTES dans lesquelles tu peux t'engouffrer pour explorer les choses comme tu veux. Je t'ai juste "honnêtement" au sens où je n'ai pas voulu excessivement simplifié, donné de quoi moudre du grain. Mais tu peux retenir que:


Z1/ $non(x)=(x\to 0)$ est un théorème dans TOUTES LES LOGIQUES

Z2/ Que seule la question de savoir si $0$=Tout$ ou pas peut varier dans les logiques très faibles

Z3/ Que face à des étudiants, même chevronnés, s'il n'est pas question de logique, tu peux te simplifier en disant que c'est une définition et donner la "petite preuve orpheline" que j'ai donnée (qui persuade toute personne ne bonne fois que cette définition doit être perçue comme un théorème à ceci près que comme on est en amont, il serait malhonnête de faire semblant de croire qu'il préexisterait un théorie formelle sérieuse dans laquelle on arriverait à cette conclusion par déductions formelles prononcées le menton relevé.

christophe c

Si tu veux connaitre les notations officielles:

$\wedge$ se prononce "avec"

$+$ se prononce et s'écrit $\otimes$

$a^\infty$ est plutôt noté $(!a)$

$x\multimap y$ est $\phi(x,y)$ du début du post

$f(x)$ s'écrit plutôt $x^\perp$.

Thierry Poma

Bonjour Christophe

Voudrais-tu me donner une ou plusieurs références pour ceci, s'il te plait ? Je t'en remercie par avance.

Amicalement,

Titi

christophe c

J'ai mixé de nombreuses recherches récentes. Il n'existe probablement pas de livre traitant "tout d'un coup".

Peut être faire comme Foys il y a quelques années: prendre UN DES thèmes et l'étudier sérieusement. De la, ensuite "se libérer" et villegiaturer.

J'ai écrit tout le post pour montrer qu'en amont à dom on n'a plus de réponses univoque honnête. Cela dit il savait déjà l'essentiel.

Sous la logique intuitionniste il faut "se brusquer" et entrer dans la CCH pour profiter du sujet.

Perso je n'ai pas "capté" tout ça par des livres mais en exécutant 100 fois la CCH sur CAML. Une fois le sujet maîtrisé ça a l'air de rien mais je ne peux pas savoir l'ampleur des déconstructions utiles pour l'ingerer ayant eu en plus l'avantage de déconstruire pour la MQ et... pour ma vie perso aussi souvent.

Thierry Poma

@Christophe :

Je te remercie. Mais, n'y aurait-il pas un lien, s'il te plait ? un simple lien.

christophe c

De mon téléphone. Quand je serai sur mon pc j'essaierai de te satisfaire

Dom

Et au sujet de la définition de « non » qui n’est pas « implique tout » ?
Par rapport au tabou ambiant qui fait peur ? Une suggestion ?
C’est ici que ça a commencé : http://www.les-mathematiques.net/phorum/read.php?16,2091964,2092198#msg-2092198

Merci pour le temps que tu as mis au sujet de la FI et des théorèmes nécessitant RPA.
Je ne sais pas si je vais regarder ça tout de suite.

claude quitté

Dom
Elle est bizarre ta négation ``Je ne sais pas si je vais regarder ça tout de suite''. Est ce que cela ne serait pas plutôt ``Je crois que je ne vais pas regarder ça tout de suite'' ?

Dom

En effet, une façon polie sous forme de litote qui veut dire : "je sais que je ne vais pas regarder tout de suite".

Martial

Et moi je sais que je ne sais pas si demain matin je saurai si je vais regarder ça tout de suite.

Cette phrase étant prise comme axiome on peut en déduire un seul théorème : Pour aujourd'hui, c'est mort !

Dom

Martial,
Par pitié vend la mèche sur ce qu’est la définition de « non(P) ».
Christophe avait dit que c’était « P->tout ».
Mais il a nuancé dernièrement. C’est maintenant un théorème.

Thierry Poma

@Dom : bonsoir. En vertu de ceci, $\vdash_m\,\neg\,\phi\leftrightarrow(\phi\rightarrow\perp)$, d'où (purement linguistique) $\vdash_i\,\neg\,\phi\leftrightarrow(\phi\rightarrow\perp)$ et $\vdash_c\,\neg\,\phi\leftrightarrow(\phi\rightarrow\perp)$ également. Dit autrement, si $u\in\{m,\,i,\,c\}$, $\vdash_u\,\neg\,\phi\leftrightarrow(\phi\rightarrow\perp)$. Précisons que $m$ tient pour "logique minimale", $i$ pour "logique intuitionniste" et $c$ pour "logique classique".

Le symbole $\top$ signifie "toujours vraie," alors que $\perp$ signifie "toujours faux". C'est ce que je viens de lire dans Modal Logic for Open Minds de Johan van Benthem, page 11.

Dom

Je n’ai pas le bagage pour lire ceci même si ce forum m’a déjà proposé ce genre de choses.
« Sous les hypothèses, etc. ».

On dit dans ce fil :

1) $\phi\rightarrow\perp$ n’est pas la définition de $\neg\,\phi$

2) on démontre que : $\neg\,\phi\leftrightarrow(\phi\rightarrow\perp)$

Alors ou bien j’ai mal compris ou bien ça ne me dit toujours pas ce qu’est $\neg\,\phi$ bien que ce soit équivalent à $\phi\rightarrow\perp$

raoul.S

@Dom je ne comprends pas bien ton problème. $\neg\,\phi$ est juste une formule (un mot vérifiant certaines conditions) de la logique du premier ordre, et n'a pas de sens en soit. Qu'est ce que tu entends par "définition de $\neg\,\phi$" ?

Tu peux penser à $\neg\,\phi$ comme à "non phi" ou phi est une autre formule (qui est susceptible de prendre les valeurs vrai ou faux).

Les formules sont des mots particuliers, et les démonstrations sont "des enchaînements" (des arbres plutôt) de formules qui respectent certaines règles. Mais à ce niveau il n'y a aucune interprétation.

Par exemple le post de Thierry POMA ICI est la démonstration de la formule (mot) : $\neg\,\phi\leftrightarrow(\phi\rightarrow\perp)$. Tu peux penser à cette dernière formule comme à "$\neg\,\phi$ est équivalent à $\phi\rightarrow\perp$".

C'est tout.

Franchement si tu veux vraiment avoir une introduction à ce genre de trucs je te conseille un bouquin comme Introduction à la logique, théorie de la démonstration. Tu comprendras tout en lisant les premières pages. J'ai la première édition d'ailleurs (jamais terminé... 8-)).

Dom

En effet il doit me manquer des éléments.

J'ai cru bêtement que quand on avait introduit le symbole $\neg$, alors on l'avait évidemment défini.

Je vais tenter une analogie quant à cette discussion :

-ABCD est un parallélogramme est équivalent à [AC] et [BD] ont le même milieu. Mais ce n'est pas la définition d'un parallélogramme.
-Mais alors qu'est-ce qu'un parallélogramme ?

Bon, j'irai jeter un oeil dans la littérature comme tu fais bien de me le conseiller.

Foys

Dom a écrit:

On dit dans ce fil :

1) $\phi \to \perp$ n’est pas la définition de $\neg \phi$

Cela dépend des auteurs et des façons de l'introduire.
Dans la correspondance de Curry-Howard et ses dérivés (y compris la réalisabilité classique), il n'y a pas du tout de négation à la base. Celle-ci est bel et bien construite (i.e. définie) indirectement par cette formule (non A := A implique tout). C'est ce qui est pratiqué dans les prouveurs comme COQ.

Cela étant dans tous les cas il y a au moins équivalence.

Dom

Ok Foys.
« Cela dépend des auteurs » : Il reste à trouver un auteur qui ne le fait pas comme ça, ni comme la correspondance de C.H.

Peut-être que Christophe avait autre chose en tête également.

Bonne nuit.

raoul.S

@Dom j'ai trouvé ce PDF d'Antoine Chambert-Loir "Logique du premier ordre". Tu peux lire quelques pages à partir de la 17 pour te faire une idée plus précise.

Dom

Merci !

Martial

@Dom : sans vouloir me faire de la pub je te conseille de lire le paragraphe de mon chap 4 consacré à la LI (pages 67 et suivantes). C'est très élémentaire et ça va te prendre 1/4h 20mn maxi.

https://sites.google.com/view/martial-leroy

Perso quand je parle de LI (ce qui est assez rarissime), dans le langage de base je mets $\perp$ mais pas $\neg$. Et ensuite je considère que $\neg A$ est un "raccourci" pour $A \rightarrow \perp$, où $\perp$ désigne"le faux" ou "Tout", comme tu veux.
Dans mon exposé, $\neg A = A \rightarrow \perp$ est donc une définition.
Dans le post initial de Christophe, comme il n'utilise que les symboles $\rightarrow$, $0$ et $1$, ça semble effectivement être un théorème... mais c'est vrai qu'il ne définit pas $\neg A$ de façon formelle

christophe c

De mon téléphone dom:

Je le redis pour les gens qui sont sur des logiques fortes on a LES DEUX ce qui est encore mieux.

Si on veut on peut annoncer que c'est une définition.

Mais SI ON VEUT on peut ajouter le symbole non comme notion premiere et PROUVER que non X c'est pareil que X=>tout.

J'ai déjà mentionné cette preuve 3615 fois.

Ce "avoir les 2" semble te perturber dom. Mais il n'y a pourtant pas de quoi.

christophe c

J'appelle forte une logique quand elle admet que

A implique (A et A)

Autrement dit celles de 99.9% des matheux non logiciens.

gai requin

Mais cette preuve de $\neg X\leftrightarrow (X\rightarrow\perp)$ utilise le tiers exclus. ;-)

Thierry Poma

La [méta-]preuve que j'ai déposée ici n'utilise pas le principe du tiers exclu ; elle est valable en logique minimale, en logique intuitionniste et en logique classique.

Thierry Poma

Ci dessous se trouve la liste des règles de la logique minimale, extraite du livre La logique, pas à pas, page 194. Je conseille vivement ce livre que j'ai découvert la semaine dernière. Pour la lecture de chaque règle (à l’exception de l'axiome), l'on pourra vous y aider...

Jean-Louis

Cher Thierry, j'ai lu dans une présentation du livre dont tu parles que "il est conçu pour les étudiants entretenant une relation conflictuelle avec les sciences" qu'il s'agit "de mettre la logique à la portée de tous, en particulier des non mathématiciens" .D'après toi, à quel niveau se situe-t-il vraiment?
Merci à toi.
Cordialement.
Jean-Louis.

Martial

@Thierry : tu vas dire que je suis chiant, mais dans ton dernier tableau je n'arrive pas à lire les petits zizis qui sont à droite des traits de fraction...

Martial

@Thierry : laisse tomber, j'ai trouvé une solution plus simple, lol

Martial

@Thierry : il eût fallu que je susse qu'il pût exister un ouvrage aussi génial !

@Christophe : je commence à comprendre pourquoi tu as autant de considération pour Jacques Duparc.

@Tous : rien à voir, mais je viens de lire les deux articles de Penelope Maddy : "Believing the axioms I & II", que je conseille d'ailleurs à tout le monde.
Ce que je veux dire c'est qu'après ça ça fait du bien de voir un beau livre écrit dans la langue de Molière.

christophe c

@GR qui écrit

http://www.les-mathematiques.net/phorum/read.php?16,2091964,2093042#msg-2093042

Pas du tout!!!

Je te les répète en ligne, mais tu aurais pu mieux lire:

nonA
1=>nonA
non(nonA)=>non1
A=>non1
A=>0

---

A=>0
non0 => nonA
nonA



Si tu penses à "0 = non1" dis-le.

christophe c

Remarque : de façon générale, d'ailleurs, dans un ordre où deux éléments ont une borne inf, où il y a un plus petit élément $0$ et où pour tout $x$, il y a un plus grand élément nommé $non(x)$ tel que $\inf(x,non(x)) = 0$, tout "adjoint" même potentiel de inf vérifiera ça.

Pour les lecteurs autres que GR, adjoint $\sigma$ de inf veut dire, $\forall x,y,z:$ que
$$ \inf(x,y) \leq z \iff x\leq \sigma(y,z).

$$ Tu as alors par définition que
$$ \inf(x,y) \leq 0 \iff x\leq \sigma(y,0)

$$ La tradition a été de noter $a \Rightarrow b$ à la place de $\sigma(a,b)$, mais la pauvreté des axiomes n'en change pas.

gai requin

@cc : C'est-à-dire que quand un long post commence par :
4.2/ Pour toute phrase $x: (1/\to x)=x$ :-S, j'ai des doutes sur la suite et j'arrête de lire.