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é :
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.
- 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 :
CQFD
@theorem