Question sur l'instanciation existentielle
J'avais du mal à comprendre l'instanciation existentielle. Mon manuel (Rosen - Discrete Mathematics and its Applications) indique ceci à propos de l'instanciation existentielle:
L'instanciation existentielle est la règle qui permet de conclure qu'il existe un élément c dans le domaine pour lequel P (c) est vrai si l'on sait que ∃xP (x) est vrai. Nous ne pouvons pas sélectionner ici une valeur arbitraire de c, mais plutôt ac pour laquelle P (c) est vrai. Habituellement, nous n'avons aucune connaissance de ce qu'est c, seulement qu'il existe. Parce qu'il existe, nous pouvons lui donner un nom (c) et continuer notre argumentation.
Cela a du sens pour moi pour certaines déclarations existentielles.
Par exemple, considérez la déclaration $\exists x\in \mathbb{Z}$ $(x + 1 = 2)$. Il n'y a qu'un seul entier qui rend la fonction propositionnelle ($x + 1 = 2$) vrai (à savoir, $1$). Par conséquent, il me semble logique qu'un nouveau symbole$c$ peut être créé pour nommer "le seul entier qui fait $x + 1 = 2$ vrai".
Cependant, considérez la déclaration $\exists x\in \mathbb{Z}$ $(x * 0 = 0)$. Il existe de nombreux entiers qui font de la fonction propositionnelle ($x * 0 = 0$) vrai (ex. $1$, $2$, $3$).
Dans ce cas, lorsque nous créons un nouveau symbole $c$, est-ce que ce symbole nommant "l'un des entiers qui rend $x * 0 = 0$ vrai "? Je trouve cela légèrement ambigu, alors je me demandais si je comprenais correctement la signification de ce symbole.
Veuillez clarifier et merci pour votre temps.
Réponses
Cependant, considérez la déclaration $\exists x\in \mathbb{Z}$ $(x * 0 = 0)$. Il existe de nombreux entiers qui font de la fonction propositionnelle ($x * 0 = 0$) vrai (ex. $1$, $2$, $3$).
Dans ce cas, lorsque nous créons un nouveau symbole $c$, est-ce que ce symbole nommant "l'un des entiers qui rend $x * 0 = 0$ vrai"?
Oui, c'est exactement ça. Donc ... même si l'utilisation de$c$suggère que nous savons exactement de quel objet nous parlons, ce n'est en fait pas le cas. On sait encore seulement qu'il y a au moins un objet qui satisfait la formule en question. Mais, pour approfondir notre raisonnement, nous devons pouvoir parler de `` l'un de ces objets '' et pour cela, ce système utilise une constante individuelle ... même si vous devez bien sûr vous assurer que cette constante n'était pas déjà utilisé ailleurs dans la preuve pour faire référence à un autre objet.
Veuillez noter qu'il existe d'autres systèmes de preuve formels qui n'utilisent pas $c$ dans ce cas, mais gardez la variable une variable, ce qui a l'avantage de suggérer que vous ne savez en effet pas de quel objet spécifique vous parlez ... mais l'inconvénient est que vous obtenez maintenant des lignes dans la preuve que, une fois prise hors contexte du reste de la preuve, aurait une variable libre ... et c'est en effet un inconvénient suffisant pour que certaines personnes utilisent des constantes à la place.
J'ai parfois pensé que peut-être une façon de traiter tout cela est d'avoir un troisième ensemble de façons de pointer vers des objets autres que des constantes et des variables: des symboles que vous utiliseriez en effet pour cette instanciation très existentielle, et qui dénotent `` un objet avec une propriété, bien que nous ne sachions pas laquelle », c'est-à-dire pas complètement arbitraire (comme une variable normale), mais pas non plus spécifique (comme une constante). Cependant, je n'ai jamais fait quoi que ce soit dans les systèmes formels.