Logique propositionnelle

On se donne un ensemble de variables propositionnelles $p,q,r,\dots$ L'ensemble $\mathcal{F}$ des formules est le plus petit ensemble tel que :

$$\frac{}{p\in \mathcal{F}}\frac{\phi \in \mathcal{F}}{\neg \phi \in \mathcal{F}}\frac{\phi ,\psi \in \mathcal{F}}{(\phi \wedge \psi )\in \mathcal{F}}\frac{\phi ,\psi \in \mathcal{F}}{(\phi \vee \psi )\in \mathcal{F}}\frac{\phi ,\psi \in \mathcal{F}}{(\phi \to \psi )\in \mathcal{F}}$$

et de même pour $\leftrightarrow$. Les notations sont celles que le programme fixe : $\neg ,\vee ,\wedge ,\to ,\leftrightarrow$. L'arité d'un connecteur est son nombre d'arguments : $1$ pour $\neg$, $2$ pour les autres.

Les sous-formules de $\phi$ sont $\phi$ elle-même et, récursivement, celles de ses arguments — ce sont exactement les sous-arbres. La taille est le nombre de nœuds, la hauteur celle de l'arbre.

let rec taille = function
  | Var _ -> 1
  | Non f -> 1 + taille f
  | Et (a, b) | Ou (a, b) | Implique (a, b) -> 1 + taille a + taille b

Les quantificateurs $\forall$ et $\exists$ introduisent une notion de portée : dans $\forall x\phi$, la portée de $\forall x$ est $\phi$. Une occurrence de $x$ dans cette portée est liée ; une occurrence hors de toute portée d'un quantificateur sur $x$ est libre.

$$\underset{\text{les deux }x\text{ sont lieˊs}}{\underbrace{\forall x(P(x)\to Q(x,\underset{\text{libre}}{\underbrace{y}}))}}$$