Quelle est la définition d'une définition?
Dans la logique mathématique ou d'autres systèmes formels, quelle est la définition d'une définition, formellement?
Si "A" est défini comme "B", à quoi ressemble la définition de "A"? Implique-t-il à la fois «A» et «B» (par exemple «A: = B»), ou simplement «B»?
Par exemple, à la p126 du §3. Extensions par définitions dans les interprétations syntaxiques VIII et les formes normales dans la logique mathématique d' Ebbinghaus , supposons que$S$ est un jeu de symboles (non logique),
3.1 Définition. Laisser$\Phi$ être un ensemble de $S$-Phrases.
(a) Supposons $P \notin S$ est un $n$-ary relation symbole et $\phi_P(v_0, ... , v_{n-1})$ un $S$-formule. Alors on dit que$$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$ est un $S$-Définition de $P$ dans $\Phi$.
Que dois-je appeler comme un $S$-Définition de $P$ dans $\Phi$:
$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $?
Est-ce circulaire de définir $P$ en termes de lui-même?
Est un $𝑆$-Définition de $𝑃$ dans $Φ$ une interprétation du symbole $P$ comme un $S'$-phrase? (dans le cadre d'une interprétation syntaxique de$S'$ dans $S'$ lui-même?)
Est-ce que l'apparence de $P$ dans sa propre définition $∀ 𝑣_0,....∀ 𝑣_{𝑛−1}(𝑃𝑣_0...v_{𝑛−1}↔𝜙_𝑃(𝑣_0,...,𝑣_{𝑛−1}))$, dans le même sens que l'apparition de $A$ dans $𝐴:=𝐵$?
$\phi_P(v_0, ... , v_{n-1})) $? (Je suppose que$P$ est défini comme $\phi_P(v_0, ... , v_{n-1})) $ dans $\Phi$.)
$\phi_P$? (Comparez cela à la seconde:$P$ lui-même n'implique pas de variables)
Voir Comment cette définition définit-elle un symbole$P$ en dehors du jeu de symboles $S$ comme un $S$-phrase?
Merci.
Réponses
Nous avons une signature $S$ et nous l'étendons à $S':=S\cup\{P\}$.
le $S$-Définition de $P$ est le $S'$-formule $$\forall v_0\dots v_{n-1}: Pv_0\dots v_{n-1}\leftrightarrow \phi_P(v_0,\dots,v_{n-1})$$qui peut être formellement traité comme un axiome supplémentaire à la donnée$S$-la théorie avec laquelle nous travaillons, produisant ainsi un équivalent $S'$-théorie, dans laquelle le symbole $P$peut être utilisé comme abréviation pour la formule$\phi_P$.
Par exemple, la formule ci-dessous est la définition de la relation de commande habituelle $\le$ d'entiers non négatifs dans la langue $(0,+)$: $$\forall x,y:\ x\le y\,\leftrightarrow\,\exists z: x+z=y$$
Ci-dessous, je vais d'abord essayer de décrire le processus de manière plus intuitive, puis répondre à vos inquiétudes concernant la circularité. Je soupçonne que ce dernier point peut en fait être plus utile, alors n'hésitez pas à lire d'abord la deuxième section - et en particulier, la devise mise en évidence ici sera, je pense, très utile.
(Re: votre dernier commentaire, la définition est $(1)$- la chose qui vous dit comment le nouveau symbole se comporte, en termes des anciens symboles que vous avez déjà et que vous comprenez.)
L'expression clé ici est « expansion par définitions ».
Intuitivement, nous avons à l'esprit le processus suivant:
En commençant par une signature $S$ et certains ensemble $\Phi$ de $S$-sentences, on devient un peu agacé par les inefficacités : il y a des choses dont on peut parler en utilisant$S$-formules mais uniquement de manière détournée. Pensez par exemple au langage de la théorie des ensembles,$\{\in\}$: nous pouvons exprimer des choses comme "$x$ est le produit cartésien de $y$ et $z$"dans ce langage, mais uniquement via des formules extrêmement longues. (C'est un bon exercice pour gérer l'exemple précédent - en utilisant, par exemple, des paires de Kuratowski.)
Donc, étant donné notre formule vraiment compliquée $\varphi(x_0,...,x_{n-1})$, nous voulons élaborer une nouvelle théorie qui est fondamentalement la même que $\Phi$ sauf qu'il a en plus une "abréviation" pour $\varphi$.
Premièrement, cela signifie que nous voulons élargir notre langage: plutôt que de travailler avec $S$ nous voulons travailler avec $S\cup\{R\}$ pour certains $n$symbole de relation -ary $R\not\in S$ que nous entendons servir d'abréviation pour $\varphi$.
Maintenant, nous devons définir une théorie dans ce langage plus large. Cette théorie devrait subsumer ce que nous avons déjà (c'est-à-dire$\Phi$), devrait dicter correctement le comportement de $R$ (c'est-à-dire que c'est une abréviation pour $\varphi$) et ne devrait rien faire d'autre. Cela nous amène à considérer la nouvelle théorie$$\Phi':=\Phi\cup\{\forall x_0,...,x_{n-1}(R(x_0,...,x_{n-1})\leftrightarrow \varphi(x_0,...,x_{n-1})\}.$$
Le passage de $S,\Phi$, et $\varphi$ à $S\cup\{R\}$ et $\Phi'$est une extension par définitions . Nous avons ici une redondance sérieuse : dans un sens précis,$\Phi'$ n'est vraiment pas mieux que $\Phi$. (Officiellement,$\Phi'$est une extension conservatrice de$\Phi$ au sens le plus fort possible: chaque modèle de $\Phi$ a exactement une extension à un modèle de $\Phi'$.) Ce n'est pas surprenant. Nous savions déjà que nous pouvions exprimer ce qui nous tenait à cœur via$\varphi$, nous voulions simplement pouvoir le faire plus rapidement.
Soit dit en passant, notez que cela suggère une version naturelle "efficace au maximum" de toute théorie: ajoutez simplement de nouveaux symboles pour chaque formule! Cela s'appelle la morleyisation , et est parfois utile (bien que généralement un peu idiot ).
OK, qu'en est-il de la circularité qui vous inquiète?
Tout d'abord, notez que "$R$"elle-même n'est qu'un symbole. La nouvelle phrase que nous ajoutons n'est pas vraiment une définition de $R$, mais plutôt une définition de la signification de $R$, ou si vous préférez une règle régissant le comportement des$R$.
Plus sérieusement, la circularité n'est jamais un problème en FOL! L'idée clé est la suivante, ce qui, je pense, constitue une rupture importante par rapport aux intuitions que l'on pourrait apporter de la programmation:
Un ensemble de phrases du premier ordre ne crée pas de choses, il décrit des choses.
Plus précisément, un ensemble de phrases de premier ordre $\Phi$découpe une classe particulière de structures, celles dont il s'agit d'une description précise. Par exemple, les ensembles d'apparence potentiellement dangereux$$\{\forall x(P(x)\leftrightarrow P(x))\}$$ et $$\{\forall x(Q(x)\leftrightarrow \neg Q(x))\}$$sont parfaitement sans cercle; ils sont juste vides (= prise de toute structure) et contradictoires (= prise de pas de structure) respectivement.