cours/formule logique.md

up

up
M1 LOGOS . logique . calculer

[!definition] Définition 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 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