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
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
Règle de lecture de la variable locale en place de fonction minimale.
($F u → u x1 ... xn ) a = ($F u → a x1 ... xn ) 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