Lazi

Étude changement =c

Contexte

Pour le théorème "Argument égaux par calcul", on a besoin d'une relation proche de =c mais qui exprime une similitude de l'expression globale même en cas d'incalculabilité.

=c est redondant sur la partie fonction car dans une globalité calculable implique que la partie fonction est calculable.

Il serait bon de garder l'énnoncé "vérité => égalité et =c entre les membres".

Question

Pourrait-on unir la relation "=s" avec "=c" de sorte que deux formules égales par calcul soient similaires dans leurs parties calculables même si les formules globales sont incalculables ?

Étude

Incompatibilité

Quand on déduit une égalité x *=* y, x et y peuvent être incalculables et la recherche de la relation entre les deux demanderait une exploration (finie car la preuve de l'égalité est finie).
Quand on calcule, dans la preuve du théorème "Arguments égaux par calcul", a +f b et a +f c, la propriété entre les deux formules doit garder la relation de similarité entre les parties "fonction".
Donc la réponse est non.

Réponse

Non (voir "Incompatibilité").