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
, le « ou inclusif ») :
| 0 | 1 | |
| 0 | 1 | 1 |
| 1 | 1 | 1 |
Comme il n’y a que des « 1 » dans le tableau,
est toujours vrai (c’est une tautologie) indépendamment des valeurs de vérité de
et
. Tester la validité d’une proposition ayant
variables propositionnelles nécessite de remplir un tableau ayant
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
peut-elle être vraie et fausse en même temps ?
CanProve(p And Not p)
La réponse False signifie non pas que
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
.
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
?
PrettyForm(CanProve(Not(p => q)))
répond p And Not( q ) : Le contraire de
est donc
. La seule manière pour qu’une implication soit fausse est que sa prémisse soit vraie mais pas sa conclusion. Par exemple
est fausse (mais pas sa réciproque ; voir à l’onglet « Implication » pour plus de détails).
Quel est le contraire du contraire de
?
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
et la négation de sa négation :
.
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 ![]()
Conjonction
Commutativité
CanProve(p And q => q And p)
et la variante en échangeant
et
montrent l’équivalence logique entre
et
. 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
(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
est distributive par rapport à la disjonction
.
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
(voir l’onglet « implication ») : On a donc
(tout triangle rectangle isocèle est rectangle) mais pas
.
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
, soit en
soit encore en
:
est équivalente à
, et en particulier implique
. Mais ça, MathPiper le sait :
>PrettyForm(CanProve(((p => q) And (Not p => q)) => q))
affiche bien True, ce qui veut dire que
![]()
C’est le principe du raisonnement par disjonction des cas (ici il n’y a que deux cas :
et
).
Disjonction
Commutativité
CanProve(p Or q => q Or p)
et la variante en échangeant
et
montrent l’équivalence logique entre
et
. 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
.
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
est elle aussi distributive par rapport à la conjonction
. 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
: 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
(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
comme étant
: L’implication entre
et
signifiant que si
est vraie,
l’est nécessairement aussi, et que donc si
est fausse,
aussi : ou bien
est vraie, ou alors c’est
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
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
et de
, la proposition
. Par exemple «
; or si
, le triangle de côtés
,
et
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
n’est pas la seule chose qu’on puisse déduire de
, il y a aussi
...
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,
n’implique
que si
).
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
et
n’est pas simplifiable en logique propositionnelle.

) : C’est le principe de la démonstration par l’absurde.
Commentaires