Calul Propositionnel Résumé de cours d’après les transparents
(du calcul propositionnel) variable propositionnelle Sont synonymes: formule (du calcul propositionnel) proposition (complexe) Les propositions ou formules sont définies ainsi: 1 Les propositions atomiques sont des propositions 2 Si Xest une proposition, alors (:X) ("non X", la négation de X) est une pro-position 3 Si Xet Ysont des
Calcul propositionnel: déductions syntaxiques
Calcul propositionnel : déductions syntaxiques Axiomes logiques et règles d’inférence du système formel « PR » Un raisonnement logique peut être rédigé sous forme de démonstration, soit d’un théorème, soit d’une conséquence de certaines hypothèses Pr Ousmane THIARE Calcul propositionnel: déductions syntaxiques 16 avril
Logique et Calcul Propositionnel
Logique et Calcul Propositionnel Syntaxe du calcul propositionnel Definition (Formule bien formee)´ On definit une formule bien form´ ee (´ fbf) par : p, ou` p est une variable propositionnelle (A ∨B) (A ∧B) (¬A) (A → B) : si A alors B (A ↔ B) ou` A et B sont des variables propositionnelles ou des formules bien formees ´
Théorème de complétude du calcul propositionnel
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 Σ est satisfaisable si il existe une distribution de valeurs de vérité, δ, qui satisfait toutes les formules de Σ, c’est-à-dire telle que, pour toute formule B ∈ Σ, δ(B) = 1
Informatique Département d’informatique module : Logique
2) Soit CPF’ le calcul propositionnel formel obtenu à partir de CPF en remplaçant l’axiome Ax3 par l’axiome : ( B A) (( B A) B) (Ax3’) Élaborer une démonstration pour montrer que la formule F2 est un théorème dans CPF’ : (2 pts)
Informatique Département d’informatique module : Logique
II) Soit CPF’ le calcul propositionnel formel obtenu à partir de CPF en remplaçant l’axiome Ax3 par l’axiome Ax3’ : ( B A) (( B A) B) À l’aide de la méthode axiomatique, montrer, dans CPF’, ce qui suit :
Specimen promo Mathématiques BTS CG - Tout en fiches - 72876
∎ 5 Comment exploiter un logiciel de calcul formel ? 64 ∎ 6 Comment calculer l’équation d’une tangente ? 66 Fiche 10 Tableau de variations et équation f (x) = k ∎ 1 Comment déterminer le tableau de variation à partir de la fonction dérivée ? 71
LOG TD 4 - IRISA
Ce TD est consacr e au probl eme de la validit e des formules du calcul propositionnel, et en particulier a l’ etude de la m ethode r esolution Introduite en 1965 par Robinson, le syst eme de r esolution est un syst eme formel qui utilise des formules sous-formes de clauses, qui n’a pas d’axiomes, et qui comporte deux r egles d’inf erence
[PDF] le resultat d'une 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] calcul taux d'évolution annuel moyen excel
[PDF] taux d'évolution successif
[PDF] imc 22 femme
[PDF] tableau imc femme
MAGISTERE MATH.-INFO. (2003-2004) Logique
E. Bouscaren
Théorème de complétude du calcul
propositionnelNotes complémentaires (0)
1 Quelques rappels de sémantique
Définition: Un ensemble de formulesΣestsatisfaisablesi il existe une distribution devaleurs 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 queAestconsé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.? 12 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).
2Démonstration:
(1)A1= ((A→((A→A)→A))→((A→(A→A))→(A→A))), (Axiome2 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 que0|≂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, B1,...,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
3Par 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Σ|≂AetΣ|≂¬A. Par le lemme 2.7 (iii),|≂(¬A→(A→B)). En appliquant le Modus Po-
nens deux fois, on obtient bienΣ|≂B.? 42.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, A1,...,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 àAiinfé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δ} |≂Bet{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 que0?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 uneformuleAtelle 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 fini1?Σ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. Alorspar (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