Définition logique à égalité et loi d'identité dans «Introduction à la logique» de Suppes
" Introduction à la logique " de Patrick Suppes fournit des règles pour les définitions formelles dans le chapitre 8. Les règles ci-dessous sont spécifiées pour un nouveau symbole d'opération avec égalité:
Une équivalence $D$ introduction d'un nouveau symbole d'opération à n places $O$ est une définition correcte dans une théorie si et seulement si $D$ est de la forme:
$O(v_1, ..., v_n) = w \leftrightarrow S$
et les restrictions suivantes sont satisfaites:
(i)$v_1, ..., v_n, w$sont des variables distinctes.
(ii)$S$ n'a pas de variables libres autres que $v_1, ..., v_n, w$.
(iii)$S$est une formule dans laquelle les seules constantes non logiques sont des symboles primitifs et des symboles préalablement définis de la théorie.
(iv) La formule$\exists !w[S]$ est dérivable des axiomes et des définitions précédentes de la théorie.
Il y a aussi une mention préalable de la loi de l'identité :
Si x est quoi que ce soit, alors $x=x$.
Supposons maintenant que vous ayez la définition suivante:
$$ \forall f,x,y[f_x = y \iff f \text{ is a function } \land \langle x,y \rangle \in f] $$
Supposons également que vous ayez des fonctions précédemment définies et des paires ordonnées de telle sorte que vous puissiez prouver $\exists !y[S]$ avec extentionnalité, il suit donc la règle (iv).
Voici le problème: dans les limites de cet ensemble de règles, il semble que l'on puisse utiliser la loi de l'identité avec n'importe quelle variable, disons$A$, pour prétendre que $A_x=A_x$ et utilisez cela pour prétendre que $A \text{ is a function } \land \langle x,A_x \rangle \in A$, et ainsi, que $A$est une fonction, même si nous n'en savons rien. Cette logique peut être utilisée avec n'importe quelle variable, que ce soit une relation normale, un ensemble simple ou même un élément urinaire, donc cette déduction doit être erronée.
Au début, je pensais enfreindre la règle (iii), comme la déclaration "$A \text{ is a function } \land \langle x,A_x \rangle \in A$"contient un symbole non défini précédemment, $A_x$, qui est définie dans l'instruction elle-même, donc elle ne serait pas valide.
Cependant, considérez la définition suivante: $$ \newcommand\liff{\leftrightarrow} \newcommand\lif{\rightarrow} \newcommand\lfi{\leftarrow} \newcommand\ordp[2]{\langle #1,#2 \rangle} \newcommand\mset[1]{\{ #1 \}} \newcommand\isRel[1]{#1 \text{ is a relation}} \newcommand\isFunc[1]{#1 \text{ is a function}} \newcommand\isOneOne[1]{#1 \text{ is one-one}} \mset{a} = p \iff \forall x[x \in p \liff x = a] $$
Il est unique par extentionnalité. Il en semble une conséquence claire que$\mset{a} = \mset{b} \lif a = b$, mais la seule façon que je vois pour le prouver est d'utiliser $\mset{a} = \mset{b}$ pour obtenir $\forall x[x \in \mset{b} \liff x = a]$, qui serait rejetée si mon interprétation était correcte, donc je ne pense pas que ce soit la réponse.
Mon deuxième instinct était que la règle (i) est enfreinte, que $f_x = f_x$ne compte pas comme étant des variables distinctes. Cependant, d'après la définition ci-dessus, il semble également que$a \in \mset{a}$devrait suivre. La seule façon que je vois pour le prouver est d'utiliser$\mset{a} = \mset{a}$ avec la définition, qui serait interdite si tel était le cas, donc je ne pense pas que ce soit la solution non plus.
Ma question est donc la suivante: quel est le véritable coupable de l'erreur?
Edit: Après une discussion approfondie, j'ajoute des informations pour clarifier, espérons-le, ce qu'est cette question et ce qu'elle n'est pas.
Il ne s’agit pas de théorie des ensembles . Mon problème concerne le langage formel de la logique du premier ordre fourni par le livre. Pour éviter de se concentrer sur la théorie des ensembles, je vais donner un deuxième exemple. Supposons que nous ayons les déclarations suivantes:
$$ \forall a,b,x,y[\text{isSingleChild}(x) \land \text{parentsOf}(a,b,x) \land \text{parentsOf}(a,b,y) \Rightarrow x = y] \\ \forall a,b,x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentsOf}(a,b,x) \land \text{isSingleChild}(x)] $$
La première déclaration garantit que $x$ est unique dans la définition de $\text{son}$.
La définition de $\text{son}\{a,b\}$semble suivre toutes les règles fournies. Il ne vise pas à indiquer qu'une variable suit un prédicat spécifique, mais simplement à indiquer leur relation logique. Cependant, si vous l'utilisez avec la loi d'identité, vous pouvez en tirer:
$$ \newcommand{\fitch}[1]{\begin{array}{rlr}#1\end{array}} \newcommand{\fcol}[1]{\begin{array}{r}#1\end{array}} %FirstColumn \newcommand{\scol}[1]{\begin{array}{l}#1\end{array}} %SecondColumn \newcommand{\tcol}[1]{\begin{array}{l}#1\end{array}} %ThirdColumn \newcommand{\subcol}[1]{\begin{array}{|l}#1\end{array}} %SubProofColumn \newcommand{\subproof}{\\[-0.25em]} %adjusts line spacing slightly \newcommand{\fendl}{\\[0.037em]} %adjusts line spacing slightly \small \fitch{ \fcol{1:\fendl 2:\fendl 3:\fendl\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl } & \scol { \forall a,b,x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,x) \land \text{isSingleChild}(x)] \\ \forall x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,x) \land \text{isSingleChild}(x)] \\ \text{son}\{a,b\} = \text{son}\{a,b\} \\\quad\iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,\text{son}\{a,b\}) \land \text{isSingleChild}(\text{son}\{a,b\}) \\ \forall x[x = x] \\ \text{son}\{a,b\} = \text{son}\{a,b\} \\ \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,\text{son}\{a,b\}) \land \text{isSingleChild}(\text{son}\{a,b\}) \\ \text{isAdult}(a) \\ \forall a [\text{isAdult}(a)] \\ } & \tcol{ \text{P} \fendl 1\ \forall\text{E}\ \fendl 2\ \forall\text{E}\ \fendl\fendl \text{T}\ \fendl 4\ \forall\text{E}\ \fendl 3,5\ {\liff}\text{E}\ \fendl 6\ {\land}\text{E}\ \fendl 7\ \forall\text{I}\ \fendl }} $$
Donc, à partir de cette définition, vous pouvez en déduire que tout le monde est un adulte. Notez ce que je ne dis pas. Je ne dis pas que cet argument est valable, ni ne le défends, je dis que l'ensemble de règles donné dans le livre le permet (ce n'est probablement pas le cas, mais je ne vois aucune règle de déduction logique enfreinte). Je sais que l'argument est illogique, mais les règles formelles sont suivies . Ma question ne porte pas sur le bien-fondé de l'argument, mais sur le bien-fondé du système fourni dans le livre.
Notez également que l'assertion ne porte pas sur la théorie des ensembles, ni sur la «théorie de la famille», mais sur la logique elle-même . Mon affirmation est que (apparemment) dans le système formel donné, toute déclaration de la forme suivante s'applique:
$$ \forall a,b,x[\text{entityFrom}\{a,b\} = x \iff \text{hasSomeProperty}(a) \land \text{uniqueRelation}(a,b,x)] \vdash \forall a[\text{hasSomeProperty}(a)] $$
Je comprends que la définition n'entraîne pas de conclusion. Néanmoins, au sein du système, la conclusion semble en être déductible.
Il n'y a que trois options. Soit le système formel fourni n'est pas solide, la définition entraîne en fait la conclusion, soit je manque / interprète mal une règle sur la loi de l'identité / les règles de définition / les règles pour les quantificateurs.
Le livre et a plus de 50 ans, tous les oublis possibles dans le système auraient été remarqués à ce stade (il a également été écrit par Suppes, donc je doute qu'il y en ait), donc je suis sûr que ce n'est pas le premier. Les définitions semblent également bien formées et donnent l'impression qu'elles ne devraient pas conduire directement à la conclusion, ce n'est donc probablement pas la deuxième. Menant à la conclusion que je manque probablement ou interprète mal une disposition / règle qui rendrait cet argument non valide. La question est, laquelle?
Ce qui ne répondra pas à la question:
- "Dans la théorie des ensembles, les fonctions ont un domaine spécifique et doivent avoir [certaines propriétés d'ensemble], il n'est donc pas possible que toutes les variables soient des fonctions."
- «Votre définition de la parentalité ne décrit pas correctement l'idée de parents, car elle n'implique pas que tous les enfants ont des parents et [certaines propriétés parentales], de sorte que les définitions ne sont pas des descriptions correctes.»
La solution ne peut pas concerner le manque de fondement de l'argument dans une théorie spécifique, qui ne parviendra pas à la racine du problème. Un contexte spécifique peut être utilisé comme exemple, mais la solution doit se situer au niveau du langage formel.
Qu'est-ce qui pourrait répondre à la question:
- "L'ensemble de règles donné par le livre est en fait incomplet, car une définition avec égalité contenant [une propriété syntatique] peut conduire à une erreur. Cependant, vous pouvez l'éviter en ajoutant une nouvelle règle qui exige que votre définition ait [nouvelle contrainte de définition] "
- "Vos définitions impliquent logiquement la conclusion. Pensez-y, si votre définition est [ceci], alors [expliquez pourquoi la définition devrait logiquement conduire à la conclusion], donc l'argument et la conclusion sont valides. Je doute que ce soit ce que vous vouliez. concluez avec votre définition. Je pense que ce que vous voulez dire, c'est [définition bien comportée]. " $^{\dagger}$
- "Vous avez mal interprété la règle [n], peut-être pensez-vous que cela signifie [interprétation] quand elle dit en fait [interprétation différente]. Si vous en tenez compte, la ligne [x] de votre argument n'est pas valide."
- "Vous oubliez que vous ne pouvez pas remplacer les termes définis comme vous le faites pour les variables. Vous ne pouvez remplacer un terme défini que si [une condition syntatique] s'applique, donc étape $3$ de votre déduction est invalide. "
- "La loi de l'identité n'exige pas seulement l'unicité, mais aussi [une propriété variable], vous ne pouvez donc pas l'utiliser comme en ligne $5$, puisque la variable dans votre définition ne suit pas cette contrainte. "
Il n'est pas nécessaire que votre réponse soit l' une des réponses ci-dessus. Je ne fais que présenter les types de réponses qui, selon moi, seront probablement utiles: des réponses qui se concentrent sur le langage formel.
Merci d'avoir lu jusqu'à la fin, et j'espère que cela clarifiera suffisamment le problème que je veux résoudre.
$\dagger$Comme l'a souligné Mauro ALLEGRANZA, ce cas est particulièrement logique. Comme il l'a dit:
Pensez-y: est - il des axiomes dans votre théorie en disant que non chaque objet est un adulte?
Ce avec quoi je suis d'accord. Cependant, il y a un problème: le jeu de règles ne devrait pas permettre cela .
Plus tôt dans le même chapitre, avant que les règles ne soient établies, leur objectif est énoncé. Les " Critères pour des définitions appropriées ". L'objectif est de séparer un axiome d'une définition. Le premier ( critère d'éliminabilité ) n'est pas important pour cette discussion, mais le second l'est.
Le critère de non-créativité stipule qu'une définition$S$ est non créatif si et seulement si:
Il n'y a pas de formule $T$ dans lequel le nouveau symbole n'apparaît pas de telle sorte que $S \rightarrow T$ est dérivable des axiomes et des définitions précédentes de la théorie mais $T$ n'est pas si dérivable.
L'objectif de l'ensemble de règles est de garantir que nos définitions respectent ces deux critères. Comme indiqué à la page 155: "[...] nous passons à la tâche d'énoncer des règles de définition qui garantiront la satisfaction des deux critères d'éliminabilité et de non-créativité "
Dans mon exemple de parentalité, nous avons le premier énoncé comme axiome et le second comme définition. Cependant, dans cette théorie, la déclaration$\forall a [\text{isAdult}(a)]$ ne contient pas le nouveau symbole et peut être dérivé de la nouvelle définition, mais pas des seuls axiomes, ce qui rendrait la définition créative.
Dans ce cas, ma question devient alors: comment se fait-il que la définition soit créative, alors que l'ensemble de règles est censé garantir la non-créativité?
Réponses
L'ensemble de règles donné par le livre n'est pas incomplet. L'exemple de dérivation que vous donnez résiste également à un examen minutieux. Vous obtenez des conclusions (apparemment) paradoxales parce que la restriction (iv) ne tient réellement dans aucun de vos exemples.
Dans votre premier exemple, la formule $S$ désigne ce qui suit: "$v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2$". La restriction (iv) n'est donc satisfaite que si ce qui suit est un théorème de la théorie considérée:
$$\exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
qui, depuis $v_1,v_2$ sont des variables libres distinctes, tient précisément si
$$\forall v_1. \forall v_2. \exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
est également un théorème de votre théorie. Inutile de dire que cette dernière affirmation n'est en grande partie pas un théorème d'une théorie des ensembles raisonnable. En particulier, cela impliquerait "$\forall v. v \text{ is a function }$" par lui-même.
Dans votre deuxième exemple, la formule $S$ désigne ce qui suit: "$\text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w)$". Comme ci-dessus, la restriction (iv) n'est satisfaite que si ce qui suit est un théorème de la théorie considérée:
$$ \forall v_1. \forall v_2. \exists! w. \text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w) $$
Mais si la phrase donnée ci-dessus est un théorème de votre théorie, alors vous pouvez déjà prouver (directement, en partant de la phrase ci-dessus comme prémisse, et en utilisant $\forall E$, $\wedge E$ et $\forall I$) cette $\forall v_1. \text{isAdult}(v_1)$ est un théorème de votre théorie.