1.2 KiB
1.2 KiB
up, tags, aliases
| up | tags | aliases | ||
|---|---|---|---|---|
|
|
[!proposition]+ Théorème de lecture unique Pour toute formule
f \in \mathcal{F}_{v}une et une seule des assertions suivantes est verrifée :
f = [0]f = [1]\exists v \in V,\quad f = [v]\exists f' \in \mathcal{F}_{v},\quad f = \neg f'\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\vee f_1 f_2]\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\wedge f_1 f_2]\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\implies f_1 f_2]\exists f_1, f_2 \in \mathcal{F}_{v},\quad f = [\iff f_1 f_2]De plus :
- dans 3.
vest unique et déterminé- dans 4.
f'est unique et déterminé- dans 5. 6. 7. et 8.
f_1etf_2sont uniques et déterminés[!démonstration]- Démonstration Soit
H \in \mathcal{F}_{V}une formule On distingue 3 cas principaux et disjoints (on peut préciser plus en déclinant les 8 cas distincts) :
\exists P \in \mathcal{F}_{V},\quad H = P \in Vet de plus on remarque quepest unique\exists G \in \mathcal{F}_{V},\quad \neg Get de plusGest uniqueH
^thm