Quelles règles pour l'extension pour les fonctions

Contexte

L'extension pour définir les fonctions ($F→) doit être compatible avec les setL et subF. Elle doit aussi permetre de remplacer la variable se trouvant en position de fonction minimale par la valeur de l'argument. On ne peut remplacer n'importe que variable car les setL changent la valeur de l'argument.

Question

Quelles sont les règles adéquates pour cette extension ?

Étude

Règles trop laxistes

J'ai pensé aux règles suivantes, mais elles mènent à des absurdités :

1)

Règle : remplacer les variables de x dans ($F u → x y) a si x ne contient pas de setL u.

C'est trop laxiste car x peut contenir une fonction qui fait qu'un setL u peut se trouvé à devoir être appliqué à un u de x.

2)

Règle : Si ($F u → x) a = ($F u → y) b alors ($F u → x z) a = ($F u → y z) b

Faux si on remplace x par "identF" et z par u, car on déduit pour tout a, b que a = b.

3)

Règle :
Si

($F u → x) a = ($F u → y) a

alors

($F u → x z) a = ($F u → y z) a

Par la règle de base pour appliquer un argument à une fonction (voir ci-dessous), on a :
($F u → $F t → t u) 1b = ($F u → $F t → t 1b) 1b
En prenant z = setL u 0b 1b on obtient :
($F u → ($F t → t u)(setL u 0b u)) 1b = ($F u → ($F t → t 1b)(setL u 0b u)) 1b
donc par la règle de base pour appliquer un argument à une fonction (ici la fonction en t) :
($F u → (setL u 0b identF)u) 1b = ($F u → (setL u 0b identF)1b) 1b
donc
($F u → identF 0b) 1b = ($F u → identF 1b) 1b
donc
1b = 0b
absurde

Pas de règle locale pour lire la variable

La règle 3) ci-dessus montre que l'on ne peut pas utiliser une égalité locale. Donc pour lire la valeur d'une variable locale il faut passer par une condition sur la formule entière.

Essai de règles n°1 :

La règle de base pour appliquer un argument à une fonction :
Si

f ne contient pas de setL u libre

alors

($F u → f) a = {f où la variable u libre est remplacée par a}

Règle de lecture de la variable locale en place de fonction minimale.

($F u → u x₁ ... x_n ) a = ($F u → a x₁ ... x_n ) a

Ajouter une règle de conversion de la notation ?

La question est : doit-on ajouter des formules pour convertir les notations de fonction en distribute ?

Si on le fait alors on ajoute des vérités à la mathématique puisque à priori j'envisage d'exprimer les "pour tout" par le fait que la fonction est vrai. On ne pourrait alors plus traduire n'importe quelle preuve puisque la preuve d'une fonction convertie en distribute n'aurait pas d'équivalent.

Est-il possible d'introduire à lazi.0.1 les preuves de fonctions sous-forme de distribute ?

La règle serait que si on prouve f x où x est une variable, alors on déduit f. Pour utiliser cette vérité il faudrait une règle qui stipule que si on a distribute x y, alors on peut déduire distribute x y z pour n'importe quel z.

Est-ce que cette nouvelle règle simplifierait la définition lazi ?

@todo

Réponse

@todo