Skip to content

Exercice 1 : Quantificateurs et démonstrations formelles

🌐 Énoncé du problème / Étude de cas

Section titled “🌐 Énoncé du problème / Étude de cas”

Dans le cadre de la modélisation formelle de systèmes dynamiques discrets en informatique (par exemple, la vérification de programmes ou l’analyse de stabilité de réseaux de capteurs IoT), les ingénieurs manipulent quotidiennement des assertions logiques complexes combinant des quantificateurs universels (∀\forall) et existentiels (∃\exists).

Une mauvaise manipulation de ces quantificateurs conduit souvent à des failles de sécurité ou à des instabilités de réseaux. L’objectif de ce problème est d’étudier la manipulation rigoureuse des assertions quantifiées, d’analyser la négation de propriétés complexes et d’appliquer ces concepts à un modèle simplifié de régulation de flux de données sous contrainte énergétique.

Soit EE un ensemble non vide (qui représentera l’espace des états d’un système) et f:E→Ef : E \to E une application. On considère des propriétés portant sur ff et sur des parties de EE.


  1. Manipulation élémentaire de quantificateurs Soit P(x,y)P(x, y) une assertion à deux variables, où x∈Xx \in X et y∈Yy \in Y. Écrire formellement la négation de l’assertion : A:∀x∈X,(P(x,y0)  ⟹  ∃y∈Y,¬P(x,y))\mathcal{A} : \forall x \in X, \left( P(x, y_0) \implies \exists y \in Y, \neg P(x, y) \right) où y0fixeˊey_0 fixée est un élément de YY.

  2. Propriétés de bornitude et modélisation de capteurs On se place dans le cas où E=RE = \mathbb{R}. Soit f:R→Rf : \mathbb{R} \to \mathbb{R}. Traduire mathématiquement à l’aide de quantificateurs la phrase : “La fonction ff n’est pas majorée sur R\mathbb{R}”.

  3. Analyse critique d’un modèle d’énergie Un capteur IoT transmet des paquets de données. Soit E(t)E(t) l’énergie du système à l’instant tt (exprimée en joules J\text{J}). On modélise l’évolution par une fonction de transition ff telle que En+1=f(En)E_{n+1} = f(E_n). Un ingénieur affirme que le système est stable en énergie si : ∃M∈R,∀n∈N,En≤M\exists M \in \mathbb{R}, \forall n \in \mathbb{N}, E_n \le M

    • a) Écrire la négation de cette proposition de stabilité.
    • b) Esprit critique : En pratique, un composant matériel réel possède une énergie maximale absolue Emax=5 JE_{\text{max}} = 5 \, \text{J} dictée par la physique de sa batterie au lithium. Que penser de l’hypothèse mathématique d’existence d’un MM quelconque non borné par la physique du système ? Discutez des limites du modèle mathématique face à la réalité industrielle.
  4. Alternance des quantificateurs Soit g:R→Rg : \mathbb{R} \to \mathbb{R}. On considère les deux assertions suivantes :

    • (S1):∀x∈R,∃y∈R,g(x)<y(\text{S}_1) : \forall x \in \mathbb{R}, \exists y \in \mathbb{R}, g(x) < y
    • (S2):∃y∈R,∀x∈R,g(x)<y(\text{S}_2) : \exists y \in \mathbb{R}, \forall x \in \mathbb{R}, g(x) < y
    • a) Montrer que (S1)(\text{S}_1) est toujours vraie quelle que soit la fonction gg.
    • b) Que dire de (S2)(\text{S}_2) ? Caractériser l’ensemble des fonctions gg vérifiant (S2)(\text{S}_2).

  • Q1 : Rappelez-vous que ¬(A  ⟹  B)  ⟺  (A∧¬B)\neg(A \implies B) \iff (A \land \neg B) et que la négation inverse les quantificateurs (¬(∀)≡∃¬\neg(\forall) \equiv \exists \neg).
  • Q2 : Pour “non majorée”, l’énoncé usuel de “majorée” est ∃M∈R,∀x∈R,f(x)≤M\exists M \in \mathbb{R}, \forall x \in \mathbb{R}, f(x) \le M. Niez cette assertion en inversant soigneusement les quantificateurs.
  • Q3 : Traduisez la borne physique dans le formalisme logique et questionnez la validité du domaine de définition R\mathbb{R} pour MM ou pour EnE_n.
  • Q4 : Pour (S1)(\text{S}_1), pour un xx donné, pensez à choisir y=g(x)+1y = g(x) + 1. Pour (S2)(\text{S}_2), reliez cela à la notion de fonction majorée.

📋 Corrigé détaillé et analyse des résultats

Section titled “📋 Corrigé détaillé et analyse des résultats”
  1. Négation de l’assertion A\mathcal{A} : L’assertion est : A:∀x∈X,(P(x,y0)  ⟹  ∃y∈Y,¬P(x,y))\mathcal{A} : \forall x \in X, \left( P(x, y_0) \implies \exists y \in Y, \neg P(x, y) \right) Rappelons que ¬(A  ⟹  B)≡A∧¬B\neg(A \implies B) \equiv A \land \neg B. La négation de l’implication P(x,y0)  ⟹  (∃y∈Y,¬P(x,y))P(x, y_0) \implies \left(\exists y \in Y, \neg P(x, y)\right) est donc : P(x,y0)∧¬(∃y∈Y,¬P(x,y))P(x, y_0) \land \neg\left(\exists y \in Y, \neg P(x, y)\right) En poussant la négation devant le quantificateur existentiel : P(x,y0)∧(∀y∈Y,P(x,y))P(x, y_0) \land \left(\forall y \in Y, P(x, y)\right) Finalement, en niant le quantificateur universel initial ∀x∈X\forall x \in X en un ∃x∈X\exists x \in X, on obtient : ¬A:∃x∈X,(P(x,y0)∧∀y∈Y,P(x,y))\neg \mathcal{A} : \exists x \in X, \left( P(x, y_0) \land \forall y \in Y, P(x, y) \right)

  2. Traduction de la non-majoration : Être majorée s’écrit : ∃M∈R,∀x∈R,f(x)≤M\exists M \in \mathbb{R}, \forall x \in \mathbb{R}, f(x) \le M. La négation (donc “n’est pas majorée”) s’obtient en niant cette proposition : ∀M∈R,∃x∈R,f(x)>M\forall M \in \mathbb{R}, \exists x \in \mathbb{R}, f(x) > M Interprétation physique : Quel que soit le seuil d’alerte MM fixé, il existe toujours un état du système (ou un instant) où l’énergie dépasse ce seuil.

  3. Analyse du modèle d’énergie et esprit critique :

    • a) L’assertion de stabilité est ∃M∈R,∀n∈N,En≤M\exists M \in \mathbb{R}, \forall n \in \mathbb{N}, E_n \le M. Sa négation est : ∀M∈R,∃n∈N,En>M\forall M \in \mathbb{R}, \exists n \in \mathbb{N}, E_n > M
    • b) Analyse critique des limites du modèle : Mathématiquement, la variable MM peut appartenir à R\mathbb{R} tout entier, sans borne supérieure. Cependant, dans un contexte d’ingénierie embarquée, l’énergie est stockée dans un composant physique (batterie, condensateur) soumis à des lois de rupture. Si En>EmaxE_n > E_{\text{max}} (où Emax=5 JE_{\text{max}} = 5 \, \text{J}), le modèle mathématique continuera d’évoluer (si ff le permet), mais le système physique réel subira une détérioration irréversible (surchauffe, explosion de la batterie, coupure par un disjoncteur thermique). Conclusion du modèle : Le mathématicien étudie la borne dans R\mathbb{R}, mais l’ingénieur doit impérativement restreindre le domaine à M≤EmaxM \le E_{\text{max}}, sous peine d’obtenir un modèle abstrait parfaitement correct sur le plan formel mais totalement caduc en exploitation industrielle.
  4. Alternance des quantificateurs :

    • a) (S1):∀x∈R,∃y∈R,g(x)<y(\text{S}_1) : \forall x \in \mathbb{R}, \exists y \in \mathbb{R}, g(x) < y. Soit x∈Rx \in \mathbb{R} fixé. Choisissons y=g(x)+1y = g(x) + 1. On a bien g(x)<g(x)+1g(x) < g(x) + 1, soit g(x)<yg(x) < y. L’assertion (S1)(\text{S}_1) est donc toujours vraie pour n’importe quelle fonction gg.
    • b) (S2):∃y∈R,∀x∈R,g(x)<y(\text{S}_2) : \exists y \in \mathbb{R}, \forall x \in \mathbb{R}, g(x) < y. Cette assertion signifie qu’il existe un réel yy qui est strictement supérieur à toutes les valeurs prises par gg. C’est exactement la définition d’une fonction strictement majorée. L’ensemble des fonctions vérifiant (S2)(\text{S}_2) est donc l’ensemble des fonctions majorées sur R\mathbb{R}. Par exemple, g(x)=−x2g(x) = -x^2 la vérifie (avec y=1y = 1), mais g(x)=xg(x) = x ne la vérifie pas.