Version de

La proposition biconditionnelle

On rencontre souvent, dans les textes scientifiques, la locution « si et seulement si » que d’aucun abrègent en « ssi ».

Exemple : Un triangle a ses trois côtés égaux si il a ses trois angles égaux.

Un tel énoncé signifie deux choses :

1) Si un triangle a ses trois côtés égaux, il a ses trois angles égaux.
2) Si un triangle a ses trois angles égaux, il a ses trois côtés égaux.

La proposition qui contient « si et seulement si » équivaut donc à deux propositions conditionnelles. Nous la nommerons une proposition biconditionnelle et nous poserons la définition (notre première définition) :

Df \equiv : \quad P\equiv Q\quad =df (P\supset Q)\wedge(Q\supset P).

Remarques

1. Au lieu du foncteur abréviatif \equiv, certains auteurs notent \leftrightarrow ou \Leftrightarrow.
2. II arrive fréquemment que, au vu du contexte, le langage courant se contente de « si\ldots{}alors », là où nous disons « ssi ».
Exemple : Ouvrant son porte-feuille quelqu’un dit : « Si j’ai 10€ sur moi, je vous les prête ». Il va ici de soi que « Si je vous prête 10€, alors je les ai sur moi ».
Il s’ensuit que chaque fois que l’on cherche à « traduire » un texte dans le formalisme logique, il faut être attentif, non seulement à l’expression adoptée, mais à sa signification. Certains raisonnements peuvent parfaitement être corrects avec \equivet n’être pas valides avec \supset.

La règle repdf rend superflue l’introduction de règles spécifiques pour le foncteur \equiv.

Exemples

[1] Soit à démontrer le théorème \vdash p\equiv\bullet p\wedge p. Cela signifie qu’il faut démontrer \vdash(p\supset\bullet p\wedge p)\wedge(p\wedge p\bullet\supset p) :

 \begin{tabular}{c|l|llcl} 1 &  & $p$ &  &  & hyp\tabularnewline \cline{3-3}  2 &  & \multicolumn{2}{l}{$p$} &  & 1, rep\tabularnewline 3 &  & \multicolumn{2}{l}{$p\wedge p$} &  & 1, 2, $\wedge$i\tabularnewline 4 & \multicolumn{3}{l}{$p\supset\bullet p\wedge p$} &  & 1-3, $\supset$i\tabularnewline 5 &  & \multicolumn{2}{l}{$p\wedge p$} &  & hyp\tabularnewline \cline{3-3}  6 &  & $p$ &  &  & 5, $\wedge$e\tabularnewline 7 & \multicolumn{3}{l}{$p\wedge p\bullet\supset p$} &  & 5-6, $\supset$i\tabularnewline 8 & \multicolumn{3}{l}{$(p\supset\bullet p\wedge p)\wedge(p\wedge p\bullet\supset p)$} &  & 4, 7, $\wedge$i\tabularnewline 9 & \multicolumn{3}{l}{$p\equiv\bullet p\wedge p$} &  & 8, repdf$\equiv$\tabularnewline \end{tabular}

[2] \vdash p\equiv p

 \begin{tabular}{c|l|llcl} 1 &  & $p$ &  &  & hyp\tabularnewline \cline{3-3}  2 &  & \multicolumn{2}{l}{$p$} &  & 1, rep\tabularnewline 3 & \multicolumn{3}{l}{$p\supset p$} &  & 1-2, $\supset$i\tabularnewline 4 & \multicolumn{3}{l}{$p\supset p$} &  & 3, rep\tabularnewline 5 & \multicolumn{3}{l}{$(p\supset p)\wedge(p\supset p)$} &  & 3, 4, $\wedge$i\tabularnewline 9 & \multicolumn{3}{l}{$p\equiv p$} &  & 5, repdf$\equiv$\tabularnewline \end{tabular}

Pour des références ultérieures, notons encore :

[3] \vdash p\wedge q\bullet\equiv\bullet q\wedge p

[4] \vdash(p\wedge q)\wedge m\bullet\equiv\bullet p\wedge(q\wedge m)

[5] \vdash(p\supset q\bullet\wedge\bullet q\supset p)\supset(p\equiv q)