Lazi

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 ?

Voir l'étude.

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