LILaC
INTRODUCTION À LA LOGIQUE
Un hyper-cours de répétition
- Annexes -
Langage de la logique propositionnelle : annexes
Introduction et motivation
Besoin d'un langage formel (mathématique) pour étudier les
inférences
-
On se limite à des connecteurs propositionnels
(connecteurs associant des propositions, et non des variables et des
propositions,
comme dans la logique des prédicats,
cf. aussi l'introduction).
-
contradiction FALSE :
`` faux ''
(connecteur 0-aire)
-
négation ~A :
`` non A '' (` A n'est pas le cas ')
(connecteur unaire)
-
conjonction A ∧ B :
`` A et B ''
(connecteur binaire)
-
disjonction A ∨ B :
`` A ou B ''
(connecteur binaire)
-
implication A -> B :
`` si A alors B ''
(connecteur binaire)
-
Notion de proposition atomique (formule atomique) = enoncé indécomposable ;
il_pleut, la_route_est_mouillée, ...
plus abstraitement : p, q, ...
Retour
Remarque sur des jeux de connecteurs alternatifs
Remarque.
Notre jeu de connecteurs primitifs est
{FALSE , ~ , ∧ , ∨ , ->}.
Parfois on choisit {-> , FALSE}
comme jeu de connecteurs primitifs, et on définit
-
~A comme A -> FALSE,
-
A ∨ B comme (A -> FALSE) -> B, et
-
A ∧ B comme (A -> (B-> FALSE)) -> FALSE.
Il est aussi possible de déclarer
{~ , ∧ , v}
primitifs, et de définir
-
FALSE comme p ∧ ~p,
pour un atome p quelconque, et
-
A -> B comme ~A ∨ B.
Les différentes
formes normales et
méthodes de démonstration automatique
peuvent opérer sur des jeux de connecteurs primitifs différents,
et ont souvent recours à
l'élimination préalable de connecteurs.
Le jeu de connecteurs {-> , FALSE} est minimal,
dans le sens qu'il n'existe pas de jeu plus petit permettant de définir
toutes les autres connecteurs.
Le jeu {~ , ∧ , v} n'est pas minimal, si on admet que
A ∨ B peut être défini comme ~(~A ∧ ~B).
Par contre, et {& , ~} et
{v , ~} sont minimaux, ainsi que
{-> , ~}.
Retour
Remarque sur une définition plus constructive de FOR
Remarque.
(... à completer)
Retour
Rappel sur les démonstrations par induction
(... à completer)
Retour
Langage de la logique propositionnelle : exemples
Exemples de formules
| formules bien formés | `non-formules'
|
| p | p ∧
|
| (~p) | p ~ q
|
| FALSE | ∧ p
|
| (p ∧ q) | ( ∧ )
|
| (~(p ∧ q) ∨ r) | (p
|
| (q -> (r ∨ q)) | (q -> (r ∨ q)
|
Retour
Exemples de sous-formules
- Considérons la formule ((p ∨ q) ∧ ~p).
p en est une sous-formule, ainsi que
(p ∨ q) et (~p), tandis que
(q ∧ ~p) ne l'est pas.
p a deux occurrences dans ((p ∨ q) ∧ ~p), et
(p ∨ q) une.
- l'ensemble des sous-formules de (((p ∨ q) ∧ ~p) -> FALSE) est
{ (((p ∨ q) ∧ ~p) -> FALSE) , ((p ∨ q) ∧ ~p) , FALSE ,
(p ∨ q) , (~p) , p , q }.
Retour
Exemples de substitutions
| (p ∨ q)[p\r] | = r ∨ q
|
| (p -> q)[q\p] | = p -> p
|
| (p -> q)[r\s] | = p -> q
|
| ((p ∨ q) ∧ ~p)[p\~p] | = (~p ∨ q) ∧ ~~p
|
| ((p ∨ q) ∧ ~p)[p\(r ∧ s)] | = ((r ∧ s) ∨ q) ∧ ~(r ∧ s)
|
| (p -> r)[p\(q -> s)] | = (q -> s) -> r
|
N.B. : remarquer l'importance du parenthésage
dans les deux dernières exemples
Retour
Théorie des modèles de la logique propositionnelle : annexes
Introduction et motivation
En théorie des modèles, on fixe d'abord un ensemble de modèles
(aussi appellés valuations ou interpretations).
Ensuite, pour un modèle donné, on stipule des conditions de vérité
permettant d'établir pour n'importe quelle formule A du langage
si A est vraie ou fausse dans ce modèle.
Pour la logique propositionnelle, les notions de modèle
et de vérité dans un modèle sont déterminés par les
deux postulats suivants :
-
bivalence : une formule est soit vraie, soit fausse
-
vérifonctionnalité : la valeur de vérité d'une
formule non-atomique est déterminé par les valeurs de ses
constituants
Remarque.
Des alternatives existent dans les 2 cas. On peut postuler
l'existence de 3 valeurs de vérité 0, ½, 1 ;
voir même 0, ¼, ½, ¾, 1 , ainsi de
suite (ceci amène à la définition de logiques multi-valuées).
Le refus du postulat de vérifonctionnalité entraîne
l'existence d'un ou plusieurs connecteurs dont la valeur de vérité
n'est pas fonction des sous-formules (ceci amène à la définition
de logiques non-vérifonctionnelles, dites aussi intensionnelles,
qui font partie des logiques non-classiques).
Nous acceptons ces deux postulats ici. Il suffit alors de définir,
pour chaque connecteur, son comportement par rapport à ses sous-formules
immédiates afin de permettre d'associer une valeur de vérité
à chaque formule, étant donné une attribution de valeurs
de vérité aux variables propositionnelles. C'est ce qu'on
appelle les tables de vérité pour un connecteur.
| A
| B | A ∧ B | A ∨ B | A -> B
|
| 0 | 0 | 0 | 0 | 1
|
| 0 | 1 | 0 | 1 | 1
|
| 1 | 0 | 0 | 1 | 0
|
| 1 | 1 | 1 | 1 | 1
|
Étant donné une formule quelconque, il est alors possible
de construire la table de vérité, en prolongeant les valeurs
des variables propositionnelles moyennant les tables de vérité
pour les connecteurs.
| p | q | r | p ∨ q | (p ∨ q) ∧ r
|
| 0 | 0 | 0 | 0 | 0
|
| 0 | 0 | 1 | 0 | 0
|
| 0 | 1 | 0 | 1 | 0
|
| 0 | 1 | 1 | 1 | 1
|
| 1 | 0 | 0 | 1 | 0
|
| 1 | 0 | 1 | 1 | 1
|
| 1 | 1 | 0 | 1 | 0
|
| 1 | 1 | 1 | 1 | 1
|
Chaque ligne d'une table de vérité pour une formule A
donne les valeurs de vérité pour toutes les variables propositionnelles
apparaissant dans A. Ceci peut être vue comme la déscription
d'un état possible du monde. Généralement, c'est une
application de l'ensemble des variables propositionnelles ATM
dans {0,1}, qu'on appellera interpretation.
La méthode de balayage
peut être vue comme une stratégie sophistiquée de construction
des tables de vérité.
Retour
Remarque sur validité et satisfiabilité
Remarque.
A est insatisfiable si
I(A) = 0 pour toute interpretation I, et
A est invalide si
il existe une interpretation I t.q. I(A) = 0.
Les formules valides sont forcément satisfiables, et
les formules insatisfiables sont forcément falsifiables.
Retour
Plus sur la conséquence logique
Le problème de conséquence logique A |= B
se réduit au problème de validité |= A -> B :
Théorème de la conséquence logique
(version sémantique du théorème de déduction).
A |= B ssi |= A -> B.
Démonstration.
A |= B est le cas ssi
tout modèle de A est aussi un modèle de B, i.e.,
I(A) = 1 implique I(B) = 1 pour toute interprétation I.
Ce qui est équivalent à I(A -> B) = 1 pour tout I, i.e., à
la validité de A -> B.
Remarque sur des ensembles d'hypothèses infinis.
On peut généraliser la définition de conséquence logique à des
ensembles d'hypothèses quelconques, qui peuvent en particulier être infinis.
Une formule A
est alors conséquence logique d'un ensemble de formules S
(noté S |= A)
ssi tout modèle de S
est un modèle de A.
Par abus de notation, on écrit alors souvent
A1,...,An |= B à la place de {A1,...,An} |= B, et donc
A |= B à la place de {A} |= B. Et même,
S,A |= B à la place de S U {A} |= B
(où U denote l'union ensembliste).
Dans ce cadre, s'applique le
théorème de compacité.
Retour
Théorie des modèles de la logique propositionnelle : exemples
Exemple d'interpretation
Soit ATM = {p1, p2, ...}.
Alors l'application I telle que
I(p1) = 1,
I(p2) = I(p3) = ... = 0
est une interpretation.
L'interprétation étendue correspondante est un modèle pour
p1 ∨ p2 et
(p1 ∧ p2) -> (p1 ∧ p1),
mais non pour
p1 ∧ (p2 ∨ ~p1) :
-
I(p1 ∨ p2) = 1
-
I((p1 ∧ p2) -> (p1 ∧ p1)) = 1
-
I(p1 ∧ (p2 ∨ ~p1)) = 0
Retour
Exemples de formules valides et satisfiables
| formules valides
| formules satisfiables et invalides
| formules insatisfiables
|
| p ∨ ~p | p | p ∧ ~p
|
| p ∨ ~p ∨ q | p ∨ q | FALSE
|
| q -> q | p -> q | p ∧ ~p ∧ q
|
| (p ∧ q) -> (q ∧ p) | q -> (q ∧ p)
| (p ∨ q) ∧ ~p ∧ ~q
|
| (p ∧ q) -> p | (p ∨ q) -> p
| (p ∧ p) -> q
|
| (p ∧ ~p) -> q | (p ∧ r) -> q |
|
| FALSE -> q | p ∨ q |
|
| (p -> ~p) -> ~p | (p -> q) -> (q -> p) |
|
| (p -> FALSE) -> ~p | (p -> q) -> (~p -> ~q) |
|
Retour
Exemples de conséquences logiques
-
{p} |= p
-
{p , q} |= p
-
{p , q} |= q
-
{p , q} |= q ∧ p
-
{p , p -> q} |= q
Retour
Théorie de la preuve de la logique propositionnelle : annexes
Introduction et motivation
L'objectif de la théorie de la preuve est de donner une
caractérisation finie des formules valides,
en se basant sur un (petit) ensemble de `vérités premières' : les axiomes,
et un (petit) ensemble de règles permettant de produire toutes les vérités :
les règles d'inférence.
Retour
Remarque sur une axiomatisation avec une règle de substitution uniforme
Remarque.
Dans les schémas d'axiomes, A , B , C
sont des schémas de formules (représentant des
formules complexes, pas forcement atomiques).
On peut éviter ces schémas d'axiomes et travailler avec des axiomes.
P.ex. le premier schéma d'axiome deviendrait l'axiome
p -> (q -> p),
où p et q ne sont pas des schémas de formules
mais des variables propositionnelles
(formules atomiques).
Dans ce cas, on a besoin de la règle de substitution uniforme :
A
___________
A[p\B]
Cette règle pourra alors également être appliquée dans
les preuves
Retour
Remarque sur des ensembles d'hypothèses infinis
Remarque.
Comme dans le cas de la
conséquence logique,
on peut généraliser la définition de déduction à des ensembles
d'hypothèses quelconques, qui peuvent en particulier être infinis.
Des conventions notationnelles similaires s'appliquent.
On a également le
théorème de compacité.
Retour
Axiomatique de la logique propositionnelle : exemples
Exemples de preuve
Preuve de
A -> A :
-
A -> (A -> A)
instance de A -> (B -> A)
-
(A -> (A -> A)) -> ((A -> ((A -> A) -> A)) -> (A -> A))
instance de (A -> B) -> ((A -> (B -> C)) -> (A -> C))
-
((A -> ((A -> A) -> A)) -> (A -> A))
obtenue par Modus Ponens à partir de 1. et 2.
-
A -> ((A -> A) -> A)
instance de A -> (B -> A)
-
A -> A
obtenue par Modus Ponens à partir de 3. et 4.
Plus schématiquement :
A -> (A -> A)
(A -> (A -> A)) -> ((A -> ((A -> A) -> A)) -> (A -> A))
_________________________________________________________________________
A -> ((A -> A) -> A)
((A -> ((A -> A) -> A)) -> (A -> A))
_________________________________________________________________
A -> A
Retour
Exemples de formules prouvables et consistantes
| formules prouvables
| formules consistantes et non prouvables
| formules inconsistantes
|
| p ∨ ~p | p | p ∧ ~p
|
| p ∨ ~p ∨ q | p ∨ q | FALSE
|
| q -> q | p -> q | p ∧ ~p ∧ q
|
| (p ∧ q) -> (q ∧ p) | q -> (q ∧ p)
| (p ∨ q) ∧ ~p ∧ ~q
|
| (p ∧ q) -> p | (p ∨ q) -> p
| (p ∧ p) -> q
|
| (p ∧ ~p) -> q | (p ∧ r) -> q |
|
| FALSE -> q | p ∨ q |
|
| (p -> ~p) -> ~p | (p -> q) -> (q -> p) |
|
| (p -> FALSE) -> ~p | (p -> q) -> (~p -> ~q) |
|
Retour
Exemples de déductions
-
p |- p
-
p , q |- p
-
p , q |- q
-
p , q |- q ∧ p
-
p , p -> q |- q
Retour
Propriétés de la logique propositionnelle : annexes
Introduction et motivation
théorie des modèles : définition de la notion de validité
théorie de la preuve : définition de la notion de prouvabilité
donc : quel est le rapport entre validité et prouvabilité ?
Les notions de validité et de prouvabilité devraient
caractériser les mêmes formules.
Retour
Adéquation et complétude forte
Théorème d'adéquation forte.
Si A1,...,An |- A alors A1,...,An |= A.
Démonstration : omise
Théorème de complétude forte.
Si A1,...,An |= A alors A1,...,An |- A.
Démonstration : omise
Retour
Compacité
Si l'on définit et la
conséquence logique et la
déduction
avec des ensembles de prémisses (potentiellement infinis),
s'applique alors le
Théorème de compacité.
S |= B ssi il existe un sous-ensemble fini S' de S
t.q. S' |= B.
Démonstration :
omise
Retour
Propriétés de la logique propositionnelle : exemples
Exemples d'application du théorème de remplacement des équivalences
Exemple
Soit la formule p1 ∨ (p2 ∨ p3).
En remplaçant
p2 ∨ p3 par
p3 ∨ p2 nous obtenons
p1 ∨ (p3 ∨ p2)
Comme |- p2 ∨ p3 <->
p3 ∨ p2, nous avons
|- p1 ∨ (p2 ∨ p3) <->
p1 ∨ (p3 ∨ p2).
Un corollaire
Corollaire.
Soit |- A <-> B et
|- B <-> C.
Alors |- A <-> C.
Retour
Forme normale conjonctive de la logique propositionnelle : annexes
Introduction et motivation
mise en forme normale = simplification de formules complexes
souvent étape préalable des procédures de démonstration automatique
Retour
Forme normale conjonctive de la logique propositionnelle : exemples
Exemples de formules en forme normale conjonctive
| en forme normale conjonctive | pas en forme normale conjonctive
|
| p ∨ ~q | FALSE
|
| ~p ∧ q | p -> q
|
| ~p ∧ p | ~~p
|
| (~p ∨ q) ∧ r | ~(p ∧ q)
|
| (~p ∨ q) ∧ (r ∨ ~s) | (~(p ∧ q) ∨ r)
|
Retour
Exemples de mise en forme normale conjonctive
(p ∧ q) ∨ (r ∧ s) :
-
((p ∧ q) ∨ r) ∧
((p ∧ q) ∨ s)
-
( p ∨ r) ∧
( q ∨ r) ∧
((p ∧ q) ∨ s)
-
( p ∨ r) ∧
( q ∨ r) ∧
( p ∨ s) &
( q ∨ s)
remarquer la croissance de la longueur de la formule qui resulte
de l'application de la loi de De Morgan
(p -> q) -> p :
-
~(~p ∨ q) ∨ p
-
(~~p ∧ ~q) ∨ p
-
( p ∧ ~q) ∨ p
-
(p ∨ p) ∧ (~q ∨ p)
( (p -> q) -> p) -> p :
-
~(~(~p ∨ q) ∨ p ) ∨ p
-
~((~~p ∧ ~q) ∨ p ) ∨ p
-
~(( p ∧ ~q) ∨ p ) ∨ p
-
(~( p ∧ ~q) ∧ ~p) ∨ p
-
((~ p ∨ ~~q) ∧ ~p) ∨ p
-
((~ p ∨ q) ∧ ~p) ∨ p
-
( ~ p ∨ q ∨ p) ∧
(~p ∨ p)
remarquer le retardement de l'application de la loi de De Morgan
(distribution de la disjonction sur la conjonction)
Retour
Déduction automatique pour la logique propositionnelle : annexes
Introduction et motivation
nécessité d'une procédure de décision :
comment savoir si une formule donnée A est valide ?
Retour
Déduction automatique pour la logique propositionnelle : exemples
Exemples pour la méthode de balayage
(p -> q) -> p :
-
élimination de ->
~(~p ∨ q) ∨ p
-
choix de p et substitution
(~(~TRUE ∨ q) ∨ TRUE) ∧ (~(~FALSE ∨ q) ∨ FALSE)
-
simplification
TRUE ∧ ~(~FALSE ∨ q)
~(~FALSE ∨ q)
~(TRUE ∨ q)
~TRUE
FALSE
La même formule, en commençant par substituer q :
-
élimination de ->
~(~p ∨ q) ∨ p
-
choix de q> et substitution
(~(~p ∨ TRUE) ∨ p) &(~(~p ∨ FALSE) ∨ p)
-
simplification
(~ TRUE ∨ p) &(~~p ∨ p)
(FALSE ∨ p) &(~~p ∨ p)
p &(~~p ∨ p)
-
choix de p et substitution
(TRUE &(~~TRUE ∨ TRUE)) ∧ (FALSE &(~~FALSE ∨ FALSE))
-
simplification
(~~TRUE ∨ TRUE) ∧ FALSE
FALSE
Retour
https://www.irit.fr/~Andreas.Herzig