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

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

Énoncé

Les termes sont construits à partir des variables (ensemble infini $V$ ) par $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 . φ$ et $\forall x . φ$ (pour $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 la même valeur pour toute assignation. Exemple : $φ_{⩽} (x, y) := \exists z . y = x + z$ exprime $x ⩽ y$ .

Une formule est sous forme simple si (i) elle ne contient ni $\lor$ ni $\to$ ; (ii) elle ne contient pas $\forall$ ; (iii) toute sous-formule $t_{1} = t_{2}$ a pour $t_{1}$ une variable et pour $t_{2}$ une variable ou une somme $x + y$ de deux variables. Les preuves utilisent les règles de déduction naturelle de l'annexe du sujet (ax, aff, $⊥$ , t.e., RAA, $\to_{i}$ , $\to_{e}$ , $\land_{i}$ , $\land_{e}^{g}$ , $\land_{e}^{d}$ , $\lor_{i}^{g}$ , $\lor_{i}^{d}$ , $\lor_{e}$ , $\neg_{i}$ , $\neg_{e}$ , cut) et deux règles d'égalité, pour $x$ une variable et $t$ un terme :

$Γ ⊢ t = t ax_{=} \frac{Γ , x = t ⊢ φ [ t / x ]}{Γ , x = t ⊢ φ} sub_{=} \frac{Γ , A , B ⊢ C}{Γ , A \land B ⊢ C} cut$

( $φ [t / x]$ : remplacement des occurrences libres de $x$ par $t$ ; l'addition est tenue pour associative).

Q18. Donner une formule $d i v_{2} (x)$ vraie si et seulement si $x$ est pair.
Q19. Pour tout $n \in N$ , donner une formule $f_{n} (x)$ vraie si et seulement si $x = n$ ( $n$ n'est pas un terme).
Q20. Montrer que toute formule est équivalente à une formule sous forme simple.
Q21. Prouver en déduction naturelle $⊢ (φ (x) \lor ψ (y)) \to (\neg φ (x) \to ψ (y))$ .
Q22. Donner une formule $φ (x, y, z)$ à trois variables libres exprimant la transitivité de l'égalité et la prouver en déduction naturelle.

Corrigé

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

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

Q19. 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.

Q20. On définit, par induction sur la structure, une traduction $S (φ)$ et l'on prouve par induction structurelle 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.

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 →