• Home
• Source
• Print

TD10 – Exemples de théories

Théorie de l’égalité

Rappel : La déduction naturelle avec égalité est obtenue en ajoutant les règles suivantes à la déduction naturelle

Introduction

$\dfrac{}{\vdash t = t}I_=$

Élimination

$\dfrac{Γ\vdash p[t/x] \qquad Γ\vdash t = u}{Γ\vdash p[u/x]}E_=$

où $t,u,v$ sont des termes quelconques.

1. Montrer que l’égalité est symétrique: $\vdash ∀a.∀b.(a=b) → (b=a)$.

2. Montrer que pour tous termes $t,u,v$ on a $u=v\vdash t[u/x] = t[v/x]$.

Théorie des groupes

On considère le fragment de la théorie des entiers écrit avec le langage $0,-,+$ ($-$ est un opérateur unaire) et défini par les axiomes

Associativité	$∀x,y,z.(x+y)+z = x+(y+z)$
Élément neutre	$∀x.(x+0=x) ∧ (0+x=x)$
Opposé	$∀x.(x+(-x) = 0) ∧ ((-x)+x=0)$

1. Écrire le prédicat “l’opposé de tout nombre est unique”;
2. Prouver ce prédicat.
3. Prouver que si tout nombre est son propre opposé, alors l’addition est commutative.

Arithmétique de Peano

Rappel : L’arithmétique de Peano est une théorie des nombres écrite avec le langage $0,S,+,×$ ($S$ est un opérateur unaire, interprété comme « successeur »), et définie par les axiomes

Fondation	$∀x.Sx≠0$	Injectivité	$∀x,y.(Sx=Sy)→(x=y)$	Neutre	$∀x.x+0=x$
Addition	$∀x,y.x+Sy=S(x+y)$	Nilpotence	$∀x.x×0=0$

Distributivité

$∀x,y.x×Sy=x×y+x$

Induction

$\bigl(p[0/x] ∧ ∀y.p[y/x] → p[Sy/x]\bigr) → ∀x.p$

où $p$ est un prédicat quelconque

1. Démontrer la formule $∀x.(x=0)∨(∃y.x=Sy)$.
2. Démontrer que l’addition est commutative.
3. Démontrer la formule $∀x.Sx≠x$.
4. Donner une définition pour $x$ est inférieur ou égal à $y$ basée sur l’arithmétique de Péano.
5. Prouver que la relation ainsi définie est un ordre.
6. Prouver que $0$ est le plus petit élément et que $Sx$ est le plus petit élément plus grand que $x$.
7. Prouver que cet ordre est total (i.e. que $x≤y$ ou $y≤x$ pour tout $x,y$).
8. Prouver le schéma de induction forte: $\bigl(p[0/x] ∧ ∀z.(∀y.y<z→p[y/x])→p[Sz/x]\bigr)→∀x.p$