1$\text{Proposition}$
$\text{Phrase qui peut être soit vraie soit fausse}$
2$\text{Ensemble des variables propositionnelles } \mathcal V$
$\text{Propositions élémentaires / Propositions atomiques}$
3$\text{Définition inductive de l'ensemble des formules du calcul propositionnel } \mathcal F$
$\text{Cas de base : } \begin{cases} \bot \in \mathcal F \\ \top \in \mathcal F \\ \forall \varphi \in \mathcal V \quad \varphi \in \mathcal F \end{cases}$
$\text{Constructeur : } \begin{cases} \forall \varphi \in \mathcal F \quad \lnot \varphi \in \mathcal F \\ \forall (\varphi, \varphi') \in \mathcal F^2 \quad \forall \square \in \{\land, \lor, \implies, \Longleftrightarrow\} \quad \varphi \square \varphi' \in \mathcal F \end{cases}$
4$\text{Définition inductive de la taille d'une formule } \varphi \in \mathcal F \text{, noté } |\varphi|$
$\begin{cases} \forall \varphi \in \mathcal V \quad |\bot| = |\top| = |\varphi| = 1 \\ \forall \varphi \in \mathcal F \quad |\lnot \varphi| = 1 + |\varphi| \\ \forall (\varphi, \varphi') \in \mathcal F^2 \quad \forall \square \in \{\land, \lor, \implies, \Longleftrightarrow\} \quad |\varphi \square \varphi'| = |\varphi| + |\varphi'| + 1 \end{cases}$
5$\text{Définition inductive de la hauteur d'une formule } \varphi \in \mathcal F \text{, noté } h(\varphi)$
$\begin{cases} \forall \varphi \in \mathcal V \quad h(\bot) = h(\top) = h(\varphi) = 0 \\ \forall \varphi \in \mathcal F \quad h(\lnot \varphi) = 1 + h(\varphi) \\ \forall (\varphi, \varphi') \in \mathcal F^2 \quad \forall \square \in \{\land, \lor, \implies, \Longleftrightarrow\} \quad h(\varphi \square \varphi') = 1 + \max(h(\varphi), h(\varphi')) \end{cases}$
6$\text{Définition inductive de l'ensemble des sous-formules d'une formule } \varphi \in \mathcal F \text{, noté } SF(\varphi)$
$\begin{cases} SF(\bot) = \{\bot\} \\ SF(\top) = \{\top\} \\ \forall \varphi \in \mathcal V \quad SF(\varphi) = \{\varphi\} \\ \forall \varphi \in \mathcal F \quad SF(\lnot \varphi) = \{\lnot \varphi\} \cup SF(\varphi) \\ \forall (\varphi, \varphi') \in \mathcal F^2 \quad \forall \square \in \{\land, \lor, \implies, \Longleftrightarrow\} \quad SF(\varphi \square \varphi') = \{\varphi \square \varphi'\} \cup SF(\varphi) \cup SF(\varphi') \end{cases}$
7$\text{Valuation}$
$\text{Application, généralement noté } \sigma \text{, de } \mathcal V \text{ sur } \{0, 1\}$
8$\text{Définition inductive de } \begin{cases} \text{l'évaluation} \\ \text{la valeur de vérité} \end{cases} \text{d'une formule } F \in \mathcal F \text{ sous une valuation } \sigma, \text{ noté } \llbracket F \rrbracket_\sigma$
$\begin{cases} \llbracket \bot \rrbracket_\sigma = 0 \\ \llbracket \top \rrbracket_\sigma = 1 \\ \forall \varphi \in \mathcal V \quad \llbracket \varphi \rrbracket_\sigma = \sigma(\varphi) \\ \forall \varphi \in \mathcal F \quad \llbracket \lnot \varphi \rrbracket_\sigma = 1 - \llbracket \varphi \rrbracket_\sigma \\ \forall (\varphi, \varphi') \in \mathcal F^2 \quad \llbracket \varphi \land \varphi' \rrbracket_\sigma = \llbracket \varphi \rrbracket_\sigma \llbracket \varphi' \rrbracket_\sigma \\ \forall (\varphi, \varphi') \in \mathcal F^2 \quad \llbracket \varphi \lor \varphi' \rrbracket_\sigma = 1 - (1 - \llbracket \varphi \rrbracket_\sigma)(1 - \llbracket \varphi' \rrbracket_\sigma) \\ \forall (\varphi, \varphi') \in \mathcal F^2 \quad \llbracket \varphi \implies \varphi' \rrbracket_\sigma = 1 - \llbracket \varphi \rrbracket_\sigma (1 - \llbracket \varphi' \rrbracket_\sigma) \\ \forall (\varphi, \varphi') \in \mathcal F^2 \quad \llbracket \varphi \Longleftrightarrow \varphi' \rrbracket_\sigma = 1 - \llbracket \varphi \rrbracket_\sigma (1 - \llbracket \varphi' \rrbracket_\sigma) - \llbracket \varphi' \rrbracket_\sigma (1 - \llbracket \varphi \rrbracket_\sigma) \end{cases}$
9$\text{Égalité syntaxique entre deux formules}$
$\text{Pour toutes formules } (F, G) \in \mathcal F^2$
$F = G \text{ si et seulement si } F \text{ et } G \text{ ont la même } \begin{cases} \text{écriture} \\ \text{représentation arborescente} \end{cases}$
10$\text{Modèle de } F \in \mathcal F$
$\text{Valuation } \sigma: \mathcal V \rightarrow \{0, 1\} \text{ tel que } \llbracket F \rrbracket_\sigma = 1$
11$\text{Satisfiabilité de } F \in \mathcal F$
$F \text{ admet un modèle}$
12$F \in \mathcal F \text{ est une tautologie}$
$\forall \sigma: \mathcal V \rightarrow \{0, 1\} \quad \llbracket F \rrbracket_\sigma = 1$
13$F \in \mathcal F \text{ est une antilogie}$
$\forall \sigma: \mathcal V \rightarrow \{0, 1\} \quad \llbracket F \rrbracket_\sigma = 0$
14$\text{Équivalence logique entre deux formules}$
$\text{Pour toutes formules } (F, G) \in \mathcal F^2$
$F \equiv G \Longleftrightarrow \forall \sigma: \mathcal V \rightarrow \{0, 1\} \quad \llbracket F \rrbracket_\sigma = \llbracket G \rrbracket_\sigma$
15$\text{Conséquence logique d'une formule}$
$\text{Pour toutes formules } (F, G) \in \mathcal F^2$
$F \vDash G \text{ si et seulement si pour toute valuation } \sigma: \mathcal V \rightarrow \{0, 1\} \text{ si } \llbracket F \rrbracket_\sigma = 1 \text{ alors } \llbracket G \rrbracket_\sigma = 1$
16$\text{Conséquence logique d'un ensemble de formule}$
$\text{Pour tous } \Gamma = (F_1, ..., F_n) \in \mathcal F^n \text{ et } G \in \mathcal F$
$\Gamma \vDash G \text{ si et seulement si pour toute valuation } \sigma: \mathcal V \rightarrow \{0, 1\} \text{ si } \forall i \in \llbracket 1, n \rrbracket \quad \llbracket F_i \rrbracket_\sigma = 1 \text{ alors } \llbracket G \rrbracket_\sigma = 1$
17$\text{Notation des tautologies avec la conséquence logique}$
$\forall F \in \mathcal F \quad F \text{ est une tautologie si et seulement si } \vDash F$
18$\text{Caractérisation des conséquences logiques}$
$\forall (F, G) \in \mathcal F^2 \quad F \vdash G \text{ si et seulement si } \vDash F \implies G$
19$\text{Équivalences logiques usuelles}$
$\begin{cases}
A \land B \equiv B \land A \quad ; \quad A \lor B \equiv B \lor A \quad \textit{(Commutativité)} \\
A \land (B \lor C) \equiv (A \land B) \lor (A \land C) \quad \textit{(Distributivité de "et" sur "ou")} \\
A \lor (B \land C) \equiv (A \lor B) \land (A \lor C) \quad \textit{(Distributivité de "ou" sur "et")} \\
A \land (B \land C) \equiv (A \land B) \land C \quad ; \quad A \lor (B \lor C) \equiv (A \lor B) \lor C \quad \textit{(Associativité)} \\
A \lor A \equiv A \quad ; \quad A \land A \equiv A \quad \textit{(Idempotence)} \\
A \land \top \equiv A \quad ; \quad A \lor \top \equiv \top \quad \textit{(Neutre / Absorbant avec "top")} \\
A \land \bot \equiv \bot \quad ; \quad A \lor \bot \equiv A \quad \textit{(Neutre / Absorbant avec "bottom")} \\
A \land \lnot A \equiv \bot \quad ; \quad A \lor \lnot A \equiv \top \quad \textit{(Tiers Exclu / Contradiction)} \\
\lnot\lnot A \equiv A \quad \textit{(Double Négation)} \\
\lnot(A \lor B) \equiv \lnot A \land \lnot B \quad ; \quad \lnot(A \land B) \equiv \lnot A \lor \lnot B \quad \textit{(Loi de De Morgan)} \\
A \Rightarrow B \equiv B \lor \lnot A \quad \textit{(Implication)} \\
A \Leftrightarrow B \equiv (A \Rightarrow B) \land (B \Rightarrow A) \quad \textit{(Équivalence)}
\end{cases}$
20$\text{Équivalence et substitution}$
$\text{On peut remplacer avec des équivalences dans des sous-formules}$