Qu'est-ce qu'une démonstration ?

$\newcommand{\c}{\rhd}$
Dans ce fil, on donne une définition rapide mais formelle de ce qu'est une preuve mathématique sans fausse philo ou ésotérisme.
La notion de preuve est entièrement syntaxique. Ce qui suit est implémentable informatiquement.

-Soit $P$ un ensemble (j'utilise le vocabulaire ensembliste uniquement pour la clarté et n'utilise aucun résultat de théorie des ensembles dans ce qui suit; dans un langage informatique on recourrait à des types).
On suppose que $P$ est muni d'une loi de composition interne "$\c$".
Soit $A$ une partie de $P$. Une "preuve avec axiomes dans $A$" est une suite finie $f_1,\ldots,f_n$ d'éléments de $A$ telle que pour tout $i\in \{1,\ldots,n\}$, $f_i\in A$, ou il existe $j,k<i$ tels que $f_j=f_k \c f_i$ (cette dernière règle s'appelle "modus ponens").
Soit $g \in P$. Une "preuve de $g$ avec axiomes dans $A$" est simplement une preuve avec axiomes dans $A$ : $g_1,\ldots,g_m$ dont la conclusion (le dernier terme $g_m$) est précisément $g$.
NB: l'ensemble $A$ est totalement arbitraire.

(ceci est une digression): Soit $V$ une partie de $P$ contenant $A$ et telle que pour tous $a,b\in P$, si $a$ et $a \c b$ sont dans $V$, alors $b \in V$ (*). Alors tout élément $f$ de $P$ possédant une preuve avec axiomes dans $A$ appartient à $V$ (cela se voit immédiatement par récurrence sur la longueur de la preuve). Intuitivement $P$ est un ensemble de "phrases", "$a \c b$" veut dire "$a$ entraîne $b$" ou "$a$ implique $b$" et $V$ est "l'ensemble des phrases vraies" whatever that means, (*) et l'affirmation qui le suit disent simplement que si tous les éléments d'un certain ensemble de phrases sont vrais, toutes les phrases prouvables à partir d'axiomes pris exclusivement dans cet ensemble sont vraies.

On désigne par $S$ l'ensemble de tous les éléments de $P$ de la forme $\big(x \c (y \c z)\big) \c \big((x \c y) \c (x \c z)\big)$ où $x,y,z \in P$. On désigne par $K$ celui de tous les éléments de la forme $a \c (b \c a)$ où $a,b\in P$.
Soit $B$ une partie de $P$ contenant $S\cup K$.
(I) pour tout $u\in P$, $u \c u$ possède une preuve avec axiomes dans $B$. (On écrira désormais $C \vdash v$ pour abréger l'expression "$v$ possède une preuve avec axiomes dans $C$").
Bref $B\vdash u \c u$ (en fait $S \cup K \vdash u \rhd u$).
Une preuve est donnée par:
1°) $(u \c \big((u \c u) \c u)\big) \c \big((u \c (u \c u)\big) \c \big(u \c u)\big)$ (un élément de $S$ avec $x:=u, y := u \c u, z:=u$)
2°) $u \c \big((u \c u) \c u\big)$ (un élément de $K$ avec $a:=u, b := u \c u$)
3°) $ \big(u \c (u \c u)\big) \c (u \c u)$ (modus ponens avec 1° et 2°)
4°) $u \c (u \c u)$ (élément de $K$ avec $a:=u,b:=u$)
5°) $u \c u$ (modus ponens avec 3° et 4°)

II) à nouveau considérons une partie $D$ de $P$ telle que $S \cup K$. Soit $h,w\in P$. Si $(D\cup \{h\}) \vdash w$ alors $D \vdash (h \c w)$. Ceci s'appelle le théorème de déduction et correspond à la démarche consistant à dire "supposons machin (en plus des axiomes courants) et démontrons truc, on aura démontré que machin implique truc". Il s'agit froidement d'un programme informatique qui transforme une preuve avec un axiome supplémentaire, en une preuve d'un autre énoncé.
Précisément: soit $p:=w_1,w_2,w_3,\ldots,w_m$ une preuve de $w$ dans $D \cup \{h\}$. On construit alors par induction sur $m$ une preuve dans $D$ dans laquelle figure $h \c w_k$ pour tout $k$, de la façon suivante:
Supposons (récurrence large) qu'on ait une preuve $\ell = \ell_1,\ldots,\ell_p$ avec axiomes dans $D$, dans laquelle figure $h \c w_i$ pour tout $i<k$. Comme $w_1,\ldots,w_k$ est une preuve avec axiomes dans $D \cup \{h\}$, on a l'un des trois cas suivants.
-Si $w_k \in A$, on ajoute à la liste $\ell$ les termes $w_k, w_k \c (h \c w_k), h \c w_k$
-Si $w_k = h$, on ajoute à $\ell$ les termes successifs de la preuve de $h \c h$ décrite au (I) (remplacer $u$ par $h$ ...)
-S'il existe $q,r<k$ tels que $w_q = w_r \c w_k$, on ajoute à $\ell$ les termes:
$\big(h \c (w_r \c w_k)\big) \c \big((h \c w_r) \c (h \c w_k)\big)$, $(h \c w_r) \c (h \c w_k)$, $(h \c w_k)$.
On vérifie que l'on obtient une preuve dans $D$ de $h \c w_k$, ce qui conclut.

########################

Quantificateurs.

Dans ce qui suit $P$ désigne l'ensemble de toutes les formules de la logique du premier ordre (on suppose que le lecteur sait ce qu'est une formule ainsi que la liaison des variables) sur une signature donnée. Les connecteurs utilisés sont $\forall, \Rightarrow$ et le signe constant $\perp$ (qui se lit "faux").

Soit $\mathcal A^*$ l'ensemble de tous les énoncés $\Psi$ de la forme $\forall x_1 \forall x_2 \forall x_3 \cdots \forall x_d \Phi$ où $x_1,\ldots,x_d$ est une liste de lettres (éventuellement vide auquel cas $\Psi$ n'est autre que $\Phi$ lui-même) et $\Phi$ est une formule de l'une des formes suivantes ($A,B,C,F,G,H,L,X,Y$ et $Z$ désignant des formules quelconques) :
i) $\big(X \Rightarrow (Y \Rightarrow Z)\big) \Rightarrow \big((X \Rightarrow Y) \Rightarrow (X \Rightarrow Z)\big)$
ii) $A \Rightarrow (B \Rightarrow A)$
iii) $\big((C \Rightarrow \perp) \Rightarrow \perp\big) \Rightarrow C$
iii) $\big(\forall x (F \Rightarrow G)\big) \Rightarrow \big((\forall x F) \Rightarrow (\forall x G)\big)$
iv) $(\forall y H) \Rightarrow (H[y:=t])$ où $t$ est un terme quelconque du langage
v) $L \Rightarrow (\forall z L)$ où $z$ est une lettre qui ne figure pas dans $L$.

(III) Soit $\mathcal E$ un ensemble d'énoncés contenant $\mathcal A^*$. Soit $u$ une lettre ne figurant (**) dans aucun des énoncés de $\mathcal E$. Soit $M$ une formule. Si $\mathcal E\vdash M$ alors $\mathcal E \vdash \forall u M$. ("règle de généralisation")
A nouveau la preuve se construit par induction sur la longueur $n$ de la preuve $M_1,\ldots,M_n$ de $M$; on suppose donnée une preuve $\ell$ avec axiomes dans $\mathcal E$ contenant $\forall u M_i$ pour tous $i<n$; alors
-Si $M_n$ est un élément de $\mathcal E$, alors $u$ ne figure pas dans $M$ et donc $M \Rightarrow \forall u M$ est dans $\mathcal A^*$ donc dans $\mathcal E$. On ajoute $M \Rightarrow \forall u M$ puis $\forall u M$ à $\ell$.
-S'il existe $k,\ell<n$ tels que $M_{\ell} = M_k \Rightarrow M_n$, on lui ajoute $\big(\forall u (M_k \Rightarrow M_n)\big) \Rightarrow \big((\forall u M_k) \Rightarrow (\forall u M_n)\big), (\forall u M_k) \Rightarrow (\forall u M_n), \forall u M_n$.

L'idée de la règle de généralisation est qu'au fond la nouvelle lettre $u$, comme elle ne figure dans aucun des axiomes de la preuve (tous dans $\mathcal E$), peut désigner un objet quelconque et donc on a une preuve de ce que l'énoncé $M$ ou figure éventuellement $u$, est vrai "pour tout $u$".

-On appelle théorèmes de logique classique du premier ordre les énoncés qui ont une preuve dans $\mathcal A^*$.
-Soit $\mathcal H$ un ensemble quelconque d'énoncés (formules). Alors à l'aide du théorème de déduction (cf II), on montre qu'un énoncé $f$ possède une preuve dans $\mathcal H \cup \mathcal A^*$ si et seulement si il existe $h_1,\ldots,h_p\in \mathcal H$ tels que $h_1 \Rightarrow (h_2 \Rightarrow ( \cdots (h_p \Rightarrow f) ) \ldots )$ est un théorème de logique classique du premier ordre.

[size=x-small](**) comme variable libre voire comme variable tout court si la liaison des variables est réalisée avec des indices de De Bruijn.[/size]