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.
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.
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.
É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.
Commentaires