Les ordinateurs sont-ils logiques ? 1 : Logique propositionnelle

lundi 7 décembre 2009
par  Alain BUSSER

En logique propositionnelle, on peut vérifier la validité d’une proposition (savoir si elle est vraie ou fausse) en remplissant un tableau de ce type (exemple de la commutativité de $\vee$, le « ou inclusif ») :

$_q \fbox{(p \vee q) \Leftrightarrow (q \vee p)} ^p$ 0 1
0 1 1
1 1 1

Comme il n’y a que des « 1 » dans le tableau, $(p \vee q)\Leftrightarrow (q \vee p)$ est toujours vrai (c’est une tautologie) indépendamment des valeurs de vérité de $p$ et $q$. Tester la validité d’une proposition ayant $n$ variables propositionnelles nécessite de remplir un tableau ayant $2^n$ cases (sans les bords) ce qui risque d’être long [1]. Mais un ordinateur peut le faire en un temps raisonnable, et le logiciel de calcul formel Yacas était muni d’une fonction CanProve qui faisait quelque chose d’équivalent à ce remplissage automatique du tableau (dans l’exemple ci-dessus, elle répond « True »). Et comme Yacas a été incorporé à MathRider [2], MathRider permet d’explorer le calcul propositionnel comme on va le faire dans cet article.

On suppose donc MathRider téléchargé, installé et démarré. Pour entrer une question sur une proposition, on doit faire « shift+Entrée » et pas « Entrée » seul.

Négation

Une proposition $p$ peut-elle être vraie et fausse en même temps ?

CanProve(p And Not p)

La réponse False signifie non pas que $p \wedge \neg p$ n’est pas vraie (sous-entendu : pas tout le temps) mais qu’elle est totalement et irrémédiablement fausse. C’est une antilogie notée $\bot$.

Une proposition peut-elle être autre chose que vraie ou fausse ?

CanProve(p Or Not p)

La réponse True signifie que non, ce qui s’appelle le principe du tiers exclu.

Lois de DeMorgan (hors programme)

Avec

PrettyForm(CanProve(Not(p Or q)))

la réponse Not( p ) And Not( q ) signifie que $\neg(p \vee q)$ est logiquement équivalente à $\neg p \wedge \neg q$ :

$$\neg(p \vee q) \Leftrightarrow \neg p \wedge \neg q$$

C’est la première des deux lois de De Morgan. La seconde

$$\neg(p \wedge q) \Leftrightarrow \neg p \vee \neg q$$

s’explique de la même manière :

PrettyForm(CanProve(Not(p And q)))

donne Not( p ) Or Not( q ) comme réponse.

Quel est le contraire de $p \Rightarrow q$ ?

PrettyForm(CanProve(Not(p => q)))

répond p And Not( q ) : Le contraire de $p \Rightarrow q$ est donc $p \wedge \neg q$. La seule manière pour qu’une implication soit fausse est que sa prémisse soit vraie mais pas sa conclusion. Par exemple $2+2=4 \Rightarrow 0=1$ est fausse (mais pas sa réciproque ; voir à l’onglet « Implication » pour plus de détails).

Quel est le contraire du contraire de $p$ ?

CanProve(Not Not p)

répond juste p, alors que

CanProve(Not Not p =>p)

répond True, ainsi que

CanProve(p => Not Not p)

Tout ceci se résume par l’équivalence logique entre une proposition $p$ et la négation de sa négation : $p \Leftrightarrow \neg \neg p$.

La double négation est souvent considérée comme une figure de style lourde et donc à éviter [3]. Si un professeur d’anglais déconseille à ses étudiants de dire « she’s not ugly » d’une fille qu’il trouve belle, c’est bien parce que celle-ci risque de n’entendre qu’une seule négation et de mal comprendre le message.

Lorsque Raymond Smullyan fait son cours de logique sur la double négation comme affirmation, il termine par :

Par contre je ne connais aucune langue où, au contraire, la double affirmation équivaut à une négation.

ce à quoi, un jour, un étudiant du fond de l’amphi lui a répondu irrévérencieusement mais avec humour

Ouais, ouais, cause toujours...

On peut coder le discours de Smullyan par $\neg(p \wedge p \Leftrightarrow \neg p)$

Conjonction

Commutativité

CanProve(p And q => q And p)

et la variante en échangeant $p$ et $q$ montrent l’équivalence logique entre $p \wedge q$ et $q \wedge p$. Bien que stricto sensu ces propositions soient seulement équivalentes et non égales, la construction de l’algèbre de Lindenbaum justifie qu’on parle de commutativité de la conjonction [4].

Associativité

PrettyForm(CanProve((p And q) And r))

Permet de vérifier que $(p \wedge q) \wedge r \Leftrightarrow p \wedge (q \wedge r)$ (Exercice : Comment ?)

Distributivité

PrettyForm(CanProve((p And q) Or (p And r)))

donne pour résultat p And ( q Or r ), ce qui constitue une sorte de factorisation : On dit que la conjonction $\wedge$ est distributive par rapport à la disjonction $\vee$.

L’illustration par un diagramme de Venn revient à dire que la zone qu’on voit en mauve (parce qu’elle est à la fois rouge et bleue) peut être indifféremment décrite comme la réunion de deux lentilles ou comme l’intersection du domaine bleu (deux disques) et du rouge :

Lien avec l’implication

CanProve((p And q) => p)

répond True, alors que la réciproque

PrettyForm(CanProve(p => (p And q)))

répond Not( p ) Or q ce qui représente $p \Rightarrow q$ (voir l’onglet « implication ») : On a donc $p \wedge q \Rightarrow p$ (tout triangle rectangle isocèle est rectangle) mais pas $p \Rightarrow p \wedge q$.

Raisonnement par disjonction des cas

PrettyForm(CanProve((p => q) And (Not p => q)))

répond ( Not( p ) Or q ) And ( p Or q ) et MathPiper est bloqué à ce stade, le pauvre. En effet cette réponse est simplifiable par distributivité en $(\neg p \wedge p) \vee q$, soit en $\bot \vee q$ soit encore en $q$ : $(p \Rightarrow q) \wedge (\neg p \Rightarrow q)$ est équivalente à $q$, et en particulier implique $q$. Mais ça, MathPiper le sait :

>PrettyForm(CanProve(((p => q) And (Not p => q)) => q))

affiche bien True, ce qui veut dire que

$$\left((p \Rightarrow q) \wedge (\neg p \Rightarrow q) \right) \Rightarrow q$$

C’est le principe du raisonnement par disjonction des cas (ici il n’y a que deux cas : $p$ et $\neg p$).

Disjonction

Commutativité

CanProve(p Or q => q Or p)

et la variante en échangeant $p$ et $q$ montrent l’équivalence logique entre $p \vee q$ et $q \vee p$. Voir à l’onglet « Conjonction » pourquoi on se permet d’appeler ça une commutativité.

Associativité

PrettyForm(CanProve((p Or q) Or r))

Permet de vérifier que $(p \vee q) \vee r \Leftrightarrow p \vee (q \vee r)$.

Comment ?

Distributivité

PrettyForm(CanProve(p Or (q And r)))

affiche ( p Or q ) And ( p Or r ) ce qui correspond à un développement : La disjonction $\vee$ est elle aussi distributive par rapport à la conjonction $\wedge$. C’est la principale différence entre l’algèbre de Boole et celle des réels.

Lien avec l’implication

CanProve(p => (p Or q))

affiche True ce qui veut dire que $p \Rightarrow p \vee q$ : Si deux droites sont coplanaires alors elles sont sécantes ou parallèles. La réciproque n’est pas (toujours) vraie :

PrettyForm(CanProve((p Or q) => p))

affiche Not( q ) Or p, soit $p \Leftarrow q$ (voir onglet suivant).

Implication

Définition de l’implication

PrettyForm(CanProve(p => q))

affiche Not( p ) Or q : Au secours ! En logique propositionnelle, on définit la proposition $p \Rightarrow q$ comme étant $\neg p \vee q$ : L’implication entre $p$ et $q$ signifiant que si $p$ est vraie, $q$ l’est nécessairement aussi, et que donc si $q$ est fausse, $p$ aussi : ou bien $q$ est vraie, ou alors c’est $p$ qui est fausse ; c’est exactement ce que vient de répondre MathPiper.

Cas particuliers :

CanProve(p => True)

et

CanProve(False => p)

affichent tous deux True ce qui signifie que du point de vue de la logique propositionnelle, des propositions telles que « S’il pleut alors 2+2=4 » ou « Si 0=1 alors ce triangle est isocèle » sont vraies, ce qui est contraire à l’idée que l’intuition se fait de l’implication (lien de cause à effet).

Réflexivité

CanProve(p => p)

affiche True ce qui veut dire que toute proposition, qu’elle soit vraie ou fausse, s’implique elle-même.

Transitivité

De « tout carré est un rectangle » et de « les angles d’un rectangle sont droits » on souhaite pouvoir déduire que « les angles d’un carré sont droits », ce qui signifie qu’il est hautement souhaitable que $\left((p \Rightarrow q) \wedge (q \Rightarrow r)\right) \Rightarrow (p \Rightarrow r)$ soit une tautologie. C’est bien le cas :

CanProve(((p => q) And (q => r)) => (p => r))

affiche bien True.

Modus Ponens

CanProve((p And (p => q))=>q)

affiche True. Ce modus ponens permet de déduire, à partir de $p$ et de $p \Rightarrow q$, la proposition $q$. Par exemple « $3^2+4^2=5^2$ ; or si $a^2+b^2=c^2$, le triangle de côtés $a$, $b$ et $c$ est rectangle d’après la réciproque de Pythagore. Donc le triangle 3, 4, 5 est rectangle ».

Le modus ponens est si fondamental en logique propositionnelle qu’une démonstration est un exercice classique en logique propositionnelle.

En voici une ébauche

Puisque $p \Rightarrow q$ est équivalent à $\neg p \vee q$, le modus ponens peut aussi s’écrire $p \wedge (\neg p \vee q) \Rightarrow q$, soit par distributivité de $\wedge$ par rapport à $\vee$ :

$$(p \wedge \neg p) \vee (p \wedge q) \Rightarrow q$$

Mais le premier terme est $\bot$ d’après l’onglet « négation », et le modus ponens est donc équivalent à $(p \wedge q) \Rightarrow q$ qu’on a vu à l’onglet « conjonction ».

Le modus ponens n’est qu’une implication, pas une équivalence :

PrettyForm(CanProve(p And (p => q)))

ne répond pas q mais p And q ce qui est plus fort. En effet $q$ n’est pas la seule chose qu’on puisse déduire de $p \Rightarrow q$, il y a aussi $p$...

Réciproque

PrettyForm(CanProve((p => q) => (q => p)))

affiche Not( q ) Or p, ce qui confirme qu’une implication n’est pas forcément équivalente à sa réciproque (d’après MathPiper, $p \Rightarrow q$ n’implique $q \Rightarrow p$ que si $q \Rightarrow p$).

Contraposée

D’une part,

PrettyForm(CanProve(Not q => Not p))

affiche la même chose que

PrettyForm(CanProve(p => q))

et d’autre part

PrettyForm(CanProve((Not q => Not p) => (p =>q)))

et

PrettyForm(CanProve((p => q) => (Not q => Not p)))

affichent tous deux True : Une implication est logiquement équivalente à sa contraposée.

Lien entre contraposée et démonstration par l’absurde

Montrer $p$ revient à montrer $\top \Rightarrow p$ qui lui est équivalente ($\top$ étant une tautologie quelconque). Or la contraposée de cette dernière est $\neg p \Rightarrow \neg \top$, soit $\neg p \Rightarrow \bot$ : On suppose $p$ fausse et on en déduit une antilogie (par exemple une contradiction $q \vee \neg q$) : C’est le principe de la démonstration par l’absurde.

Équivalence logique

PrettyForm(CanProve((p => q) And (q => p)))

affiche ( Not( p ) Or q ) And ( Not( q ) Or p ) ce qui signifie que l’équivalence logique entre $p$ et $q$ n’est pas simplifiable en logique propositionnelle.


[1Une version dynamique, en JavaScript, se trouve dans ce cours de Seconde.

[2sous le nom de MathPiper qui n’est rien d’autre qu’un portage Java de Yacas

[3pas pour Corneille chez qui « je ne te hais point » est un mot d’amour.

[4La construction est résumée à la page 5 du document pdf téléchargeable au bas de cet article.


Commentaires