Intuitionnisme.

Jean-Louis: il y a des situations où le tiers exclu n'est pas intuitif.
Par exemple, si je te disais que (en acceptant le tiers exclu) j'ai la capacité d'écrire un algorithme en quelques minutes, sur mon ordi à moi dans ma chambre, qui retourne "oui" si l'hypothèse de Riemann est vraie, "non" sinon, tu me croirais ?
Bah pourtant c'est le cas si tu m'autorises le tiers exclu, et je pourrais te le prouver.

L'intuitionnisme exige essentiellement que (A,B étant des énoncés) prouver "A ou B" revienne exactement à prouver A ou à prouver B.

Maxtimax a écrit:

Jean-Louis: il y a des situations où le tiers exclu n'est pas intuitif.
Par exemple, si je te disais que (en acceptant le tiers exclu) j'ai la capacité d'écrire un algorithme en quelques minutes, sur mon ordi à moi dans ma chambre, qui retourne "oui" si l'hypothèse de Riemann est vraie, "non" sinon, tu me croirais ?
Bah pourtant c'est le cas si tu m'autorises le tiers exclu, et je pourrais te le prouver.

("Prouvable/non prouvable" serait peut-être mieux que vraie ou fausse).
Un sorcier capable de voyager dans le temps procèderait comme suit:
Il annonce au monde qu'il a un tel programme (print "non"). Puis si quelqu'un un jour proteste en lui montrant une preuve de RH, il retourne au moment de l'annonce et remplace son programme par print "oui".
(les travaux sur la réalisabilité classique on montré qu'il était possible de rajouter le tiers exclu à la correpondance de Curry-Howard avec des gestions d'exception et des sauvegardes).

Maxtimax a écrit:

Par exemple, si je te disais que (en acceptant le tiers exclu) j'ai la capacité d'écrire un algorithme en quelques minutes, sur mon ordi à moi dans ma chambre, qui retourne "oui" si l'hypothèse de Riemann est vraie, "non" sinon, tu me croirais ?
Bah pourtant c'est le cas si tu m'autorises le tiers exclu, et je pourrais te le prouver.

@Maxtimax tu pourrais m'expliquer comment tu utilises le tiers exclu ici stp car je ne vois pas.

@gai requin : Je ne suis pas modérateur mais sincèrement je ne pense pas que tes propos méritent un bannissement du forum, il n'y a rien d'infâmant là-dedans..
Par contre je pense qu'ils méritent une remarque musclée du genre : "Tu es complètement à côté de la plaque et tu écris n'importe quoi !"
A ma connaissance les travaux de Gödel n'ont RIEN A VOIR avec l'intuitionnisme !!!

@Maxtimax : j'attends avec impatience ta preuve du truc avec l'ordi sur ton pieu...

@gai requin: ce n'est pas tout à fait ça, le principe (l'interprétation de Brouwer-Heyting-Kolmogorov qui est devenue plus tard la correspondance de Curry Howard) consiste à dire que:
(i) en gros un énoncé est assimilé au nom de l'ensemble (ou du type) de ses preuves
(ii)Une preuve de $A\wedge B$ est un couple $(p,q)$ où $p$ est une preuve de $A$ et $q$ une preuve de $B$ (donc d'après (i): $A\wedge B = A \times B$)
(iii)Une preuve de $A\Rightarrow B$ est une fonction-comprendre ici un programme dans un langage fonctionnel- transformant infailliblement toute preuve de $A$ en une preuve de $B$ (autrement dit, via (i): $A\Rightarrow B = B^A$)
(iv)Une preuve de $A\vee B$ est un couple $(\varepsilon,r)$ où $\varepsilon=0$ et $r$ est une preuve de $A$, ou bien $\varepsilon=1$ et $r$ est une preuve de $B$ (en gros: $A\vee B = A \coprod B$)
(v)$\perp$ est un énoncé qui dit intuitivement "tout est vrai" ce qui se traduit formellement par l'existence pour tout énoncé $A$,d'une preuve $abs_A :\perp \Rightarrow A$
(vi) pour tout énoncé $A$, $\neg A$ abrège $A \Rightarrow \perp$
(vii) $\forall x\in E, A(x) = \prod_{u \in E} A(u)$ (généralise (ii))
(viii) $\exists x\in E, A(x) = \coprod_{v \in E} A(v)$ (généralise (iv))

Par exemple:
-si $A,B,C$ sont des énoncés, la curryfication (application qui à $f:A\Rightarrow (B\Rightarrow C)$ fait correspondre l'application qui à $(x,y) \in A \times B $ fait correspondre $f(x)(y)$) est une preuve de $(A\Rightarrow (B\Rightarrow C)) \Rightarrow ((A\times \Rightarrow C)$, son opération inverse est la preuve de la réciproque.

-la composition des applications, i.e. l'application $f\mapsto (g \mapsto g \circ f)$ ,est une preuve du syllogisme $(A \Rightarrow \Rightarrow ((B \Rightarrow C) \Rightarrow (A \Rightarrow C))$.

-en posant $C:=\perp$ dans l'exemple ci-dessus on retrouve compte tenu de (vi) une preuve de la contraposition $(A \Rightarrow \Rightarrow ((\neg \Rightarrow (\neg A))$.

***********

En revanche étant donné un énoncé $A$ , il n'existe en général, dans le système décrit ci-dessus, aucune preuve de $A\vee \neg A$, en fait aucune preuve de $A \vee (A \Rightarrow $ pour un autre $B$ quelconque (alors qu'il s'agit d'une tautologie du calcul propositionnel).

C'est à la suite de travaux datant des années 90 (Tim Griffin) que la correspondance de Curry Howard a pu être modifiée à l'aide de mécanismes de gestion d'exceptions pour inclure le tiers exclu. Une possibilité est la suivante:
On a un programme $p$ de type $A \vee (A\Rightarrow $ qui fait lorsqu'on l'appelle une sauvegarde $e$ de l'état du système puis renvoie un objet $k:A\Rightarrow B$ dont le comportement est le suivant: si on l'appelle sur un objet $x$ de type $A$, il sauvegarde $x$, puis arrête le système et rétablit la sauvegarde $e$ et retourne $x$ de type $A$.

C'est pour ça que quand vous pouvez voyager dans le temps(!!!), même si vous êtes nul en maths vous pouvez retourner un programme qui dit oui si RH est prouvable et non si elle n'est pas prouvable: le programme d'une ligne "afficher <<non>>" convient: si RH n'est jamais prouvée vous avez raison et si elle l'est vous revenez au moment où vous promettez d'avoir un tel programme et vous livrez "afficher <<oui>>" à la place. On gagne à tous les coups.

Jean-Louis a écrit:

D'après Wikipédia, pour Brouwer les objets mathématiques doivent être accessibles à l'intuition. Or qu'y a-t-il de plus intuitif que le tiers exclu ?

Je trouve le tiers-exclus très contre-intuitif. Pour gagner de la place dans la suite, je note P l'hypothèse du continu. Avec le tiers-exclus, je ne peux pas prouver P, je ne peux pas prouver non(P), mais je peux prouver P ou non(P).

C'est une règle conventionnelle comme une autre qui ne me choque nullement, mais qui ne correspond pas à mon intuition première (même s'il est possible de modifier ses intuitions avec un peu de motivation, mais c'est là une encore autre affaire).

raoul.S : aucun souci, voici :

Si l'hypothèse de Riemann est prouvable [avec une modification de Foys, merci !], alors je suis capable d'écrire ce programme : j'écris l'équivalent de "print ' oui' " dans mon langage préféré

Si l'hypothèse de Riemann n'est pas prouvable, alors je suis capable d'écrire ce programme : j'écris l'équivalent de "print 'non' " dans mon langage préféré.

Que l'hypothèse de Riemann soit prouvable ou non, je suis capable d'écrire un tel programme. Donc [c'est dans ce "donc" que ce cache le tiers exclu] je suis capable d'écrire un tel programme (le même argument marche avec l'existence de dieu en admettant que la question ait un sens, si on veut la présenter à un public plus large)

On voit que c'est un peu ce qui a été expliqué au dessus : le problème dans ce que je raconte est que je teste $A\lor \neg A$ sur un $A$ dont il m'est impossible (pour le moment :-D) de déterminer la valeur de vérité, j'obtiens donc quelque chose sans "témoin", quelque chose que je ne peux pas tester: ici je suis capable d'écrire le programme, mais je ne sais pas lequel c'est !

Si on n'est pas convaincu on pourra se rappeler de la règle suivante qui gère "ou" : Si $A\vdash C, B\vdash C$ ($P\vdash Q$ se lit approximativement "à partir de $P$ on prouve $Q$", ou quelque chose dans ce goût), alors $A\lor B \vdash C$; ainsi que : si $A\vdash B$ et $\vdash A$ alors $\vdash B$. En particulier, ici j'applique tout ça : "HR est prouvable $\vdash$ je peux écrire le programme", "HR n'est pas prouvable $\vdash$ je peux écrire le programme" et "$\vdash$ HR est prouvable ou ne l'est pas".

En logique intuitionniste, ce genre de phénomène n'apparaît pas, une preuve apporte avec elle un "témoin", autrement dit un "contenu computationnel" (Foys dit qu'on peut étendre la correspondance de Curry-Howard à la logique classique, donc étendre cet aspect "contenu computationnel", et j'ai aussi déjà vu ça, mais c'est avec différentes modifications du sens de cette expression) : en particulier quand une preuve affirme l'existence de quelque chose, on peut extraire de la preuve un témoin de cette existence. C'est un sens en lequel elle est "plus intuitive" que la classique (où on peut affirmer "truc existe" sans exhiber truc)

(PS: si ça amuse Martial j'étais effectivement dans mon lit pour écrire ça :-D)

Merci Foys et merci Maxtimax

Maintenant j'ai compris X:-(

Du coup l'affirmation "il existe un programme tel que si RH alors il affiche oui et si (non(RH)) alors il affiche non" qui m'avait l'air surprenante avant ne l'est plus maintenant :-(

À l'époque j'avais acheté ce bouquin et j'ai relu rapidement les premières pages qui parlent des séquents, et effectivement à la page 40 il y a le tiers exclu que vous avez appliqué :

"HR est prouvable" $\vdash$ "je peux écrire le programme", "HR n'est pas prouvable" $\vdash$ "je peux écrire le programme" donc, $$\vdash \text{"je peux écrire le programme".}$$

Yes, Je peux écrire ce programme !!!!

Merci Foys !

J'ai essayé de comprendre $(A\Rightarrow (B\Rightarrow C)) \Rightarrow ((A\times \Rightarrow C)$.
Il s'agit de montrer qu'il existe une application $\varphi$ de $(A\Rightarrow (B\Rightarrow C))=(C^B)^A$ dans $((A\times \Rightarrow C)=C^{A\times B}$.
Soit $f\in (C^B)^A$. $f$ est une application $A\to C^B$ donc pour tout $x\in A$, $f(x)\in C^B$, i.e. $f(x)$ est une application $B\to C$.
Donc, pour tout $y\in B$, $f(x)(y)\in C$.
Ainsi, $\varphi:f\mapsto ((x,y)\mapsto f(x)(y))$ convient.

De même, l'application qui à $x\in A$ associe l'application $f\in\perp^A\;\mapsto f(x)$ est une preuve de $A\Rightarrow \neg\neg A$.
Et j'imagine qu'on n'a pas de preuve de $\neg\neg A\Rightarrow A$. :-)

@CC
1. J'ai ``peur'' que dans tes explications d'un PC, tu restes (sans le vouloir) dans ton monde, avec peut-être le bilan que je vais rien comprendre. Mais attendons.

2. Quel est le statut de l'énoncé ``il existe 2 irrationnels strictement positifs $a,b$ tels que $a^b$ soit rationnel'' en logique intuitionniste ? D'ailleurs, est ce que cette phrase que je viens d'écrire a un sens ?

3. Mais pourquoi que les autres (plus disponibles ?) ne m'ont rien dit sur le fait que je faisais un hors-sujet (j'avais d'ailleurs prévenu) ? Ils auraient pu par exemple prendre le temps d'avertir un modérateur pour dire que C.Q. trolle encore sur un fil de logique, non ?

Claude, pour ton 2 : il y a d'autres preuves plus directes de ton machin, qui sont plus constructives - tu exhibes $a,b$ explicites en jouant avec des $\ln$ et tout, je n'ai plus pes exemples spécifiques mais ce n'eat pas compliqué.
De là à dire qu'elles sont intuitionnistes, je ne sais pas (il faut voir la construction de $\ln$ dans les différents modèles de $\mathbb R$ qui ne sont plus équivalents).

Salut Claude,

Même si on se restreint à $a$ et $b$ algébriques de degré $\geq 2$, il va être difficile de certifier que $a^b$ est rationnel.
Ok pour les entrées, bof pour la sortie.

Je suis sur un pc, mais j'ai peu de temps et de toute façon je dois "faire simple". Ces sujets ont le don de provoquer de multiples contre-sens (comme on le voit dans la totalité du fil)

Soit $E$ un ensemble dit "de phrases", ordonné** de manière complète (toute partie de $E$ a une borne inf).

** lire $a\leq b$ comme abrégeant $<<b$ est un cas particulier de $a>>$

Vous avez plusieurs niveaux de certitudes, que je décris de manière décroissante ($\to$ abrège l'implication et c'est une application de $E^2$ dans $E$).

Premier niveau:

N1.1/ il y a un élément qui s'appelle $1$ tel que $\forall x: (1\to x) = x$
N1.2/ $\forall x,y,z: ( x\to (y\to z) )=( y\to (x\to z) )$
N1.3/ pour tous $x,y: [(x\leq y)$ si et seulement si $1\leq (x\to y)]$

Ce premier niveau est assez "linguistique" dans les certitudes scientifiques et ne force pas du tout les éléments de $E$ à pouvoir être considéré comme l'ensemble des valeurs de phrases. Certes on n'est plus à un niveau "libre" (au sens de groupe libre), puisqu'on a par exemple l'égalité $((x\to y)\to (x\to y)) = (x\to ((x\to y)\to y))$, certes quasi-inoffensives, mais déjà telle qu'elle peut, pour les mal comprenants, provoquer des polémiques "nom/valeur", comme les provoque le fait que $7+3$ est un produit, puisque c'est $1\times 10$.

Par contre les axiomes de ce niveau est INCONTESTE par qui que ce soit, même les plus "étrange" psychopathes.

Deuxième niveau: là, on commence à trouver des choses que CERTAINS ETRES HUMAINS ont du mal à faire remonter au conscient (ils en sont convaincus, mais mettent du temps à prendre conscience qu'ils en sont convaincus).

N2.1/ $\forall x\in E: x\leq 1$.

Ca a comme conséquence que $\forall x,y: x\leq (y\to x)$, connu sous la description plus populaire que des hypothèses inutiles ne changent rien à la capacité de prouver ou croire aux conclusions que certaines autres entrainent.

Exemple: si $[3 = a+b$ alors $a\times 1 = a]$ n'est pas considéré comme moins sûr que $a\times 1=a$


N2.2/ Ces deux socles sont, même s'il faut un peu plus de temps, généralement considérés comme sûr par tout le monde.

Si on note $\perp$ la borne inférieure des éléments de $E$, mais le nom le plus adapté évidemment serait de l'appeler "tout", c'est à ce niveau que vit le théorème disant $non(A)$ équivaut à "A=> toute phrase"

Niveau3: Curieusement, à ce niveau 3 vit l'axiome LE PLUS PUISSANT ET DE LOIN de tous les axiomes admis par la science. Et pourtant (c'est ça la curiosité), le "peuple" l'admet PLUS FACILEMENT que le niveau 2

En termes populaires, c'est l'axiome: "(A et A) = A" que personne ne conteste et surtout que tout le monde croit à tort inoffensif. Alors qu'en fait sans lui, les maths seraient très différentes.

Techniquement, c'est $\forall x,y: [(x\to (x\to y))\leq (x\to y)]$

Niveau4: $\leq$ est isomorphe à $\geq$. (En pratique, ça revient à considérer que toute phrase vaut la négation d'une phrase, ie que l'ensemble des valeurs possibles pour une phrase n'est en particulier pas "bien fondé").

Arrivé au niveau3, en fait on a toutes les maths, et le préjugé populaire qui veut qu'il y aurait une différence de constructivité entre logique classique et intuitionniste est FAUX.

En fait, en pratique la logique intuitionniste EST PLUS COMPLEXE (propositionnellement elle est trivialement PSPACE complète, quand la classique "n'est que" NP-complète) et moins "constructive" (in somme sense) que la classique.

Le niveau4 est juste un niveau auquel "on gagne du temps" en SYMETRISANT le message qu'on espère envoyé par les extrêmes $\{\perp; 1\}$, respectivement plus petit et plus grand élément de $E$.

C'est là que s'insère la logique intuitionniste. Elle dit juste que les HYPOTHESES sont duplicables mais pas les conclusions. C'est "bêtement" un accident historique dû à notre "désir de commencer quelque part" qui n'a en fait aucun fondement.

Pour le dire autrement, la logique intuitionniste est accidentellement générée par le fait qu'il existe tout un tas de $x\in E$ tels que $\forall y\in E: y\neq x$.

En effet, il suffit que $\forall x\in E\exists y\in E: ((y\to \perp)\to \perp) = x$ pour qu'elle n'existe plus (enfin précisément ne soit plus représentée par $E$).

Elle est à comparer au refus des nombres irrationnels en 1000 avant JC et toute sorte d'addictions similaires.

Attention, je n'en fais pas une critique négative et elle est bien strictement incluse dans la classique en termes de théorèmes, donc bien évidemment qu'une preuve intuitionniste EST UN CAS PARTICULIER de preuve classique. Elle n'est pas "étrangère".

Prenons maintenant un espace topologique connexe et deux ouverts non vides disjoints $U,V$. Et bien personne ne s'évanouit devant la remarque que $U\cup V$ NE PEUT PAS valoir l'espace entier.

Pour TRES EXACTEMENT LES MËMES RAISONS SEMANTIQUES, certaines phrases $p$ sont "inrecouvrables" et vérifient, si on s'en tient à l'intuitionniste $\forall x:\ [$ si $p\leq (x\vee \neg x)$ alors $((p\leq x)$ ou $(p\leq \neg x))]$.

Cet "accident" a provoqué de gros remous et donné le préjugé (complètement faux en général) qu'il s'agit d'une forme de constructivité. La réalité est beaucoup moins sexy, comme le montre le fait que $(x\vee \neg x) \leq (x\vee \neg x) $ sans pour autant que $[(x\vee \neg x) \leq x]$ ou $[(x\vee \neg x) \leq (\neg x) ]$

Pour conclure, elle est passionnante et en termes de "temps de vie à être étudiée intensément", elle dépasse ses jeunes soeurs (logique linéaire (que le niveau1) et logique affine (niveau 1+2)).

Pour revenir à ce qu'a dit Claude, et même si je sais que l'exemple qu'il prend est présenté (c'est quasiment toujours le même) 100000 fois dans l'enseignement supérieur pour illustrer ce thème, il faut bien rappeler que c'est une question de FORME DE PREUVES et non de "contenu sémantique sensé".

Le fait que [($a$ est rationnel) ou ($a$ n'est pas rationnel)] est un axiome classique, mais pas intuitionniste est FORMELLEMENT administratif. C'est juste "vrai" (il suffit de consulter les listes respectives d'axiomes de ces logiques (ou de règles démonstratives de ces logiques) pour le "constater administrativement")

Mais les exemples ne sont pas parlants car jouent sur un oubli totalement accidentel:



est une duale parfaitement respectable des exemples courant de enseignants non logiciens en L2 et pourtant c'est un théorème tout ce qu'il y a de plus parfaitement intuitionniste

* Vous pouvez aussi penser à $non(a \in \Q$ et $a\notin \Q)$


Abréviations:

Aux niveaux 1 et 2, il y a 2 et et deux ou

Ils collapsent à partir du niveau 3

A (et1) B est l'abréviation de $<<$ la borne inférieure des éléments de $E$ suivants $(A\to (B\to x))\to x$ quand $x$ parcourt $E>>$

A (et2) B est juste $inf(\{A;B\})$

A (ou1) B est l'abréviation de $<<$ la borne inférieure des éléments de $E$ suivants $((A\to x)\to ((B\to x)\to x))$ quand $x$ parcourt $E>>$

A (ou2) B est juste $sup(\{A;B\})$

Sur un plan historique, on s'est perçu (correspondance de Curry Howard) que Preuves = Programmes. C'est souvent mal dit et présenté comme une inclusion à tort: $Preuves\subset Programmes$.

Le préjugé de constructivité de la logique intuitionniste avait conduit à écarter l'axiome non intuitionniste (ie les formes équivalentes : TE; nonnon=id). Mais c'était un déni PUREMENT PSYCHOLOGIQUE. Dans les faits, c'était juste une erreur (un peu comme quelqu'un qui a payé ses shoes 700E a plus de mal à penser qu'on en obtient des vraies à 40E aux puces et préfère croire que les puces est un vaste marché illégal organisé en toute lumière et avec pignon sur rue dans le nord de Paris)

Ca a permis à un scientifique nommé Timothy Griffin de devenir l'idole à égalité avec Godel de notre contemporain Jean-Louis Krivine qui considère sa découverte comme aussi importante que celle de Godel.

La découverte que l'axiome du tiers exclu est "tout autant" programmable que le reste des axiomes de la science est la suivante:

Vous disposez d'une stratégie qui connaissant le digicode de la porte qui permet de passer du lieu $(A\to Paradis)$ au lieu $Paradis$ est capable de vous emmener au paradis à coup sûr.

Et bien à partir de là, vous avez un moyen***** d'aller dans le lieu A: il suffit de donner n'importe quel code (qui n'a aucunement besoin d'être valable) à votre stratégie, et "elle gueulera"*** seulement quand vous serez arrivé dans A, taperez sur le digicode de la porte qui vous mène au paradis et vous apercevrez.... que ce digicode n'est pas le bon.

*** enfin c'est vous qui "gueulerez, si vous vouliez aller au paradis. Mais vous êtes arrivé dans A



En pratique, c'est juste "try .... finally ..." à la place de "begin ... end" (c'est juste un "goto" qui évite de perdre du temps.

***** je donne une "preuve" de l'axiome non intuitionniste ((A=>Paradis)=>Paradis)=>A

Poirot : j'ai trouvé plus simple ! (il n'est pas de moi par contre) : $\sqrt{10}^{\log(4)}$ ! $\sqrt{10}$ est facilement irrationnel, $\log (4) = \frac{\ln(4)}{\ln(10)}$ aussi (même argument que $\frac{\ln(2)}{\ln(3)}$ et $\sqrt{10}^{\log(4)} = 10^{\log(2)} = 2$

J'avais vu une fois, je ne sais plus où, l'exemple trivial $\sqrt{2}^{2log_{2} {3}} = 3$

@foys@cc : Je n'y comprends plus rien ! :-S
A-t-on une preuve intuitionniste de $\neg\neg A\Rightarrow A$ ?

gai requin a écrit:

A-t-on une preuve intuitionniste de $\neg \neg A \Rightarrow A$?

Non.
Tu peux consulter ce fil http://www.les-mathematiques.net/phorum/read.php?16,1859928 pour une autre interprétation des énoncés de la logique intuitionniste, qui permet de répondre à ce genre de question (les ouverts d'un espace topologique $X$ sont vus comme des énoncés avec, étant donnés deux ouverts $V,W$, $V \wedge W := V \cap W$, $V\vee W:= V \cup W$, $V \Rightarrow W := \text{intérieur de } (W \cup (X \backslash V))$, $\perp := \emptyset$ et $\top := X$). Les théorèmes intuitionnistes sont égaux à $X$ tout entier.

Si $\neg \neg A \Rightarrow A$ était prouvable, en gros on aurait pour tout espace topologique $X$ et tout ouvert $V$ de $X$, l'inclusion $n(n(V)) \subseteq V$ avec $n(U):= \text{intérieur de } (X \backslash U)$.
Ceci est démenti par le cas où $X=\R$ et $V:= \R \backslash \{0\}$.

@Foys : Merci pour cette autre interprétation avec laquelle $\neg\R \setminus \{0\}=\emptyset$.
Est-ce que cela signifie qu'on ne peut pas construire un programme avec un nombre réel $x$ en entrée et qui réponde à la question de savoir si on a $x=0$ ? Grosso modo, la machine se trompe pour $x$ non nul suffisamment proche de $0$.

Merci Foys pour avoir exposé ce cadre unifié avec moult détails !
Pour être honnête avec toi, je n'y connais pas grand chose en catégorie mais c'est peut-être l'occasion pour moi d'y jeter un œil plus aiguisé. :-S
Je reviendrai vers toi dès que possible pour l'exo borne supérieure implique borne inférieure...

Il ne s'agit pas du tout d'un cas d'évidence : si c'est le cas, saurais-tu le prouver ? Ou donner une procédure qui décide, étant donné un nombre réel, s'il est positif ou (négatif ou nul) ?

@christophe c: les abréviations $0:=\emptyset$ et $1:=\{\emptyset\}$ ne sont pas connues de tout le monde...