[PDF] Théorème de complétude du calcul propositionnel

View - Download Théorème de complétude du calcul propositionnel

Previous PDF

Next PDF

MAGISTERE MATH.-INFO. (2003-2004) Logique

E. Bouscaren

Théorème de complétude du calcul

propositionnel

Notes complémentaires (0)

1 Quelques rappels de sémantique

Définition: Un ensemble de formulesΣestsatisfaisablesi il existe une distribution de

valeurs de vérité,δ, qui satisfait toutes les formules deΣ, c"est-à-dire telle que, pour toute

formuleB?Σ,δ(B) = 1. Un ensemble qui n"est pas satisfaisable est ditinconsistant.

On a démontré en cours:

Proposition 1.1(Theorème de compacité du calcul propositionnel)SoitΣun ensem- ble de formules,Σest satisfaisable si et seulement si tout sous-ensemble fini deΣest satisfaisable. Définition: SoientΣun ensemble de formules etAune formule. On dit queAest

conséquence sémantiquedeΣ, notéΣ?A, si toute distribution de valeurs de véritéδ

qui satisfaitΣsatisfait égalementA.

SiAest une tautologie on a∅ ?A, noté?A.

Les premières propriétés:

Lemme 1.2SoitΣun ensemble de formules etBune formule. (i)Σest inconsistant ssi il existe une formuleAtelle queΣ?AetΣ? ¬A. (ii)Σest inconsistant ssi, pour toute formuleA,Σ?AetΣ? ¬A. (iii)Σ?BssiΣ? {¬B}est inconsistant. La proposition suivante est équivalente au théorème de compacite (1.1): Proposition 1.3SoitΣun ensemble de formules etBune formule. AlorsΣ?Bsi et seulement si il existe un sous-ensemble finiFdeΣtel queF?B. Démonstration de l"équivalence: Supposons d"abord 1.1: SiΣ?B, par le lemme 1.2, Σ?{¬B}est inconsistant. Par 1.1, il existe un sous-ensemble finiFdeΣtel queF?{¬B} est inconsistant. Par 1.2 à nouveau,F?B. Réciproquement, supposons 1.3, et soitΣun ensemble de formules inconsistant. Alors par 1.2 , il existe une formuleAtelle queΣ?AetΣ? ¬A. Par 1.3, il existeF1etF2, sous-ensembles finis deΣtels queF1?AetF2? ¬A. DoncF1?F2?AetF1?F2? ¬A, et doncF1?F2est un sous-ensemble fini deΣqui est inconsistant.? 1

2 Complétude pour le calcul propositionnel

On reprend ici brièvement la démonstration du théorème de complétude donné en cours

(et qui est celle du livre "Introduction to Mathematical Logic" de E. Mendelson.) On considère le calcul propositionnel avec les connecteurs{¬,→}

2.1 Preuves formelles, premières propriétés

LES AXIOMES

On prend trois schémas d"axiomes:

(A1) : Pour toutes formules propositionnellesA,B -(A→(B→A)) (A2) : pour toutes formules propositionnellesA,B,C (A3) : pour toutes formules propositionnellesA,B -((¬B→ ¬A)→((¬B→A)→B))

Une RÈGLE de déduction:

-le Modus Ponens: pour toutes formules propositionnellesA,B, de{A,(A→B)}on déduitB. Définition: SoitΣun ensemble de formules propositionnelles etAune formule proposi- tionnelle. On dit queAestconséquence syntaxique, ou conséquence formelledeΣ, notéΣ|≂A, s"il existe unedémonstration formelle(ou preuve formelle) deAà partir deΣ, c"est-à-dire, s"il existe une suite finie{A1,...,Ak}de formules propositionnelles, telles que -Ak=A, - soitAiest une formule deΣ, - soitAiest un axiome - soitAia été déduit par Modus Ponens de deux formulesAletAm= (Al→Ai) avecm,l < i.

Remarques évidentes:

-{A} |≂A - SiAest un axiome,|≂A - SiΣ1?Σ2etΣ1|≂A, alorsΣ2|≂A.

Un exemple de démonstration formelle

Lemme 2.1Pour toute formuleA,|≂(A→A).

2

Démonstration:

(1)A1= ((A→((A→A)→A))→((A→(A→A))→(A→A))), (Axiome

2 avecB= (A→A)etC=A)

(2)A2= (A→((A→A)→A)), (Axiome 1 avecB= (A→A)) (3)A3= ((A→(A→A))→(A→A)), ( Modus Ponens appliqué àA1etA2) (4)A4= (A→(A→A)), (Axiome 1 avecB=A) (5)A5= (A→A)( Modus Ponens appliqué àA3etA4).? Les lemmes suivant sont immédiats mais importants.Σest un ensemble de formules,A etBsont des formules: Lemme 2.2SiΣ|≂AetΣ|≂(A→B), alorsΣ|≂B. Lemme 2.3SiA1,...,Akest une démonstration formelle deΣ|≂A, de longueurk, alors pour chaquei < k,A1,...,Aiest une démonstration formelle deΣ|≂Aiqui est de longueuri, donc de longueur strictement inférieure àk. Lemme 2.4(Finitude)SiΣ|≂A, alors il existe un sous-ensemble finiΣ0deΣtel que

0|≂A.

Lemme 2.5SiΣ|≂(A→B), alorsΣ? {A} |≂B.

Démonstration:Σ? {A} ?Σ, donc puisqueΣ|≂(A→B), a fortioriΣ? {A} |≂(A→

B). Par la remarque plus haut:Σ? {A} |≂A, donc (2.2)Σ? {A} |≂B.?

Un peu plus difficile, la réciproque:

Lemme 2.6(Lemme de déduction)

SiΣ? {A} |≂B, alorsΣ|≂(A→B).

Démonstration: On raisonne par récurrence sur la longueur d"une démonstration formelle, B

1,...,Bk+1=B, deΣ? {A} |≂B.

On suppose quek≥0.

Premier cas:Bk+1est un axiome ou un élément deΣ. Alors on a la suite suivante: (1)C1=B(axiome ou élément deΣ) (2)C2= (B→(A→B))(axiome A1) (3)C3= (A→B)(par Modus Ponens appliqué àC1etC2) qui est une démonstration formelle de(A→B)à partir deΣ. Deuxième cas:B=A. Alors on a vu plus haut (Lemme 2.1) que|≂(A→A). Troisième cas (possible uniquement sik≥2):Bk+1=Best obtenu par application de la règle de Modus ponens àBietBj= (Bi→B), aveci,j < k+ 1. Par le lemme 2.3, il y a des preuves deΣ?{A} |≂Biet deΣ?{A} |≂Bjde longueurs inférieures ou égales àk. Donc par hypothèse de récurrence, on a (1)Σ|≂(A→Bi) (2)Σ|≂(A→(Bi→B)).

Par l"axiome(A2), on a aussi

3

Par Modus Ponens appliqué à (2) et (3),

et par Modus Ponens appliqué à (1) et (4), (5)Σ|≂(A→B).? Avec l"aide du Lemme de déduction (2.6) et un peu de travail, on peut montrer:

Lemme 2.7Pour toutes formulesA,BetC,

(i)|≂(¬¬A→A) (ii)|≂(A→ ¬¬A) (iii)|≂(¬A→(A→B)) Les "théorèmes" donnés dans le lemme précédent sont exactement ceux dont on va avoir besoin pour démontrer le théorème de complétude (on aurait bien sûr pu les prendre au départ comme axiomes supplémentaires, mais cela n"aurait pas été très économique).

Enfin un dernier résultat fondamental:

Lemme 2.8Pour tout ensemble de formulesΣ, pour toutes formulesAetB, si Σ? {A} |≂BetΣ? {¬A} |≂B, alorsΣ|≂B. Démonstration: Par le lemme de déduction (2.6), on a (1)Σ|≂(A→B) et (2)Σ|≂(¬A→B).

Par 2.7 (v):

par Modus Ponens appliqué à (1) et (3), (4)Σ|≂((¬A→B)→B) par Modus Ponens appliqué à (2) et (4), (5)Σ|≂B.? Définition: On dit queΣestcontradictoiresi il existe une formuleAtelle queΣ|≂A etΣ|≂¬A. Lemme 2.9Σest contradictoire si et seulement si, pour toute formuleB,Σ|≂B. Démonstration: SupposonsΣcontradictoire, donc il existe une formuleAtelle queΣ|≂A

etΣ|≂¬A. Par le lemme 2.7 (iii),|≂(¬A→(A→B)). En appliquant le Modus Po-

nens deux fois, on obtient bienΣ|≂B.? 4

2.2 Rapports avec la sémantique

2.2.1 Le théorème de complétude finitaire

Proposition 2.10(Validité)SoientΣun ensemble de formules etAune formule. Si Σ|≂A, alorsΣ?A. En particulier, si|≂A, alorsAest une tautologie. Démonstration: On commence par vérifier facilement que siAest l"un des axiomes (A1), (A2) ou (A3), alorsAest une tautologie. Ensuite, on raisonne par récurrence sur la longueur d"une preuve formelle deΣ|≂A, A

1,...,An+1=A, avecn≥0.

Premier cas:An+1=Aest un axiome, alors on a vérifié queAest une tautologie donc certainementΣ?A. Deuxième cas:A?Σet le résultat est évident. Troisième cas (sin≥2):Aest obtenu par application de la règle de Modus Ponens àAi

inférieure ou égale àndeΣ|≂Aiet deΣ|≂Aj. Par hypothèse de récurrence, on a donc

Σ?AietΣ?(Ai→A).

Soitδune distribution qui satisfaitΣ, alors par ce qui précéde,δ(Ai) = 1etδ(Ai→

A) = 1. Par définition (sémantique) du connecteur→, on doit avoirδ(A) = 1.? Proposition 2.11(Théorème de complétude finitaire)

SoitAune formule, si?Aalors|≂A.

Il s"agit donc d"exhiber une preuve formelle de la tautologieA. Pour cela on commence par le lemme suivant qui est très astucieux. Lemme 2.12SoitAune formule à variables parmi{P1,...,Pn}. Soitδune distribution P iδ=Pisiδ(Pi) = 1,Piδ=¬Pisiδ(Pi) = 0.

Et on pose

A

δ=Asiδ(A) = 1,Aδ=¬Asiδ(A) = 0.

Alors{P1δ,...,Pnδ} |≂Aδ.

Démonstration: Par induction sur la complexité de la formuleA. - SiAest une variable propositionnelle,A=Pi, alorsPiδ=Aδet certainement {P1δ,...,Pnδ} |≂Piδ. - SiA=¬B. Siδ(B) = 0, alorsBδ=¬B=A=Aδet donc, par hypothèse d"induction,{P1δ,...,Pnδ} |≂Aδ.

Siδ(B) = 1,Bδ=BetAδ=¬¬B. Par hypothèse d"induction on a{P1δ,...,Pnδ} |≂B,

par le lemme 2.7(ii),|≂(B→ ¬¬B)et donc par Modus Ponens,{P1δ,...,Pnδ} |≂¬¬B.

- SiA= (B→C), avec par hypothèse d"induction, pour touteδ,{P1δ,...,Pnδ} |≂Bδ

et{P1δ,...,Pnδ} |≂Cδ. Il y a trois cas. Tout d"abord, siδ(B) = 0, alorsBδ=¬B, et

δ(B→C) = 1, doncAδ=A. On a{P1δ,...,Pnδ} |≂¬B, par le lemme 2.7 (iii), 5 |≂(¬B→(B→C)), et par Modus Ponens,{P1δ,...,Pnδ} |≂(B→C). Deuxième cas, siδ(B) = 1etδ(C) = 1, doncCδ=CetAδ=A= (B→C). On a par hypothèse{P1δ,...,Pnδ} |≂C, par l"axiome (A1),|≂(C→(B→C)), donc par Modus Ponens,{P1δ,...,Pnδ} |≂(B→C). Dernier cas, siδ(B) = 1etδ(C) = 0, doncδ(A) = 0. Par induction,{P1δ,...,Pnδ} |≂B

et{P1δ,...,Pnδ} |≂¬C. Par le lemme 2.7 (iv),|≂(B→(¬C→ ¬(B→C))). En

appliquant le Modus Ponens deux fois de suite, on obtient bien{P1δ,...,Pnδ} |≂¬(B→

C)(=Aδ).?

On peut maintenant démontrer la proposition 2.11: SoitAune tautologie. Alors pourtouteapplicationδde{P1,...,Pn}dans{0,1}, A δ=Aet donc, par le lemme précédent,{P1δ,...,Pnδ} |≂A. En particulier, pour touteδ0application de{P1,...,Pn-1}dans{0,1}, on a {P1δ0,...,Pn-1δ0,Pn} |≂A et {P1δ0,...,Pn-1δ0,¬Pn} |≂A.

Par le lemme 2.8, on déduit que :

{P1δ0,...,Pn-1δ0} |≂A, et ceci à nouveaupour touteδ0. En appliquant ce raisonnement plusieurs fois on arrive à {P1} |≂Aet{¬P1} |≂A et en appliquant une dernière fois le lemme 2.8, à |≂A.? Corollaire 2.13SoientΣun ensemble fini de formules etAune formule. SiΣ?A, alorsΣ|≂A.

Démonstration: Par hypothèse,Σest fini, on raisonne par récurrence sur sa cardinalité.

SiΣest vide (de cardinalité nulle) , alors c"est exactement la proposition 2.11. Il suit facilement queΣ0?(Dn→A). En effet, soitδqui satisfaitΣ, alors siδ(Dn) = 0, on a toujoursδ((Dn→A)) = 1; siδ(Dn) = 1,δsatisfaitΣ0? {Dn}, doncδ(A) = 1et

δ((Dn→A)) = 1aussi.

Par hypothèse de récurrence,Σ0|≂(Dn→A). Par le lemme 2.5,Σ0? {Dn} |≂A.?

2.2.2 Les théorèmes de complétude et de compacité

On peut déduire le théorème de complétude général du corollaire précédent et du théorème

de compacité:

Proposition 2.14(Théorème de complétude)

SoientΣun ensemble de formules etAune formule. SiΣ?A, alorsΣ|≂A. 6 Démonstration: SiΣ?A, par compacité, il existeΣ0sous-ensemble fini deΣtel que

0?A(voir section 1). Par le corollaire 2.13,Σ0|≂A, et doncΣ|≂A.?

Mais on trouve souvent des preuves directes du théorème de complétude général, avec un ensemble de formulesΣinfini. On peut alors en déduire le théorème de compacité: SoitΣun ensemble de formules non satisfaisable. On a vu (1.2) que alors il existe une

formuleAtelle queΣ?AetΣ? ¬A. Par le théorème de complétude,Σ|≂AetΣ|≂¬A.

Par le lemme de finitude ( 2.4), il y aΣ1etΣ2, sous-ensembles finis deΣ, tels queΣ1|≂A

etΣ2|≂¬A, Par le lemme de validité (2.10),Σ1?AetΣ2? ¬A. Le sous-ensemble fini

1?Σ2est donc non satisfaisable.

En fait on démontre souvent le théorème de complétude sous la forme équivalente suivante: Proposition 2.15SoitΣun ensemble de formules non contradictoire, alorsΣest satis- faisable. Démonstration de l"équivalence des propositions 2.14 et 2.15: Supposons 2.14, et soitΣun ensemble de formules qui n"est pas satisfaisable. Alors

par (1.2), il existe une formuleAtelle queΣ?AetΣ? ¬A. Par 2.14,Σ|≂AetΣ|≂¬A,

doncΣest contradictoire. Maintenant supposons 2.15. SiΣ?A, alors (1.2)Σ?{¬A}est non satisfaisable. Par

2.15, doncΣ?{¬A}est contradictoire, et donc par 2.9,Σ?{¬A} |≂A, et bien sûr on a

aussiΣ? {A} |≂A. Par 2.8,Σ|≂A.? 7quotesdbs_dbs28.pdfusesText_34

[PDF] calcul des propositions exercices corrigés

[PDF] le resultat dune multiplication est

[PDF] comment calculer le taux de possession du stock

[PDF] cout de stockage annuel

[PDF] calcul du stock moyen

[PDF] exercice cout de passation et possession

[PDF] calcul tangente formule

[PDF] calcul tangente fonction

[PDF] calcul tangente en ligne

[PDF] calculer tangente calculatrice

[PDF] a quoi sert le sinus

[PDF] taux d'évolution successif

[PDF] imc 22 femme

[PDF] tableau imc femme

[PDF] imc 23 femme