Lazi

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