Logique formelle

Mathematics, Logic · course

Voir tous les documents en mathématiques

Logique formelle

Partie I - Le calcul des pr dicats

(cid:190) Mod lisation

(cid:137) CP0. Le calcul des Pr dicats dordre 0 (Propositions)

(cid:137) CP1. Le calcul des Pr dicats dordre 1 (Pr dicats)

Partie II - Les m thodes de calcul

(cid:190) D duction

ENSI

Logique formelle

1

Logique formelle

Chapitre 1

Le calcul des Propositions

Calcul propositionnel

Logique dordre 0

CP0

ENSI

Logique formelle

2

Calcul des propositions

I Syntaxe

1. D finition du langage

2. Arbre de d composition dune formule

3. Substitution dans une formule

II S mantique

ENSI

Logique formelle

3

Calcul des propositions Syntaxe

1- D finition du langage

Un langage logique est d fini par une syntaxe, qui est d finie

par un ensemble de symboles (alphabet) et un ensemble de

r gles permettant de combiner ces symboles sous forme de

(bien

mots

form es). Cest laspect structurel et grammatical du langage.

(s quence de symboles) appel es

formules

On associe au langage une s mantique qui permet de lui

donner un sens

(linterpr ter). C'est- -dire attacher aux

formules ainsi qu'aux symboles une signification (paragraphe II).

Pour d finir un langage, on doit commencer par d finir son

alphabet.

ENSI

Logique formelle

4

Calcul des propositions Syntaxe

(cid:131) Des variables propositionnelles (atomes)

R 0 = { p, q, & } vent. indic es { p1, q1, p2, q2, & }

(cid:131) Des symboles logiques (connecteurs)

n gation ( non )

disjonction ( ou ) binaire

(

conjonction ( et )

'

implication ( implique )

quivalence ( si et seulement si )

unaire

(cid:131) Des constantes

V (vrai) F (faux)

(cid:131) Des symboles auxiliaires

(

)

,

ENSI

Logique formelle

5

Calcul des propositions Syntaxe

Une formule propositionnelle est un mot construit sur lalphabet

A0 = R 0 U {( , ' , , , } U { F,V } U { ( , ) , , }

Comment ? Selon quelles r gles ?

ENSI

Logique formelle

6

Calcul des propositions Syntaxe

D finition Formules propositionnelles

Lensemble des formules propositionnelles (not L0 ) est le plus

petit ensemble de mots construits sur lalphabet A0 et qui v rifie

les propri t s suivantes :

(cid:131) il contient R 0 U { V, F }

(cid:131) chaque fois quil contient le mot A,

il contient le mot ( A )

(cid:131) chaque fois quil contient les mots A et B, il contient les

mots : ( A ( B ) , ( A ' B ) , ( A B ) , ( A B )

ENSI

Logique formelle

7

Calcul des propositions Syntaxe

Autrement dit

Lensemble L0 des propositions b tis sur lalphabet A0 est le

plus petit ensemble qui contient R 0 U { V, F } et qui est clos

(stable) pour les op rations suivantes :

A L0 (cid:198) ( A ) L0

A , B L0 (cid:198) ( A ( B ) L0

( A ' B ) L0

( A B ) L0

( A B ) L0

ENSI

Logique formelle

8

Calcul des propositions Syntaxe

Autrement dit

Soit L0 lensemble des formules propositionnelles, alors :

1. un atome est une formule (R 0 L0 )

2. V et F sont des formules ( { V,F } L0 )

3. si A et B sont des formules alors

( A ( B ) , ( A ' B ) , ( A B ) , ( A B )

sont des formules

4. si A est une formule alors ( A ) est une formule

5.

rien dautre nest une formule

(toutes les formules propositionnelles sont g n r es par

application des quatre r gles pr c dentes uniquement)

ENSI

Logique formelle

9

Calcul des propositions Syntaxe

Remarque Lensemble L0 des formules propositionnelles est

appel le langage dordre 0 ou le langage du (calcul) des

propositions (ou des pr dicats dordre 0)

Exemples

(cid:131) Les mots suivants sont des formules

(p (( ( q ' r )) ( p )) ( p q )

(F V) ( ( p ( q ) ( q )

( p ) (( p ) ( ( q ))

F q

(cid:131) Les mots suivants ne sont pas des formules

( p q () (( p ) ( q ))

ENSI

Logique formelle

10

Calcul des propositions Syntaxe

Remarque

On peut enlever le parenth sage en labsence de toute

ambigu t

(cid:190) Il faut fixer une priorit (poids) pour les op rateurs

Ordre de priorit :

+

priorit la plus faible

(par convention)

'

(

-

+

-

(par coutume)

ENSI

Logique formelle

11

Calcul des propositions Syntaxe

(cid:131) La formule p ' q r ' s p u ( v

sera parenth s e :

( ( ( ( p ' q ) ( r ' s ) ) ( p ) ) ( u ( v ) )

2

5 3

6

1

7

4

(cid:131) La formule p (q r) ( s ( t ' p (p ( r) t

sera parenth s e :

( ( ( p ( ( (q r ) ( s ) ( ( t ' p ) ) ) ( (p ( r )) ) t )

ENSI

Logique formelle

12

Calcul des propositions Syntaxe

2- Arbre de d composition dune formule

A : ( ( p ' ( q p ) ) ' ( q ( r) ) ( q p )

A11

A12

A1

A2

A11: p ' ( q p ) A12 : ( q (

r )

A111

A1121

A1122 A121

A122

A112

A2 : ( q p )

A21 A22

On peut repr senter cette d composition sous forme dun arbre

ENSI

Logique formelle

13

Calcul des propositions Syntaxe

A1

'

A11

A

A2

A12

A21

q

A22:

A111

p

'

A112

A121:

(

A122:

A221

p

A1121

A11211

q

ENSI

A1122

q

r

A11221

p

Logique formelle

14

Calcul des propositions Syntaxe

(

q

q

r

p

Les op rateurs traiter

Publicité

en premier se trouvent

au bas de larbre

'

p

'

p

q

ENSI

Logique formelle

15

Calcul des propositions Syntaxe

Th or me de lecture unique

Pour toute formule A L0 , un et un seul des 3 cas suivants se

pr sente :

1. A R 0 U { V, F }

2. il existe une unique formule B L0 telle que A = ( B)

3. il existe un unique symbole de connecteur binaire

{ ( , ' , , }

et un unique couple de formules ( B, C ) L0

2

tels que A = (B # C)

ENSI

Logique formelle

16

" = " galit syntaxique

Calcul des propositions Syntaxe

Corollaire

Larbre de d composition dune formule est unique

Remarque

On dit que le langage des propositions est non ambigu

ENSI

Logique formelle

17

Calcul des propositions Syntaxe

3- Substitution dans une formule

D finition

Soient

" A et B deux formules propositionnelles

" p une variable propositionnelle de A

A [ p B ] est le mot obtenu en substituant la formule B

la variable p

La substitution sapplique toutes les occurrences de la

variable p

Autre notation : A (B / p)

ENSI

Logique formelle

18

Calcul des propositions Syntaxe

Exemple

A : p (q ( p) B : q r

" La variable p a 2 occurrences dans A

" La variable q a une seule occurrence dans A

A [ p B ] = B (q ( B)

= (q r) ( q ( (q r))

ENSI

Logique formelle

19

Calcul des propositions Syntaxe

On peut tendre la substitution un ensemble de formules

A [ p1 B1 , p2 B2 , & , pn Bn ]

est le mot obtenu en substituant respectivement les

formules B1, B2 , &, Bn toutes les occurrences des

variables p1, p2, &, pn

ENSI

Logique formelle

20

Calcul des propositions Syntaxe

Th or me

Soient

" A , B1 , B2,&, Bn des formules propositionnelles

p1, p2, &, pn des variables propositionnelles

"

alors le mot A [ p1 B1, p2 B2, & , pn Bn ]

est une formule propositionnelle

ENSI

Logique formelle

21

Calcul des propositions Syntaxe

Exemples

A : p ' q B : q ( r C : p ' r

" A [ p B, q C] = B ' C = (q ( r ) ' (p ' r )

" A = A

ENSI

Logique formelle

22

Calcul des propositions Syntaxe

Remarque

La substitution simultan e (remplacement en parall le) est

diff rente de la substitution s quentielle (remplacement en

s rie)

A [ p1 B1, p2 B2] ` (A [ p1 B1] ) [ p2 B2 ]

substitution simultan e substitution s quentielle

ENSI

Logique formelle

23

Calcul des propositions Syntaxe

Exemples

A : p ' q

B : p ( q

C : p q

" A [ p B, q C] =

( p ( q ) ' ( p q )

"

(A [ p B ] ) [ q C] =

( ( p ( q ) ' q ) [ q C]

= ( p ( ( p q ) ) ' ( p q )

" A [ q C, p B] =

( p ( q ) ' ( p q )

"

(A [ q C] ) [ p B ] =

( p ( ( p q ) ) [ p B ]

= ( p ( q ) ' ( ( p ( q ) q )

ENSI

Logique formelle

24

Calcul des propositions Syntaxe

Remarque

" Pour la substitution simultan e lordre nest pas important

A [ p B , q C] = A [ q C , p B ]

" Pour la substitution s quentielle lordre est important

(A [ p B]) ` (A [ q C] ) [ p B ]

ENSI

Logique formelle

25

Calcul des propositions

I Syntaxe

II S mantique

1. Interpr tation

2. Satisfiabilit - Validit

3. Equivalence et cons quence s mantiques

4. Syst me complet de connecteurs

5. Satisfiabilit dun ensemble de formules

6. Application

7. Formes normales

ENSI

Logique formelle

26

Calcul des propositions S mantique

S mantique : relatif au sens (du grec s mantikos : qui signifie )

Donner un sens une description textuelle (fournir un mod le de

certains aspects de ce que repr sente cette description)

" Syntaxe = d finition des formules (la forme)

" S mantique = effets de l valuation des formules (le sens)

ENSI

Logique formelle

27

Calcul des propositions S mantique

1- Interpr tation

A chaque proposition A, on va lui associer une valeur de

v rit dans lensemble { VB , FB } au moyen dune application

appel e interpr tation (not e I)

(cid:190) Notation I

Pour cela nous allons utiliser un morphisme sur lalg bre de

Boole

ENSI

Logique formelle

28

Calcul des propositions S mantique

D finition Alg bre de Boole

Lalg bre de Boole est form e par :

" un ensemble de valeurs de v rit

B = { VB , FB }

" un ensemble dop rateurs bool ens

{ (B , 'B , B , B , B }

d finis comme suit :

ENSI

Logique formelle

suite

29

Calcul des propositions S mantique

b b

VB

VB

FB

FB

VB

FB

VB

FB

B b b 'B b b (B b b B b b B b

FB

VB

VB

VB

VB

FB

VB

VB

FB

FB

FB

VB

VB

FB

FB

VB

VB

FB

FB

VB

ENSI

Logique formelle

30

Calcul des propositions S mantique

George BOOLE (1815 - 1864)

Math maticien et logicien anglais.

Autodidacte, cr ateur de la logique moderne qui porte

son nom (logique bool enne, aussi appel e alg bre

de Boole ou alg bre bool enne).

Il a aussi travaill dans d'autres domaines

math matiques, des quations diff rentielles aux

probabilit s en passant par l'analyse.

Il publia :

  • Mathematical Analysis of Logic (1847)
  • An investigation into the laws of thought, on which are founded the

mathematical theories of logic and probabilities (1854)

O il d veloppe une nouvelle forme de logique, la fois symbolique et

math matique. Le but : traduire des id es et des concepts en quations,

leur appliquer certaines lois et retraduire le r sultat en termes logiques.

ENSI

Logique formelle

31

Calcul des propositions S mantique

D finition Interpr tation

(cid:131) Une interpr tation (ou distribution de valeurs de v rit ),

not e I, est une application de R 0 dans lensemble B

ENSI

Logique formelle

suite

32

Calcul des propositions S mantique

D finition (suite)

(cid:131) Une interpr tation peut tre tendue lensemble de formules

Publicité

L0 (appel e aussi interpr tation) par le morphisme suivant :

"

"

"

"

"

"

[ V ]I = VB [ F ]I = FB

[ A ]I = B [ A ]I

[ A ( B ]I = [ A ]I (B [ B ]I

[ A ' B ]I = [ A ]I 'B [ B ]I

[ A B ]I = [ A ]I B [ B ]I

[ A B ]I = [ A ]I B [ B ]I

ENSI

Logique formelle

33

Calcul des propositions S mantique

Remarque

Lextension de lapplication I de R 0 L0 est unique vu

lunicit de larbre de d composition

ENSI

Logique formelle

34

Calcul des propositions S mantique

Exemple

Soit A : p ' (q p)

[ A ]I = [ p ' (q p) ]I = [ p ]I 'B [(q p) ]I

= [ p ]I 'B ( I B I)

Linterpr tation de A par I va d pendre de linterpr tation de p

et de q par I

Si I est d finie comme suit : [ p ]I = VB , I = FB

alors

[ A ]I = VB 'B ( FB B VB) = VB

ENSI

Logique formelle

35

Calcul des propositions S mantique

(cid:137)Le r sultat de linterpr tation dune formule - selon les

diff rentes distributions de valeurs de v rit possibles - peut

tre repr sent par une table appel e

table des valeurs de v rit ou table de v rit

(cid:137)La table aura 2n lignes diff rentes qui correspondent aux

diff rentes distributions de valeurs de v rit possibles (avec n

le nombre de variables distinctes de la formule)

ENSI

Logique formelle

36

Calcul des propositions S mantique

Table de v rit de

A : p ' (q p)

I

VB

VB

FB

FB

I

VB

FB

VB

FB

I

VB

VB

FB

VB

[ A ]I

VB

VB

FB

FB

(cid:190) D sormais nous confondons

les

constantes bool ens avec les op rateurs et les constantes

logiques

les op rateurs et

ENSI

Logique formelle

37

Calcul des propositions S mantique

Table de v rit de p , p ' q , p ( q , p q , p q

p q

p

p ' q p ( q

p q p q

V

V

F

F

V

F

V

F

F

F

V

V

V

F

F

F

V

V V

V

V

F

F

F

V F

V V

ENSI

Logique formelle

38

Calcul des propositions S mantique

Exemples

" Table de v rit de

B : ( ( (p q) ' p) p )

p q

p q (p q) ' p B

V

V

F

F

V

F

V

F

V

F

V

F

V

V

V F V

V F

V

ENSI

Logique formelle

suite

39

Calcul des propositions S mantique

" Table de v rit de

C : ( (p q) ' (p ' q) )

p q

p q p ' q

V

V

F

F

V

F

V

F

C

F

F

V

F

F

V

V F F

V F

F

ENSI

Logique formelle

40

Calcul des propositions S mantique

2- Satisfiabilit - Validit

D finition

Soient I une interpr tation et A une formule

Si [ A ]I = V, alors on dit que :

(cid:131) A est vraie dans linterpr tation I

(cid:131) A est satisfaite par I

(cid:131) I satisfait A

(cid:131) I est mod le de A

(cid:190) notation I ^ A

ENSI

Logique formelle

41

Calcul des propositions S mantique

D finitions

(cid:131) Une formule vraie dans toute interpr tation est dite valide

appel e aussi une tautologie

Pour tout interpr tation I, on a [ A ]I = V (cid:190) notation ^ A

(cid:131) Elle est dite invalide dans le cas contraire

(au moins fausse pour une interpr tation )

(cid:131) Une formule fausse pour toute interpr tation est dite

insatisfiable ou inconsistante ou contradictoire

appel e aussi une contradiction (ou une antilogie)

(cid:131) Elle est dite satisfiable ou consistante dans le cas contraire

(au moins vraie pour une interpr tation)

ENSI

Logique formelle

42

Calcul des propositions S mantique

Exemples

(cid:131) La formule ((p q) ' p ) p est une tautologie

(cid:131) La formule (p q) ' ( p ' q ) est une contradiction

(cid:131) La formule p ' (q p) est satisfiable et invalide

ENSI

Logique formelle

43

Calcul des propositions S mantique

Remarques

(cid:131) Si une formule est valide (tautologie) alors elle est

satisfiable. Linverse nest pas vrai

(cid:131) Si une formule est insatisfiable (contradiction) alors elle est

invalide. Linverse nest pas vrai

(cid:131) Une formule peut tre la fois satisfiable et invalide

(cid:131) Une formule ne peut jamais tre la fois valide et

insatisfiable (en m me temps une tautologie et une

contradiction)

ENSI

Logique formelle

44

Calcul des propositions S mantique

Remarque

Pour nimporte quelle formule propositionnelle, il est possible

de savoir si la formule est valide, invalide, satisfiable ou

insatisfiable

Il suffit de dresser la table de v rit

Donc le calcul des propositions est d cidable : il existe un

algorithme qui, pour toute formule propositionnelle, nous dit

si oui ou non la formule est une tautologie (notion

tudier ult rieurement)

Cest une propri t fondamentale du calcul des propositions

ENSI

Logique formelle

45

Calcul des propositions S mantique

Propositions

(cid:131) A est une tautologie ssi

A est une contradiction

(cid:131) A est une contradiction ssi

A est une tautologie

ENSI

Publicité

Logique formelle

46

Calcul des propositions S mantique

Preuve

(cid:131) A est une tautologie ssi pour tout I on a [ A ]I = V

comme [ A ]I = [ A ]I

alors pour tout I on a [ A ]I = [ A ]I = V = F

donc A est une contradiction

(cid:131)

A est contradiction ssi pour tout I on a [ A ]I = F

alors pour tout I on a [ A ]I = [ A ]I = F

donc pour tout I on a [ A ]I = V

donc A est une tautologie

Conclusion :

A est une tautologie ssi A est une contradiction

ENSI

Logique formelle

47

Calcul des propositions S mantique

Propri t s

(cid:131) (p ( p) est une tautologie

(cid:131) (p ( q1 ( & ( qn ( p ( qn+1 ( & ( qn+m) est une tautologie

(cid:131) (p ( A ( p ( B) est une tautologie

(cid:131) (p ' p) est une contradiction

(cid:131) (p ' q1 ' & ' qn ' p ' qn+1 ' & ' qn+m) est une

contradiction

(cid:131) (p ' B ' p ' C) est une contradiction

ENSI

Logique formelle

48

Calcul des propositions S mantique

Preuve

(cid:131) Pour tout I on a :

1er cas : [ p ]I = V

[ p ( p]I = [ p ]I ( [ p ]I = V ( F = V

2eme cas : [ p ]I = F alors

[ p ]I = V

[ p ( p]I = [ p ]I ( [ p ]I = F ( V = V

donc (p ( p) est une tautologie

(cid:131) Pour tout I on a :

1er cas : [ p ]I = V

[ p ' p]I = [ p ]I ' [ p ]I = V ' F = F

2eme cas : [ p ]I = F alors

[ p ]I = V

[ p ' p]I = [ p ]I ' [ p ]I = F ' V = F

ENSI

Logique formelle

49

donc (p ' p) est une contradiction

Calcul des propositions S mantique

Proposition

Soient

" A , B1, B2, &, Bn des formules propositionnelles

" p1, p2, &, pn des variables propositionnelles

Si A est une tautologie alors

A [ p1 B1 , p2 B2 , & , pn Bn ]

est galement une tautologie

ENSI

Logique formelle

50

Calcul des propositions S mantique

3- Equivalence et cons quence s mantiques

D finitions

(cid:131) Une

formule A est cons quence s mantique

(ou

cons quence logique) dune formule B ssi

tout mod le de B est un mod le de A

c- -d pour toute interpr tation I , si I = V alors I = V

(cid:190) notation B^ A

(cid:131) Une formule A est quivalente s mantiquement une

formule B ssi B est cons quence s mantique de A et A

est cons quence s mantique de B ( B ^ A et A ^ B )

(cid:190) notation A a B

ENSI

Logique formelle

51

Calcul des propositions S mantique

Propri t s

1. B ^ A ssi

B A est une tautologie (^ (B A) )

2. B a A ssi

B A est une tautologie (^ (B A) )

3. Si B a A et ^ B alors ^ A

Remarque

" La propri t 1 est tr s importante, elle relie le logique, le

math matique et la cons quence s mantique (^)

" De m me

la propri t 2 pour

math matique et l quivalence s mantique ( a )

le

logique,

le

ENSI

Logique formelle

52

Calcul des propositions S mantique

Preuve

1.

(seulement si) B ^ A

Soit I une interpr tation :

si [ B ]I = V , alors [ A ]I = V, donc [ B A ]I = V

si [ B ]I = F , alors [ B A ]I = V

donc ^ (B A)

(si) ^ (B A)

alors pour tout I, [ B A ]I = V, donc [ B ]I [ A ]I =V

en particulier si [ B ]I = V alors forcement [ A ]I = V

donc B ^ A

2. 3. Exo.

ENSI

Logique formelle

53

Calcul des propositions S mantique

Propri t s

1. Si A a B alors A a B

2. Si A a B et C a D alors

"

"

"

"

(A ( C) a (B ( D)

(A ' C) a (B ' D)

(A C) a (B D)

(A C) a (B D)

ENSI

Logique formelle

54

Calcul des propositions S mantique

Preuve

1. A a B alors pour tout I

[ A ]I = [ B ]I

donc pour tout I I = I

et donc [ A ]I = [ B ]I

do A a B

2. Exo.

Remarque

Si A a B alors A et B ont forc ment le m me mod le

ENSI

Logique formelle

55

Calcul des propositions S mantique

Th or me

Le calcul propositionnel est muni dune structure dalg bre de

Boole

(cid:131) Associativit

A ( (B ( C) a (A ( B ) ( C

A ' (B ' C) a (A ' B ) ' C

(cid:131) Commutativit

(A ( B) a (B ( A)

(A ' B) a (B ' A)

(cid:131) Distributivit

A ' ( B ( C) a (A ' B ) ( (A ' C )

A ( ( B ' C) a (A ( B ) ' (A ( C )

ENSI

Logique formelle

suite

56

Calcul des propositions S mantique

Th or me (suite)

(cid:131) Lois de De Morgan

(A ( B ) a A ' B

(A ' B ) a A ( B

(cid:131) Idempotence

(A ( A) a A

(A ' A) a A

(cid:131) Absorption

A ' ( A ( B) a A

A ( ( A ' B) a A

ENSI

Logique formelle

suite

57

Calcul des propositions S mantique

Th or me (suite)

(cid:131) El ments neutres

(A ' V ) a A

(A ( F) a A

(cid:131) El ments absorbants

(A ' F) a F (A ( V ) a V

(cid:131) Tiers exclu

(A ' A) a F

(A ( A) a V

ENSI

Logique formelle

suite

58

Calcul des propositions S mantique

Th or me (suite)

(cid:131) Inverse

V a F F a V

(cid:131) Involution

A a A

Preuve

Par table de v rit (exo)

ENSI

Logique formelle

59

Calcul des propositions S mantique

Augustus De MORGAN (juin 1806 mars 1871)

Math maticien et logicien anglais (n en Inde).

Fondateur avec Boole de la logique moderne et auteur

des lois de calcul des propositions.

De Morgan contribua beaucoup aux math matiques : la premi re notion

d'induction math matique, loi de De Morgan sur la convergence d'une suite

math matique... Il d veloppa un th or me sur les probabilit s

d' v nements vie utilis par les soci t s d'assurance aujourd'hui.

Notons que l'on doit De Morgan l'usage (en 1845) de la notation a/b

(slash) pour d signer le quotient de a par b qui fut tr s rapidement adopt e.

Il imposa l'usage du point d cimal (utilis par Neper) : 23/10 = 2.3 (soit 2,3

pour les francophones)

ENSI

Logique formelle

60

Calcul des propositions S mantique

4- Syst me complet de connecteurs

D finition

(cid:131) On appelle syst me (ou ensemble) complet de connecteurs

tout ensemble de connecteurs propositionnels permettant

dengendrer tous les autres connecteurs propositionnels

(cid:131) Il est dit minimal

lorsque aucun de ses sous-ensembles

strictes nest un syst me complet de connecteurs

ENSI

Logique formelle

61

Calcul des propositions S mantique

Exemples

(cid:131) { ( , ' , , } est un syst me complet de connecteurs

car (p q) a ( p q ) ' ( q p )

(cid:131) { ( , ' , } est un syst me complet de connecteurs

car (p q) a ( p ( q )

ENSI

Logique formelle

suite

Publicité

62

Calcul des propositions S mantique

(cid:131) { ' , } est un syst me complet de connecteurs

car (p ( q) a ( p ' q)

(cid:131) { ( , } est un syst me complet connecteurs

car (p ' q) a ( p ( q)

(cid:131) { } nest pas un syst me complet

car on a au moins besoin dun connecteur binaire

(cid:131) { ' , } et { ( , } sont donc des syst mes de connecteurs

complets et minimaux

ENSI

Logique formelle

63

Calcul des propositions S mantique

5- Satisfiabilit dun ensemble de formules

On peut tendre les r sultats de satisfiabilit un ensemble de

formules

Soient

" 0 et 1 deux ensembles de formules ( vent. infinie)

" I une interpr tation

(cid:131) 0 est satisfait par I (ou I est un mod le de 0 )

si I est mod le de toute formule de 0

(cid:131) 0 est satisfiable (ou coh rent ou consistant )

sil existe au moins une interpr tation I qui est mod le de 0

ENSI

Logique formelle

suite

64

Calcul des propositions S mantique

(cid:131) 0 est finiment satisfiable si

tout sous-ensemble fini de 0 est satisfiable

(cid:131) 0 est contradictoire (ou insatisfiable ou une contradiction) ssi

0 est non satisfiable

(cid:131) Une formule B est cons quence logique de 0 (0 ^ B ) ssi

tout mod le de 0 est mod le de B

(cid:131) 0 et 1 sont quivalents ( 0 a 1 ) ssi

toute formule de 0 est cons quence de 1 et

toute formule de 1 est cons quence de 0

c- -d 0 et 1 ont exactement les m mes mod les

ENSI

Logique formelle

65

Calcul des propositions S mantique

Th or me de compacit

Version 1

Pour tout ensemble 0 de propositions

0 est satisfiable ssi 0 est finiment satisfiable

(0 admet un mod le ssi toute partie finie de 0 admet un mod le)

Version 2

Pour tout ensemble 0 de propositions

0 est contradictoire ssi

0 admet au moins un sous-ensemble fini contradictoire

ENSI

Logique formelle

suite

66

Calcul des propositions S mantique

Th or me de compacit (suite)

Version 3

Pour tout ensemble 0 de propositions et pour toute formule B

B est cons quence de 0

ssi

B est cons quence dau moins une partie finie de 0

ENSI

Logique formelle

67

Calcul des propositions S mantique

Propositions

Soient

" 0 = { A1,&, An} et 1 deux ensembles de propositions

" A et B deux formules propositionnelles

1. 0 ^ A ssi 0 U { A } est contradictoire

2. Si 0 est satisfiable et si 1 0, alors 1 est satisfiable

3. Si 0 est satisfiable alors 0 est finiment satisfiable

4. Si 0 est contradictoire et si 0 1

alors 1 est contradictoire

5. Si 0 ^ A et si 0 1 , alors 1 ^ A

ENSI

Logique formelle

suite

68

Calcul des propositions S mantique

Propositions (suite)

6. 0 U {A} ^ B ssi

0 ^ (A B)

7. 0 ^ ( A ' B ) ssi

0 ^ A et 0 ^ B

8.

{ A1, &, An } ^ B ssi ^ (( A1 ' &. ' An ) B)

9. A est une tautologie ssi

A est cons quence logique de lensemble vide

10. A est une tautologie ssi

A est cons quence de nimporte quel ensemble de formules

11. 0 est contradictoire ssi

0 ^ ( A ' A )

ENSI

Logique formelle

suite

69

Calcul des propositions S mantique

Propositions (suite)

12. 0 est contradictoire ssi

il existe une contradiction qui soit cons quence de 0

13. { A1, &, An } est contradictoire ssi

( A1 ( &. ( An ) est une tautologie

14. 0 et 1 sont quivalents ssi

ils sont satisfaits par les m mes interpr tations

15. Lensemble vide est satisfiable

16. Lensemble de toutes les formules propositionnelles

est contradictoire

17. Tout ensemble fini de formules est s mantiquement

quivalent un ensemble constitu par seule formule

ENSI

Logique formelle

70

Calcul des propositions S mantique

Preuve

TD 1

Remarque

Un ensemble de

conjonction de formules

formules peut tre vu comme une

0 = { A1, &, An } est s mantiquement quivalent

la formule ( A1 ' & ' An )

Plus pr cis ment { A1, &, An } a { (A1 ' & ' An ) }

(point 17 de la proposition pr c dente)

ENSI

Logique formelle

71

Calcul des propositions S mantique

6- Application

Soit l nonc suivant :

Si je travaille bien alors je vais r ussir. Si je suis malade , je

ne peux pas bien travailler. Or je suis malade mais je

travaille bien. Donc je vais r ussir

1. D finition des variables propositionnelles

t : bien travailler

m : tre malade

r : r ussir

ENSI

Logique formelle

suite

72

Calcul des propositions S mantique

2. Mod lisation de l nonc :

H1 : Si je travaille bien alors je vais r ussir (cid:198) t r

H2 : Si je suis malade , je ne peux pas bien travailler

(cid:198) m t

H3 : je suis malade mais je travaille bien (cid:198) m ' t

C : je vais r ussir (cid:198) r

3. V rifier que {H1, H2, H3} ^ C, c- -d :

{ t r , m t , m ' t } ^ r

ssi

(t r) ' (m t) ' (m ' t) ^ r

ssi

^ (((t r) ' (m t) ' (m ' t)) r)

ENSI

Logique formelle

suite

73

Calcul des propositions S mantique

Remarque

On peut voir l nonc comme suit

{H1, H2} ^ (H3 C)

c- -d H3 fait partie de conclusion

Ceci ne change rien au r sultat final car nous avons

{H1, H2, H3} ^ C ssi

{H1, H2} ^ (H3 C)

(point 6 de la proposition pr c dente)

ENSI

Logique formelle

suite

74

Calcul des propositions S mantique

Remarque

L nonc est correct : par table de v rit , nous avons bien

{H1, H2, H3} ^ C

Au fait nous avons {H1, H2, H3} est contradictoire. Donc

nimporte quelle conclusion donne toujours un nonc correct.

Par exemple si nous prenons C : je ne vais pas r ussir

Nous avons toujours {H1, H2, H3} ^ C

ENSI

Logique formelle

75

Calcul des propositions S mantique

Commentaires sur les connecteurs logiques

(cid:131) Conjonction

A ' B

A et B ; A mais B ; A quoique B ; A tandis que B

(cid:131) Disjonction A ( B

ou inclusif ( vel en latin)

A ou B ; A ou/et B (juridique) ; A moins que B

A sinon B ; A sauf si B ; A ou B et peut tre les deux

(cid:131) Ou exclusif

A B a (A ' B) ( ( A ' B)

A ou B mais pas les deux ; soit A, soit (exclusivement) B

( aut en latin)

ENSI

Logique formelle

suite

76

Calcul des propositions S mantique

(cid:131) Implication A B

si / lorsque A, alors / n cessairement/ cest que B

A implique / entra ne B

A est condition suffisante de / suffit B

A seulement si / que si B

B si /lorsque A

B est condition n cessaire de A

ENSI

Logique formelle

suite

77

Calcul des propositions S mantique

(cid:131) Equivalence A B

A (est) quivalent B

A si et seulement si B

A est condition n cessaire est suffisante (CNS) de B

A si B et r ciproquement

" A ssi B : A seulement si B (A B) ; A si B (A B)

" A cns B : A condition suffisante B (A B)

A condition n cessaire B (A B)

ENSI

Logique formelle

78

Calcul des propositions S mantique

7- Formes normales

D finition

(cid:131) On appelle litt ral un atome ou une n gation datome

(ex. : p , p , &)

(cid:131) Une formule est dite sous forme normale disjon...