David Madore's WebLog: 2024-07

L'ensemble ℕ des entiers naturels, et diverses formes de récurrence

Comme en maths classiques, il y a plusieurs approches fondationnelles pour faire apparaître l'ensemble des entiers naturels, mais il faut forcément postuler quelque chose (au moins l'existence d'une sorte d'ensemble infini) ; si on aime le point de vue ensembliste, pourra identifier, comme proposé par von Neumann, 0 avec ∅, 1 avec {0}={∅}, 2 avec {0,1}={∅,{∅}}, 3 avec {0,1,2}, etc., mais il est sans doute préférable de traiter les entiers naturels comme « atomiques » : je n'ai pas envie de rentrer dans ces considérations-là. Toujours est-il que, d'une manière ou d'une autre, on va vouloir postuler ou démontrer que :

Il existe un ensemble noté ℕ et appelé ensemble des entiers naturels, muni d'un élément 0∈ℕ (appelé zéro) et d'une fonction S:ℕ→ℕ (la fonction successeur), vérifiant le principe de récurrence :

‣ Si E est un ensemble quelconque, e∈E un élément et f:E→E une fonction, alors il existe une unique u:ℕ→E telle que u(0) = e et u∘S = f∘u (c'est-à-dire u(S(n)) = f(u(n)) pour tout n∈ℕ).

On dit alors que u est construite par récurrence par itération de f à partir de la valeur initiale e. (Concrètement, u(0)=e, u(1)=f(e), u(2)=f(f(e)) et ainsi de suite.)

Comme en maths classiques, il existe toutes sortes de variations autour de ce principe de récurrence. Celui que je viens d'énoncer est un principe de récurrence « catégorique » ou « universel » (parce qu'on peut le décrire de façon savante en théorie des catégories) ; mais on peut en déduire d'autres principes peut-être plus familiers, comme les suivants (ce que je raconte ci-dessous n'est pas spécialement liée aux maths constructives, mais comme je me suis un peu gratté la tête pour retrouver comment les obtenir, autant prendre la peine d'écrire ces preuves explicitement) :

• Récurrence avec paramètre : si E est un ensemble quelconque, e∈E un élément et g:ℕ×E→E une fonction, alors il existe une unique u:ℕ→E telle que u(0) = e et u(S(n)) = g(n,u(n)) pour tout n∈ℕ.

  Autrement dit, dans une définition par récurrence, on a le droit d'utiliser l'indice n du terme défini et pas juste la valeur du terme précédent.

  (Pour le démontrer à partir du principe de récurrence tel que je l'ai énoncé plus haut, il suffit d'appliquer ce dernier à l'ensemble ℕ×E avec la valeur initiale (0,e) et f(n,v) = (S(n),g(n,v)) : la première coordonnée du U:ℕ→ℕ×E ainsi obtenu est forcément l'identité d'après l'unicité dans le principe de récurrence sans paramètres, et la condition sur la seconde coordonnée est exactement la condition de la récurrence avec paramètre. ∎)

• Récurrence sur les propriétés : si P⊆ℕ est une partie de ℕ telle que 0∈P et ∀n∈ℕ.(n∈P ⇒ S(n)∈P), alors en fait P=ℕ.

  Autrement dit, si une propriété est vraie en 0 et est vraie en S(n) à chaque fois qu'elle est vraie en n, alors elle est vraie en tout n∈ℕ.

  Démonstration à partir des points précédents : Déjà, on peut déjà remplacer P⊆ℕ par sa fonction indicatrice p:ℕ→Ω, qui vérifie du coup p(0)=⊤ et ∀n∈ℕ.(p(n) ⇒ p(S(n))), et le but est de montrer que p vaut constamment ⊤.

  Si à la place de ∀n∈ℕ.(p(n) ⇒ p(S(n))) on avait fait l'hypothèse ∀n∈ℕ.(p(n) ⇔ p(S(n))), c'est-à-dire ∀n∈ℕ.(p(S(n))=p(n)) ce serait facile puisque c'est une relation de récurrence sur la fonction p qui est aussi vérifiée par la fonction constamment égale à ⊤, donc l'unicité dans le principe de récurrence, appliqué à E=Ω, e=⊤ et f=id_Ω montre que p(n)=⊤ pour tout n.

  Mais comme on a seulement fait l'hypothèse ∀n∈ℕ.(p(n) ⇒ p(S(n))), il faut s'y ramener. Voici une possibilité (il y a peut-être plus simple, je ne sais pas) : on définit q:ℕ→Ω par récurrence par q(0)=⊤ et q(S(n)) = p(n)∧q(n) (ceci utilise la récurrence avec paramètre : E=Ω, e=⊤ et g(n,v) = p(n)∧v dans la notation du point précédent), et on définit aussi r(n) = p(n)∧q(n). Alors r(n) = p(n)∧q(n) = q(S(n)) par définition, et comme p(n) implique p(S(n)) (c'est notre hypothèse), on voit que r(n) implique p(S(n))∧q(S(n)), c'est-à-dire précisément r(S(n)) ; or réciproquement, r(S(n)) signifie p(S(n))∧q(S(n)), ce qui implique notamment q(S(n)), qui est égal à r(n) ; bref, on a montré ∀n∈ℕ.(r(n) ⇔ r(S(n))). Par ce qui vient d'être dit (paragraphe précédent), on voit que r(n) est vrai pour tout n, c'est-à-dire que p(n)∧q(n) l'est, et notamment p(n) est vrai pour tout n. ∎

On peut alors démontrer la proposition fondamentale suivante :

Proposition : tout entier naturel n est soit égal à 0 soit est le successeur d'un entier naturel m (c'est-à-dire n=S(m)) ; de plus, ces deux cas sont exclusifs (c'est-à-dire que zéro n'est pas le successeur d'un entier naturel) et le m dans le deuxième cas est unique (c'est-à-dire que la fonction S est injective).

Démonstration : On va observer successivement les points suivants :

‣ ① Tout entier naturel est soit 0 soit de la forme S(m) (autrement dit, ∀n∈ℕ.(n=0 ∨ ∃m∈ℕ.(n=S(m)))).

Ce point ① se démontre par une récurrence triviale sur n : la propriété que je viens de dire est trivialement vraie en 0 et trivialement vraie en S(m) si elle l'est en m (on n'a même pas besoin d'utiliser l'hypothèse de récurrence !).

Il reste à expliquer que la disjonction est exclusive et que le m est unique.

À cet effet, notons ℕ⊎{⬥} la réunion disjointe de ℕ et d'un singleton dont l'élément sera noté ‘⬥’.

Alors il existe une (unique) fonction D : ℕ → ℕ⊎{⬥} telle que D(0)=⬥ et D(S(n))=n pour tout n∈ℕ. En effet, je viens d'en donner une définition par récurrence avec paramètres (et j'ai expliqué plus haut pourquoi une telle définition est légitime).

Considérons dans l'autre sens la fonction S′ : ℕ⊎{⬥} → ℕ définie par S′(⬥)=0 et S′(n)=S(n) si n∈ℕ : cette définition est légitime par les propriétés générales des unions disjointes (définir une fonction sur X⊎Y revient à la définir sur X et sur Y séparément).

‣ ② Les fonctions D : ℕ → ℕ⊎{⬥} et S′ : ℕ⊎{⬥} → ℕ qui viennent d'être définies sont des bijections réciproques entre ℕ et ℕ⊎{⬥}.

En effet le fait que D∘S′=id_ℕ⊎{⬥} est immédiat sur les définitions, et le fait que S′∘D=id_ℕ se vérifie séparément pour 0 et pour S(m), ce qui, d'après le point ①, suffit à conclure.

‣ ③ La fonction S est injective : ∀m₁∈ℕ.∀m₂∈ℕ.((S(m₁)=S(m₂))⇒(m₁=m₂)).

Ceci découle du point ② : si S(m₁)=S(m₂) alors D(S(m₁))=D(S(m₂)), c'est-à-dire m₁=m₂. (On, si on préfère : S est la restriction à ℕ de la fonction S′ qui est bijective donc injective, donc S elle-même est injective.)

‣ ④ L'élément 0 de ℕ n'est pas de la forme S(m) (i.e., ¬∃m∈ℕ.(0=S(m)), donc la disjonction au point ① est exclusive).

En effet, si S(m)=0 alors D(S(m))=D(0), c'est-à-dire m=⬥, contredisant le fait que la réunion ℕ⊎{⬥} a été prise disjointe.

Ceci conclut tout ce qui devait être démontré. ∎

Je répète que tout ceci n'a pas vraiment de rapport avec les maths constructives : il s'agissait ici de démontrer les axiomes de Peano (qui sont, en gros, les points ③ et ④ de la démonstration ci-dessus, ainsi que la récurrence sur les propriétés telles qu'énoncée plus haut) à partir du principe de récurrence « catégorique » que j'ai postulé. En arithmétique du premier ordre, ce sont ces axiomes de Peano qu'on va postuler, mais ici je travaille librement avec des ensembles, et c'est quand même important de savoir qu'on peut — et de façon complètement constructive — démontrer les axiomes de Peano dans le contexte où je me suis placé. Mais tout ce qui vient d'être écrit n'est quand même pas complètement hors sujet pour un billet sur les maths constructives, parce que j'ai notamment prouvé que pour tout entier naturel n on a n=0 ∨ ¬(n=0) (vu que j'ai prouvé n=0 ∨ ∃m∈ℕ.(n=S(m)) et que ¬(S(m) = 0)), ce qui est l'ingrédient essentiel pour pouvoir dire que ℕ est discret, cf. ci-dessous.

On peut ensuite dérouler les définitions et sorites habituels sur les entiers naturels. L'addition ℕ×ℕ→ℕ, (m,n)↦m+n est définie par récurrence sur n par m+0=m et m+S(n)=S(m+n) ; la multiplication ℕ×ℕ→ℕ, (m,n)↦m×n est définie par récurrence sur n par m×0=0 et m×(S(n))=(m×n)+m (et on pose 1:=S(0), ce qui ne doit pas causer de confusion avec la notation pour un singleton, avec lequel on peut d'ailleurs choisir d'identifier 1 si on travaille sur des fondements ensemblistes) ; l'exponentiation ℕ×ℕ→ℕ, (m,n)↦m↑n est définie par récurrence sur n par m↑0=1 et m↑(S(n))=(m↑n)×m ; et l'ordre large (≤) ⊆ ℕ×ℕ (qu'on peut préférer voir comme sa fonction indicatrice ℕ×ℕ→Ω) par m≤n ssi il existe k tel que n=m+k (et on définit n≥m comme synonyme de m≤n, et m<n ou n>m comme synonyme de S(m)≤n disons).

Comme je l'avais évoqué dans un bout d'une entrée précédente sur le sujet, « la plupart » des résultats arithmétiques du premier ordre (i.e., ne parlant que d'entiers naturels, pas de fonctions ou de parties des entiers naturels) valables en maths classiques restent valables en maths constructives. Par exemple :

• l'addition est associative et commutative et 0 est neutre pour elle, la multiplication est associative et commutative et 1 est neutre pour elle, la multiplication est distributive sur l'addition, l'exponentiation vérifie les règles de calcul dont on a l'habitude ;
• l'ordre est total et se comporte comme on s'y attend venant des maths classiques : si m,n∈ℕ alors m≤n ou m≥n, et en fait on a exactement une des trois affirmations m<n ou m=n ou m>n, on a m≤n si et seulement si m<n ou m=n, on a m≤n si et seulement si ¬(m<n), on a m<n si et seulement si ¬(m≤n) ;
• l'ordre est compatible avec les opérations au sens où par exemple m≤n et m′≤n′ impliquent m+m′≤n+n′ et m×m′≤n×n′ ;
• la division euclidienne, la définition des nombres premiers, l'existence et l'unicité de la décomposition en facteurs premiers, tout ça fonctionne essentiellement comme en maths classiques (je ne rentre pas dans les détails).

J'insiste notamment sur le fait que pour m,n entiers naturels, on a (m=n)∨¬(m=n) : c'est-à-dire que ℕ est discret comme défini précédemment. Il est donc légitime d'écrire m≠n pour ¬(m=n).

Il n'est donc pas abusé de dire que l'arithmétique du premier ordre voit « très peu de différences » entre les maths constructives et les maths classiques. Il y a la même ressemblance pour toute la théorie des structures finies (groupes finis, graphes finis, ce genre de choses), quand on définit fini comme en bijection avec {1,…,n} pour un certain n∈ℕ, ce que j'expliquerai après ; c'est-à-dire dès lors que la structure peut se « coder » comme entiers naturels et donc se représenter en arithmétique du premier ordre : intuitivement, l'explication est que les énoncés décidables par énumération de tous les cas ne peuvent pas se comporter différemment en maths constructives des maths classiques.

J'écris la plupart des résultats et très peu de différences entre guillemet, parce que même en arithmétique du premier ordre, il n'est pas correct que tout énoncé démontrable classiquement est démontrable constructivement. Le résultat technique précis, que j'avais déjà évoqué en passant dans un billet précédent, est que tout énoncé arithmétique Π₂ démontrable dans l'arithmétique de Peano est démontrable dans l'arithmétique de Heyting [la théorie donnée en logique intuitionniste par les axiomes de Peano du premier ordre usuels] : ici, Π₂ signifie qu'il est quantifié de la forme ∀∃, c'est-à-dire une succession de quantificateurs universels devant une succession de quantificateurs existentiels, tous portant sur des entiers naturels, devant un énoncé à quantificateurs bornés (donc, en pratique, finiment testable). Pour trouver des affirmations du premier ordre sur les entiers naturels intéressantes qui sont démontrables classiquement mais pas constructivement, il faut se gratter un peu la tête, mais c'est possible. Je pense que la plus simple est toute machine de Turing soit termine soit ne termine pas (ce qui est classiquement trivial mais pas démontrable en arithmétique de Heyting) ; bien sûr, formaliser ceci exige de définir au préalable (arithmétiquement au premier ordre) la notion de machine de Turing. J'avais plus ou moins expliqué ce fait dans ce billet passé. (On peut même donner des machines de Turing précises et explicites dont on ne peut pas montrer constructivement qu'elles terminent ou ne terminent pas, mais ceci exigerait d'être plus précis que je ne l'ai été sur les fondements que j'ai utilisés, parce qu'en gros il s'agira de la machine de Turing qui recherche une contradiction dans les fondements en question.)

Néanmoins, cette ressemblance entre maths classiques et maths constructives vaut pour l'arithmétique du premier ordre, i.e., tant qu'on ne parle (et surtout, ne quantifie sur) que des entiers naturels. Dès qu'il est question de suites (cf. plus bas) ou surtout d'ensembles d'entiers naturels, les différences entre maths classiques et constructives apparaissent clairement.

Rappel du contexte et quelques notations

Redisons rapidement ici quelques unes des choses que j'ai évoquées dans ma précédente introduction aux maths constructives.

Très sommairement, donc, les maths constructives sont des maths faites en logique intuitionniste, c'est-à-dire dans laquelle on abandonne le principe de tiers exclu selon lequel toute affirmation P est soit vraie soit fausse (P∨¬P), ou, ce qui revient au même, que si une affirmation P n'est pas fausse alors elle est vraie (¬¬P⇒P ; en revanche, P n'est pas vrai est la même chose que P est faux, c'est la définition). (Les termes de maths constructives et de logique intuitionniste ne sont pas tout à fait interchangeables, mais je vais les traiter un peu comme tels : voir la partie historique de l'entrée précédente pour plus de précisions sur l'histoire des termes.) La logique intuitionniste étant plus faible que la logique classique, tout résultat obtenu dans ce cadre restera valable dans le cadre de la logique classique : on aura moins de théorèmes (et ceux qui restent peuvent devenir plus durs à démontrer), mais du coup, on peut considérer qu'une preuve constructive est plus forte (plus rare, donc plus difficile) qu'une preuve classique. Parmi les raisons de vouloir s'imposer la discipline de chercher à faire des preuves constructives, on peut notamment mentionner :

• certains pensent (mais ce n'est pas mon cas) que les mathématiques constructives sont plus correctes, parce qu'elles sont plus en accord avec leur conception philosophique de l'univers mathématique (cf. ce que je racontais sur Brouwer) ; on peut aussi simplement penser que la logique intuitionniste, à défaut d'être plus correcte, est plus économique que la logique classique, et qu'on doit donc essayer de travailler avec ;
• les preuves constructives (donc les théorèmes qu'elles produisent) sont valables plus largement que les preuves classiques (notamment, un énoncé constructivement valable est valable dans n'importe quel topos muni d'un objet d'entiers naturels) ;
• les preuves constructives apportent plus d'information que les preuves classiques (notamment, dans certaines conditions, on peut extraire un algorithme d'une preuve constructive qui calcule l'objet dont le théorème affirme l'existence — d'où le terme de constructif) ;
• la question de savoir ce qui est prouvable constructivement apporte un nouveau regard sur des théorèmes connus, qui peut être intéressant du point de vue logique, ou du point de vue pédagogique, en permettant de mieux comprendre les liens logiques entre les théorèmes et les difficultés à passer de l'un à un autre ;
• le fait de s'assurer que les définitions ou les lemmes utilisées fonctionnent bien dans un contexte constructif peut être un critère pour choisir la « bonne » définition ou la « bonne » preuve entre des possibilités classiquement indifférentes (et on peut espérer que la « bonne » se généralisera mieux) : par exemple, classiquement, en topologie, on peut définir les fermés à partir des ouverts ou les ouverts à partir des fermés, mais constructivement, seule la première approche fonctionne, ce qui suggère qu'il vaut mieux définir une topologie par ses ouverts ;
• certains outils informatiques assistants de preuve, provenant de systèmes de typage, fonctionnent naturellement en logique intuitionniste : même si on peut les faire travailler en logique classique en postulant le principe du tiers exclu, on peut penser qu'une preuve valable constructivement sera plus facile à produire, à analyser ou à utiliser dans de tels outils ;
• et enfin, bien sûr, la question de savoir si un résultat est valable constructivement est une question mathématique (classique !) tout à fait légitime, qu'on peut considérer pour son intérét intellectuel intrinsèque.

Mais avant de commencer vraiment, il faut que je dise un mot sur les règles du jeu. J'ai (plus ou moins) décrit les règles de la logique dans une partie de mon entrée précédente, et mon but est de les illustrer par l'exemple, donc je ne vais pas les réexpliquer ici, mais il faut que je parle un peu du cadre dans lequel je me place (parce qu'il n'y a pas un cadre unique pour faire des maths constructives) :

Dans ce qui suit, je vais me placer dans un cadre informel utilisant des conventions fondationnelles choisies pour dérouter le moins possible le mathématicien classique. Techniquement, les choses que je vais dire (correctement formalisées) seront vraies dans n'importe quel topos muni d'un objet d'entiers naturels, ou seront des théorèmes de la théorie IZF (un analogue assez standard de ZF en logique intuitionniste), mais je n'ai pas envie de définir ni ce qu'est un topos ni ce que sont les axiomes d'IZF parce que ce serait contraire à mon objectif pédagogique. Je vais essayer de rester agnostique ou vague quant à la question de savoir si je considère que « tout est un ensemble » (comme c'est le cas si on se place dans IZF) ou si les objets ont des types (ça n'a pas vraiment de rapport avec l'intuitionnisme, disons qu'il est peut-être plus tentant en maths constructives de travailler dans des théories des types que dans des fondements ensemblistes, mais comme mon but est de faire des choses élémentaires je n'ai pas envie de faire de choix ni même d'expliquer la différence). Pour ceux qui ont besoin de détails (les autres, sautez la fin de ce paragraphe), je précise cependant certaines des choses que je prends dans mes fondations, ou qui en résulte. D'abord, l'égalité fonctionne comme on l'attend classiquement, c'est-à-dire que c'est la plus fine relation d'équivalence et elle est extensionnelle (c'est-à-dire que d'une part si x=y alors f(x)=f(y) pour n'importe quelle fonction f, prédicat ou expression faisant intervenir une variable libre ; et d'autre part si deux ensembles X,Y ont les mêmes éléments, ∀t.(t∈X⇔t∈Y), alors ils sont égaux, et si deux fonctions f,g ayant mêmes source et but prennent les mêmes valeurs ∀t.(f(t)=g(t)), alors elles sont égales). Je suppose aussi que les ensembles de parties peuvent être formés librement, et je noterai 𝒫(X) l'ensemble des parties de X (par ailleurs l'ensemble des parties d'un singleton jouera notamment un rôle crucial comme l'ensemble des « valeurs de vérité », je vais y venir). En revanche, je ne peux pas supposer l'axiome du choix (on va voir qu'il implique le tiers exclu), et je ne veux pas le faire, même pas l'axiome du choix dénombrable, parce que même classiquement il y a un intérêt à étudier ce qui se passe sans lui, mais je vais revenir sur ce sujet ; je vais quand même postuler l'« axiome du choix unique » (ou axiome du non-choix) que j'expliquerai plus loin.

☞ Je rappelle à toutes fins utiles que dire P (où P est une formule logique) signifie exactement la même chose que de dire P est vraie (cf. le début de cette entrée, qui concerne les maths classiques mais ce n'est pas pertinent ici) ; et dire P est fausse ou P n'est pas vraie signifie exactement la même chose que ¬P (la négation de P, qui est un raccourci de langage pour P⇒⊥, c'est-à-dire si P est vraie, alors les poules ont des dents). Là où la logique intuitionniste diffère de la logique classique c'est qu'elle ne permet pas de passer de P n'est pas fausse (i.e., ¬¬P) à P est vraie. (En revanche, trois négations équivalent à une seule, quatre à deux, etc. : il est faux que P n'est pas fausse est pareil que P est fausse, et il n'est pas faux que P n'est pas fausse est pareil que P n'est pas fausse.)

Ça n'a rien à voir avec la logique intuitionniste, mais je signale aussi, s'il y avait un doute, que P⇒Q⇒R doit se lire comme P⇒(Q⇒R), et qu'il est équivalent à P∧Q⇒R (lequel doit se lire, lui, comme (P∧Q)⇒R). Sauf dans le contexte où je signale informellement un tas d'implications en série : on a les implications successives P ⇒ Q ⇒ R ⇒ S doit bien sûr se comprendre comme on a P⇒Q et aussi Q⇒R et aussi R⇒S. J'espère que cela ne causera pas de confusion.

Pour attirer l'attention sur les principales surprises des maths constructives par rapport aux maths classiques, j'utiliserai le souligné comme ceci (pour dire quelque chose comme on ne peut pas affirmer que pati-pata) ou le rouge comme ceci (pour un bout de raisonnement qui n'est pas valable constructivement ; mais de toute façon je le dirai toujours explicitement).

Ensembles vides et habités, singletons, sous-terminaux, valeurs de vérité

Commençons par la notion la plus simple qui soit, celle d'ensembles vide et habités.

On dit que E (un ensemble « dans l'univers » ou bien une partie d'un autre ensemble X, j'ai dit que je ne voulais pas rentrer dans ce genre de questions) est vide lorsqu'il n'a pas d'élément, c'est-à-dire, en symboles, ¬∃x.(x∈E) (il n'existe pas de x qui appartienne à E) ou, ce qui revient logiquement au même ∀x.¬(x∈E) (quel que soit x, il est faux que x appartienne à E), ou si on préfère l'écrire comme ça, ∀x∈E.(⊥) (tout x appartenant à E conduit à une absurdité, le symbole ‘⊥’ désigne l'énoncé tautologiquement faux, et l'ensemble vide est donc l'ensemble des x qui vérifient ⊥), avec la convention habituelle que ∀x∈E.(P(x)) signifie ∀x.(x∈E⇒P(x)) (de même que ∃x∈E.P(x) signifie ∃x.(x∈E∧P(x)) ; et je rappelle par ailleurs que ¬P signifie P⇒⊥).

Tout ce que je viens de dire est exactement pareil qu'en mathématiques classiques, et on note ∅ l'ensemble vide (unique par extensionnalité, au moins en tant que partie d'un X fixé).

Mais la notion d'ensemble non-vide, i.e., d'ensemble vérifiant ¬(E=∅), elle, n'a que très peu d'intérêt constructif : un ensemble E est non-vide s'il vérifie ¬¬∃x.(x∈E) ou, ce qui revient au même ¬∀x.¬(x∈E), mais on ne peut pas faire grand-chose avec un ensemble non-vide : notamment, on ne peut pas affirmer qu'un ensemble non-vide a un élément (je vais revenir là-dessus ci-dessous).

Ce qui est beaucoup plus utile, donc, est la notion d'ensemble habité, c'est-à-dire d'ensemble vérifiant ∃x.(x∈E), ou, si on préfère l'écrire comme ça, ∃x∈E.(⊤) (le symbole ‘⊤’ désigne l'énoncé tautologiquement vrai) : un ensemble habité est un ensemble ayant un élément. Du coup, un ensemble vide est simplement un ensemble non-habité (ou inhabité, mais attention à la confusion entre français et anglais ici !).

Il s'agit là d'un exemple extrêmement simple d'un phénomène assez courant en mathématiques constructives : quand on a deux notions qui classiquement sont simplement la négation l'une de l'autre (parfois les deux ont un nom, parfois seulement l'une des deux), constructivement on va généralement attacher plus d'importance à celle qui permet de définir l'autre comme sa négation (ici, habité permet de définir vide comme non-habité, mais vide ne permet pas de définir habité, qui est plus fort que non-vide) : généralement parlant, en mathématiques constructives, les négations ont d'assez mauvaises propriétés, donc on s'attache autant que possible à définir des notions positives. (Bien sûr, la situation n'est pas toujours aussi simple que ce que je viens de décrire : parfois une même notion classique donne naissance à plusieurs notions constructives entre lesquelles il n'est pas évident de choisir, voir par exemple ici/là sur Twitter concernant la notion de « corps ».)