Calcul Propositionnel

Formules

Les formules de la logique propositionnelle sont construites à partir :

d'un ensemble fini de variables propositionnelles, \(\newcommand{\limplies}[0]{\Rightarrow}\newcommand{\lequiv}[0]{\Leftrightarrow}V\) (en général des lettres minuscules, par exemple \(V=\{a, b, c\}\)) ;
d'un opérateur unaire de négation \(\lnot\) ;
de quatre opérateurs binaires :
1. ou : \(\lor\) ;
2. et : \(\land\) ;
3. implique : \(\limplies\) ;
4. équivalent : \(\lequiv\).

Notations

on utilise souvent deux constantes : \(\top\) dont la valuation est toujours 1 et \(\bot\) dont la valuation est toujours 0 ;
on note \(F \equiv G\) si et seulement si pour toute valuation \(v\), \(v(F)=v(G)\) (les formules \(F\) et \(G\) sont sémantiquement équivalentes).

Aide mémoire

Équivalences notables

Il est souvent utile de simplifier ou de transformer des formules grâce aux équivalences notables suivantes :

\[ \begin{align*} (X \limplies Y)&\equiv ((\lnot X)\lor Y)\\ ((X \land Y)\land Z)&\equiv (X \land (Y\land Z)))\\ (X\land Y)&\equiv (Y\land X)\\ (X \land (Y\lor Z))&\equiv (X \land Y)\lor (X\land Z))\\ (\lnot(\lnot X))&\equiv X\\ (\lnot(X\land Y))&\equiv ((\lnot X)\lor (\lnot Y) \end{align*} \]

\[ \begin{align*} (X\lequiv Y)&\equiv ((X\limplies Y)\land(Y\limplies X))\\ ((X \lor Y)\lor Z)&\equiv (X\lor (Y\lor Z))\\ (X\lor Y)&\equiv (Y\lor X)\\ (X \lor (Y\land Z))&\equiv (X \lor Y)\land (X\lor Z))\\ (\lnot(X\lor Y))&\equiv ((\lnot X)\land (\lnot Y) \end{align*} \]

Règles de Quine

L'algorithme de Quine utilise d'autres équivalences notables qui s'appuient sur les valuations constantes de \(\top\) et \(\bot\) :

\[ \begin{align*} (\lnot \bot)&\equiv \top&(\lnot \top)&\equiv \bot\\ (\top\limplies X)&\equiv X&(X\limplies \top)&\equiv \top\\ (\bot\limplies X)&\equiv \top&(X\limplies \bot)&\equiv (\lnot X)\\ (X\lor \top)&\equiv \top&(X\lor \bot)&\equiv X\\ (\top\lor X)&\equiv \top&(\bot\lor X)&\equiv X\\ (X\land \top)&\equiv X&(X\land \bot)&\equiv \bot\\ (\top\land X)&\equiv X&(\bot\land X)&\equiv \bot\\ (X\lequiv \top)&\equiv X&(X\lequiv \bot)&\equiv (\lnot X)\\ (\top\lequiv X)&\equiv X&(\bot\lequiv X)&\equiv (\lnot X)\\ \end{align*} \]

Règles du calcul des séquents

Le calcul des séquents repose sur les huit règles suivantes, dans lesquelles \(A\) et \(B\) sont des formules du calcul propositionnel, alors que \(\Gamma, \Delta, \Theta\) et \(\Sigma\) désignent des listes éventuellement vides de formules séparées par des virgules) :

\( \begin{array}{c} \Gamma,A,B,\Delta \vdash \Theta\\\hline \Gamma,(A\land B),\Delta \vdash \Theta \end{array}\land_g \)

\( \begin{array}{c} \Theta \vdash \Gamma,A,\Delta\phantom{\Gamma,A,\Delta} \Theta \vdash \Gamma,B,\Delta \\\hline \Theta\vdash\Gamma,(A\land B),\Delta \end{array}\land_d \)

\( \begin{array}{c} \Gamma,A,\Delta \vdash \Theta \phantom{\Gamma,A,\Delta}\Gamma,B,\Delta \vdash\Theta\\\hline \Gamma,(A\lor B),\Delta \vdash \Theta \end{array}\lor_g \)

\( \begin{array}{c} \Theta \vdash \Gamma,A,B,\Delta \\\hline \Theta\vdash\Gamma,(A\lor B),\Delta \end{array}\lor_d \)

\( \begin{array}{c} \Gamma,\Delta \vdash A,\Theta \phantom{\Gamma,A,\Delta} \Gamma,B,\Delta \vdash \Theta\\\hline \Gamma,(A\limplies B),\Delta \vdash \Theta \end{array}\limplies_g \)

\( \begin{array}{c} A,\Gamma \vdash \Delta, B, \Theta\\\hline \Gamma\vdash\Delta,(A\limplies B),\Theta \end{array}\limplies_d \)

\( \begin{array}{c} \Gamma,\Delta\vdash A,\Theta\\\hline \Gamma,(\lnot A),\Delta \vdash \Theta \end{array}\lnot_g \)

\( \begin{array}{c} A,\Gamma \vdash \Delta,\Theta\\\hline \Gamma\vdash\Delta,(\lnot A),\Theta \end{array}\lnot_d \)

On admet comme axiome tout séquent de la forme suivante : \[ \Gamma,A,\Delta \vdash \Theta,A,\Sigma \]