Théorème de l'ordonnancement des calculs

Contexte

Pour faire des raisonnements par récurrence sur les calculs des formules (comme le théorème des calculs et de l'égalité structurel) il nous faut trouver un ordre sur les formules de manière à pouvoir indexer les formules sur ℕ par un index vérifiant des propriétés adéquates pour la récurrence.

Énoncé

Il existe une relation d'ordre stricte et totale R sur les formules calculables de sorte que :

si le calcul de x passe par y alors R x y
si R x y et si z est la fonction de x ou y alors R x z

Preuve

Nous allons définir la relation R1 sur les formules calculables par R1 x y ssi on a la disjonction:

le calcul de x passe par y
si R1 x y et si z est la fonction de x ou y

Remarque : on peut fournir une définition non récurrente (mais plus longue), en utilisant la notion de "fonctions d'une formule".

Remarque : pour une formule a +f b, soit le calcul de a est terminé, soit le calcul de a +f b passe par b. On le prouve en supposant a →c1 a1 et en voyant alors que d'après les règles du 1-calcul que l'on a a +f b →c1 a1 +f b.
De la remarque précédante on déduit que si R1 x y et si z est la fonction de x ou y alors soit z est un calcul terminé soit le calcul de x passe par z.

Nous allons déjà prouver que R1 est une relation d'ordre stricte :

Antireflexivité :

Raisonnons par l'absurde et supposons R1 x x. x est alors incalculable (car dans tous les cas le calcul de x passe par x et donc le calcul boucle), ce qui est absurde car x est calculable. Donc pour tout x calculable ¬ R x x, donc R1 est antiréflexive.

Transitivité :

Supposons R1 x y et R1 y z.
Si le calcul de y est terminé, alors z est une sous-fonction de y, et par définition de R1, R1 x z (règle 2).
Si le calcul de y n'est pas terminé, alors le calcul de x passe par y.

- Si le calcul de y passe par z, d'après la définition du "calcul passant par", tous les cas dans la définition implique que si le calcul de y passe par z alors le calcul de x passe par z.
- Sinon z est une sous-fonction de y, et d'après la règle 2 de la définition de R1, on a R x z.

D'après le théorème de Szpilrajn, comme R1 est une relation d'ordre stricte, il existe une relation R qui étend R1 et qui est une relation d'ordre stricte totale.

Il nous reste à montrer que les éléments minimaux sont des mots :

Soit x un élément minimal. Supposons que x soit une application x1 +f x2 alors R x x1 ce qui contredit la minimalité de x. Donc l'hypothèse que x est une application est absurde. Donc x est un mot.

CQFD

@theorem