Corrigé Mines-Ponts 2026 Informatique I MPI — Partie 4 (Q17 à Q22) : Arithmétique de Presburger, forme simple, déduction naturelle

Sujet officiel du concours Mines-Ponts, session 2026, épreuve Informatique I MPI. Corrigé rédigé par Ibrahim Alame.

Énoncé

Les termes sont les variables (ensemble infini $V$ ) et les sommes $t_{1} + t_{2}$ ; il n'y a pas de constante. Les formules : $t_{1} = t_{2}$ , $\neg φ$ , $φ_{1} \to φ_{2}$ , $φ_{1} \land φ_{2}$ , $φ_{1} \lor φ_{2}$ , $\exists x . φ$ , $\forall x . φ$ ( $x$ ne suivant pas déjà un quantificateur dans $φ$ ) ; les variables prennent leurs valeurs dans $N$ . $[[φ]]_{a}$ est la valeur de vérité de $φ$ pour l'assignation $a$ de ses variables libres ; deux formules de mêmes variables libres sont équivalentes si elles ont même valeur pour toute assignation. Exemple : $\exists z . y = x + z$ exprime $x ⩽ y$ .

Une formule est sous forme simple si (i) elle ne contient ni $\lor$ ni $\to$ ; (ii) ni $\forall$ ; (iii) dans toute sous-formule $t_{1} = t_{2}$ , $t_{1}$ est une variable et $t_{2}$ une variable ou une somme $x + y$ de deux variables.

Les preuves utilisent les règles de l'annexe du sujet (ax, aff, $⊥$ , t.e., RAA, introductions et éliminations de $\to, \land, \lor, \neg$ , cut), celles des quantificateurs, et deux règles d'égalité ( $x$ variable, $t$ terme, $φ [t / x]$ remplacement des occurrences libres de $x$ par $t$ , addition tenue pour associative) :

$\frac{Γ , A , B ⊢ C}{Γ , A \land B ⊢ C} cut \frac{Γ ⊢ A x \in / F V ( Γ )}{Γ ⊢ \forall x . A} \forall_{i} \frac{Γ ⊢ \forall x . A}{Γ ⊢ A [ t / x ]} \forall_{e} \frac{Γ ⊢ A [ t / x ]}{Γ ⊢ \exists x . A} \exists_{i}$

$\frac{Γ ⊢ \exists x . A Γ , A ⊢ B x \in / F V ( Γ ) \cup F V ( B )}{Γ ⊢ B} \exists_{e}$

$\frac{Γ , A ⊢ B x \in / F V ( Γ ) \cup F V ( B )}{Γ , \exists x . A ⊢ B} \exists_{e}^{'} Γ ⊢ t = t ax_{=} \frac{Γ , x = t ⊢ φ [ t / x ]}{Γ , x = t ⊢ φ} sub_{=}$

Q17. Donner une formule $d i v_{2} (x)$ vraie si et seulement si $x$ est pair.
Q18. Pour tout $n \in N$ , donner une formule $f_{n} (x)$ vraie si et seulement si $x = n$ ( $n$ n'est pas un terme).
Q19. Montrer que toute formule est équivalente à une formule sous forme simple.
Q20. Prouver $⊢ (φ (x) \lor ψ (y)) \to (\neg φ (x) \to ψ (y))$ .
Q21. Donner une formule sans variable libre exprimant la transitivité de l'égalité et la prouver.
Q22. Prouver $⊢ \forall x .\forall y .\forall z . (\exists a .\exists b . x = y + a \land y = z + b) \to (\exists c . x = z + c)$ .

Corrigé

Q17. $d i v_{2} (x) := \exists y . x = y + y$ .

Pour une assignation donnant à $x$ la valeur $n$ , elle est vraie si et seulement s'il existe $y \in N$ avec $n = 2 y$ , c'est-à-dire si $n$ est pair. Ce que le correcteur attend : écrire $\exists y . x = 2 y$ est interdit, $2 y$ n'est pas un terme ; $y + y$ en est un.

Q18. Sans constante, on caractérise $0$ puis $1$ par des propriétés, puis $n$ comme somme de $n$ copies de $1$ . Soit $Z (x) := (x = x + x)$ .

$f_{0} (x) := Z (x)$ , c'est-à-dire $x = x + x$ : dans $N$ , $x = 2 x ⟺ x = 0$ .
$f_{1} (x) := \neg Z (x) \land \neg\exists y .\exists z . (\neg Z (y) \land \neg Z (z) \land x = y + z)$ : « $x$ est non nul et n'est pas la somme de deux entiers non nuls ». Si $x = 1$ : $1 \neq = 0$ , et $y + z ⩾ 2$ dès que $y, z ⩾ 1$ , donc $f_{1} (1)$ est vraie. Si $x = 0$ , $\neg Z (x)$ est faux. Si $x ⩾ 2$ , $x = 1 + (x - 1)$ avec $1 \neq = 0$ et $x - 1 \neq = 0$ : $f_{1} (x)$ est fausse.
Pour $n ⩾ 2$ : $f_{n} (x) := \exists u . (f_{1} (u) \land x = n termes u + u + \dots + u)$ , où $f_{1} (u)$ est $f_{1}$ écrite avec la variable $u$ ; les variables $x, u, y, z$ sont distinctes. Elle est vraie si et seulement s'il existe $u$ valant $1$ tel que $x = n u$ , c'est-à-dire si $x = n$ .

La somme de $n$ copies de $u$ est un terme (associativité), et chaque quantificateur porte sur une variable nouvelle : les $f_{n}$ sont bien des formules. (Contrôle exécuté par évaluation directe, quantificateurs bornés à $64$ : $f_{n} (x)$ vraie exactement pour $x = n$ , pour $n ⩽ 5$ et $x < 40$ .)

Ce que le correcteur attend : aucune constante $0$ ou $1$ dans les termes ; une définition de $f_{n}$ qui dépend de l'entier $n$ du méta-langage, jamais d'un terme (pas de $f_{n - x}$ avec $x$ variable), et pas de $f_{n}$ défini par $f_{n}$ appliquée à un autre terme.

Q19. On définit, par induction sur la structure, une traduction $S (φ)$ et l'on prouve par induction structurelle sur les formules la propriété

$P (φ)$ : $S (φ)$ est sous forme simple, a les mêmes variables libres que $φ$ , et $[[S (φ)]]_{a} = [[φ]]_{a}$ pour toute assignation $a$ .

Toutes les variables liées introduites ci-dessous sont nouvelles : distinctes entre elles et de toutes les variables déjà présentes, ce qui est possible car $V$ est infini ; la condition sur les quantificateurs est ainsi respectée.

Étape 1 : les termes (cas de base, le plus délicat). Pour tout terme $t$ et toute variable $z$ n'apparaissant pas dans $t$ , on définit une formule simple $E_{t} (z)$ de variables libres ${z} \cup var (t)$ telle que $[[E_{t} (z)]]_{a}$ soit vraie si et seulement si $a (z) = [[t]]_{a}$ :

si $t$ est une variable $w$ : $E_{t} (z) := (z = w)$ ;
si $t = t_{1} + t_{2}$ : $E_{t} (z) := \exists z_{1} .\exists z_{2} . (E_{t_{1}} (z_{1}) \land E_{t_{2}} (z_{2}) \land z = z_{1} + z_{2})$ , avec $z_{1}, z_{2}$ nouvelles.

100 % gratuit

La suite du corrigé est sur Adloun

Le corrigé rédigé en entier, question par question, et le tuteur pour poser des questions sur ce sujet.

Voir le corrigé complet, gratuitement

Inscription gratuite en 30 secondes (e-mail, nom d'utilisateur, mot de passe, classe ou profil), sans carte bancaire : arrivée directe sur le corrigé.

Toutes les parties de l'épreuve

Corrigé complet gratuit →