forAll
Contexte
Il s'agit d'ajouter les déductions pour introduire le mot clé "forAll"
Voir aussi "Comment définir les extensions nécessaire ?"
Question
Quels sont les déductions nécessaires ? Pour chaque déduction, il faudra décrire:
- ses arguments
- son objet
- le domaine
- sa traduction (pour la déduction d'applicaiton)
- la preuve de la validité de la traduction de la déduction d'application
Étude
Utiliser une variable ?
Déduction d'ajout
Arguments :
- f est une formule
- v un mot qui n'est pas une variable de la mathématique
- p une preuve dans la mathématique où v est une variable ajoutée
Objet:
La ctruth ayant les conditions provenant de celles de p et de conclusion $F[forAll] +f f
Domaine:
- Les conditions de l'objet de p ne doivent pas contenir la variable v.
- La conclusion de p doit être f +f $T['var,v]
Déduction d'application
Arguments:
- f une formule
- x une formule
Objet:
La ctruth de condition $F[forAll] +f f et de conclusion f +f x
Domaine:
Aucunne condition.
Traduction:
p de la déduction d'ajout où l'on remplace v par x.
Validité de la traduction
La preuve générale ne contient pas de condition, donc les conditions de p sont déjà prouvées. La validité de p ne change pas si on remplace v par une formule quelconque de la mathématique. Le résultat de ce remplacement est une preuve de p +f x. On peut donc remplacer la déduction d'application par cette preuve.
Réponse
Voir l'étude.
@extension @todo