exists
Contexte
Il s'agit d'ajouter les déductions pour introduire le mot clé "exists"
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
Déduction d'ajout
Arguments :
- f une formule
- x une formule
Objet:
La ctruth de condition f +f x et de conclusion $F[exists] +f f.
Domaine:
Aucunne condition.
Déduction d'application
Arguments:
- f une formule
- v un mot qui n'est pas une variable de la mathématique
- c une formule
- p une preuve dans la mathématique augmentée de la variable v
Objet:
La ctruth :
- de conditions :
- les conditions de p
- moins la condition f +f $T[ 'var, v ]
- plus la condition $F[exists] +f f
- de conclusion : c.
Domaine:
- La conclusion de p est c.
- Les conditions de p n'utilisent pas la variable de nom v.
Traduction:
p où l'on remplace v par le x de la déduction d'ajout correspondante.
Validité de la traduction
Comme la preuve générale à traduire n'a pas de condition on a une déduction d'ajout correspondante et donc une formule x telle que f +f x est déjà prouvé. p a toute ses conditions de prouvées sauf f +f $T[ 'var, v ]. Comme v est une variable, la validité de p est inchangée si on remplace v par une formule quelconque de la mathématique. Soit q la preuve résultant du remplacement dans p de v par x. q a toutes ses conditions de démontrées (car f +f x est prouvé) et q prouve c.
Donc on peut remplacer la déduction d'application par q.
Réponse
Voir l'étude.
@extension