diff --git a/formule logique.md b/formule logique.md
index 76098f1f..1fe921dd 100644
--- a/formule logique.md	
+++ b/formule logique.md	
@@ -3,5 +3,40 @@ up:
   - "[[M1 LOGOS . logique . calculer]]"
 ---
 > [!definition] Définition
-> Soit $V$
-^definition
\ No newline at end of file
+> Soit $V$ un ensemble (de symboles de variables).
+> On demande que $V$ soit disjoint de l'ensemble $L$ des symboles logiques.
+> Les **formules** sont des [[langage formel mot|mots]] de l'alphabet $V \cup L$ c'est-à-dire  des suites finies d'éléments de $V \cup L$
+^definition
+
+> [!definition] 
+> $\mathcal{F}_{v}$ est le plus petit ensemble de mots vérifiant les propriétés suivantes
+>  - $[0] \in \mathcal{F}_{v}$
+>  - $[1] \in \mathcal{F}_{v}$
+>  - si $v \in V$ alors $[v] \in \mathcal{F}_{v}$
+>  - si $f \in F_{v}$ alors $\neg f \in \mathcal{F}_{v}$
+>  - si $f_1, f_2 \in F_{v}$ alors :
+>      - $(f_1 \vee f_2) \in \mathcal{F}_{v}$ ou, autrement : $[\vee f_1 f_2] \in \mathcal{F}_{v}$
+>      - $(f_1 \wedge f_2) \in \mathcal{F}_{v}$ ou, autrement : $[\wedge f_1 f_2] \in \mathcal{F}_{v}$
+>      - $(f_1 \implies f_2) \in \mathcal{F}_{v}$ ou, autrement : $[\implies f_1 f_2] \in \mathcal{F}_{v}$
+>      - $(f_1 \iff f_2) \in \mathcal{F}_v$ ou, autrement : $[\iff f_1 f_2] \in \mathcal{F}_{v}$
+
+# Propriétés
+
+> [!proposition]+ Théorème
+> Pour toute formule $f \in \mathcal{F}_{v}$
+> une et une seule des assertions suivantes est verrifée :
+>  1. $f = [0]$
+>  2. $f = [1]$
+>  3. $\exists v \in V,\quad f = [v]$
+>  4. $\exists f' \in \mathcal{F}_{v},\quad f = \neg f'$
+>  5. $\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\vee f_1 f_2]$
+>  6. $\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\wedge f_1 f_2]$
+>  7. $\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\implies f_1 f_2]$
+>  8. $\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\iff f_1 f_2]$
+> De plus :
+>  - dans 3. $v$ est unique et déterminé 
+>  - dans 4. $f'$ est unique et déterminé
+>  - dans 5. 6. 7. et 8. $f_1$ et $f_2$ sont uniques et déterminés
+
+
+