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 :
  • [\vee f_1 f_2] \in \mathcal{F}_{v} sous entendu (f_1 \vee f_2)
  • [\wedge f_1 f_2] \in \mathcal{F}_{v} sous entendu (f_1 \wedge f_2)
  • [\implies f_1 f_2] \in \mathcal{F}_{v} sous entendu (f_1 \implies f_2)
  • [\iff f_1 f_2] \in \mathcal{F}_{v} sous entendu (f_1 \iff f_2)

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

[!proposition]+ On définit une fonction p qui à un symbole associe un poids : p(0) = p(1) = p(v) = -1 pour tout v \in V p(\neg) = 0 p(\wedge) = p(\vee) = p(\implies) = p(\iff) = 1 p(\emptyset) = 0 Puis par réccurence, avec m = [a_1, \dots ,a_{n}] avec a_{i} \in V \cup L p(m) = p(a_1) + \cdots + p(a_{n})

A a alors le théorème suivant : Un mot f est une formule si et seulement si on a :

1. p(f) = -1
2. pour tout préfixe f' de f, f' \neq f on a p(f') \geq 0

[!corollaire] Un préfixe f' d'une formule f (tel que f' \neq f) n'est pas uen formule.