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