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.
v
est unique et déterminé- dans 4.
f'
est unique et déterminé- dans 5. 6. 7. et 8.
f_1
etf_2
sont 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 V
et de plus on remarque quep
est unique\exists G \in \mathcal{F}_{V},\quad \neg G
et de plusG
est uniqueH
^thm