diff --git a/règles de démonstration.md b/règles de démonstration.md
index 1c40d5cc..2f6e21cd 100644
--- a/règles de démonstration.md	
+++ b/règles de démonstration.md	
@@ -3,6 +3,7 @@ up:
 tags:
   - s/maths/logique
 aliases:
+  - règle d'axiome
 ---
 
 ```breadcrumbs
diff --git a/théorie logique.md b/théorie logique.md
index 59cc5649..18794fb3 100644
--- a/théorie logique.md	
+++ b/théorie logique.md	
@@ -13,6 +13,7 @@
 > > [!corollaire] Lemme
 > > Une théorie $T$ est cohérente s'il n'existe pas d'énoncé $f$ tel que $T \vdash f$ et $T \vdash \neg f$
 > > 
+^coherence
 
 > [!proposition]+ Finitude
 > Si $T \vdash f$
@@ -60,9 +61,27 @@
 > > [!démonstration]- Démonstration
 > > Soit $(g_1, \dots, g_{n})$ une démonstration formelle de $T \cup \{ f \} \vdash g$
 > > On obtient une démonstration formelle de $T \vdash f \to g$ en partant de la suite $(f \to g_1, \dots, f\to g_{n})$ et en insérant des formules supplémentaires :
-> > $T \vdash f \to g_1 \qquad T \cup \{ f \}$
+> > $T \vdash f \to g_1 \qquad T \cup \{ f \} \vdash g_{1}$
 > > $\vdots$
-> > $T \vdash f \to g_{n-1}$
+> > $T \vdash f \to g_{n-1} \qquad T \cup \{ f \} \vdash g_{m}$
+> > Si $T \cup \{ f \} \vdash g_{m}$ est une [[règles de démonstration|règle d'axiome]]
+> >  - $1^{\text{er}}$ cas $g_{m} \in T$ :
+> >    $T \vdash g_{m}$ (axiome)
+> >    $T \vdash g_{m} \to (f \to g_{m})$ (tautologie : $p \to (q \to p)$)
+> >    $T \vdash f \to g_{m}$ par [[modus ponens]]
+> >  - $2^{\text{ème}}$ cas $g_{m} = f$
+> >    alors $T \vdash (f \to f)$ est une tautologie
+> >  - Si $T \cup \{ f \} \vdash g_{m}$ est un [[modus ponens]]
+> >    $T \cup \{ f \} \vdash g_{m}$  ...???
+> 
+> > [!corollaire] (raisonnement par l'absurde)
+> > Pour prouver $T \vdash f$ (il faut et ) il suffit de prouver que $T \cup \{ \neg f \}$ n'est pas [[théorie logique#^coherence|cohérente]].
+> > > [!démonstration]- Démonstration
+> > > - supposons que $T \cup \{ \neg f \}$ n'est pas cohérente
+> > >   par le théorème de déduction on a que $T \vdash \neg f \to \bot$
+> > >   alors $T \vdash (\neg f \to \bot) \to f$ ([[tautologie]])
+> > >   et donc $T \vdash f$ par [[modus ponens]]
+> > >