Lazi

Quels théorèmes sur le nombre d'imply

Contexte

Pour déterminer les conditions de validité de "imply", il est nécessaire de raisonner sur le nombre d'imply des formules sémantiquement égales et déduites par déduction d'ajout. Voir l'essai 3 de l'étude sur imply.

Question

Quels théorèmes à démontrer sur le nombre d'imply des formules déduites ?

Étude

Remarques

Par égalité on peut augmenter arbitrairement le nombre d'occurence d'un mot dans la formule , par exemple 1b = if 1b 1b imply .

Si les sous-formules sont calculables, on a une valeur déterminée du nombre de mots en prenant la formule où toute sous-formule tq son calcul est terminé.

On peut raisonner sur le nombre de "imply" à leurs place "normale", c'est à dire ayant un rôle de connecteur logique :

Pour l'implication globale il y en a un (puisqu'on déduit une implication), donc pour le prémisse aussi. Mais alors le prémisse du prémisse aussi, etc. Donc il y a une infinité d'imply.

Essai 1

La vérité de départ est un imply. Il sert à prouver la prémisse de l'imply. Si on montre que cela implique qu'il y a un imply dans la prémisse et que l'on peut poursuivre le raisonnement par récurrence alors on aboutit à une infinité d'imply.

Il faudrait d'abord définir la propriété "forme d'imply" qui reste vrai pour la prémisse. Sachant que l'on peut utiliser des déductions d'ajout.

Il faudrait définir la notion de "vérité utilisée".

Il faudrait définir un théorème montrant que par lazi.0.0, si une implication est une vérité utilisée alors l'objet de la preuve est une implication, et ce récursivement pour ses arguments.

Il faudrait montrer que par une déduction d'ajout, si une vérité utilisée est une implication, alors on la retrouve dans la formule déduite. Mais dans les sous-preuves, si on a des déductions d'application ? Remarquons que l'on ne peut pas traduire les déductions d'application dans les sous-preuves car il y a un contexte différent (comme par exemple une hypothèse pour l'imply).

Réponse

@todo