La place du langage dans la preuve

Congru
Modifié (18 Feb) dans Fondements et Logique
Soient $L$ et $K$ deux langages du premier ordre tels que $L\subseteq K$.
Soit $T$ une $L$-théorie.
Soient $F\in \mathcal FL$ et $G\in \mathcal F K$.
Que signifie $T\vdash F$ et que signifie $T\vdash G$ ?
Pourquoi n'écrit-on pas plutôt $T\vdash _{_L} F$ et $T\vdash _{_K} G$ et $T\vdash _{_K} F$ ?
Attention : la question porte plus sur la notation qu'autre chose. C'est bizare de ne pas mentionner le langage dans $T\vdash  F$.
Family, mathematics, friends

Réponses

  • A la base la théorie $T$ est écrite dans un langage et un seul, donc inutile de le faire figurer dans les notations. Maintenant, tu peux t'amuser à rajouter autant de symboles que tu veux au langage. Tu obtiens ainsi une théorie $T'$ qui a les mêmes axiomes que $T$ mais pour laquelle tu peux utiliser les nouveaux symboles pour les démonstrations. Toute la question est de savoir si tu y démontres la même chose. Si c'est le cas on dit que $T'$ est une extension conservative de $T$.
    C'est par exemple ce qui se passe avec ZFC : le langage de base est $L=\{\in\}$. Tu peux travailler dans un langage élargi $K$ dans lequel tu fais figurer des symboles variés : $\emptyset, \bigcup, \cup, \subseteq, \{ , \}, ( , ), \mathscr P$ etc. Et il est facile de prouver que l'extension est conservative au sens où tout théorème prouvable dans $K$ l'est aussi (théoriquement) dans $L$. Et c'est heureux car sinon il te faudrait des milliards d'années pour écrire $1+1=2$.
  • Foys
    Modifié (18 Feb)
    Comme a dit Martial, on ne travaille jamais avec deux langages différents en pratique donc on ne mentionne pas $K$ et $L$.
    Les résultats de conservation sous-jacents sont d'ailleurs très frustrants car ils ont des preuves sémantiques (via mettons le théorème de complétude) triviales et des preuves syntaxiques très difficiles à trouver.
    Il est sémantiquement évident que si $K$ est un sous-langage de $L$ et si $\varphi$ est un énoncé de $K$ alors $(\dagger)$ $\underset {L} \vdash \varphi$ si et seulement si $\underset {K} \vdash \varphi$ (si vous utilisez le calcul des prédicats classique sans contexte; pour le calcul des prédicats classique avec contexte -qui est moins connu ni usité certes- ce n'et vrai qu'à condition que $K$ contienne au moins un symbole de constante: un contre exemple serait donné sinon par $K:= \{P\}$, $L:= \{P,c\}$ où $P$ est un symbole de relation à un argument, $c$ est une constante et $\varphi := (\forall x P(x)) \Rightarrow (\exists x P(x))$: en fait le formalisme sans contexte usuel n'est destiné qu'à décrire des modèles non vides quand celui avec contexte permet des modèles vides comme non vides).
    C'était une digression mais en tout cas démontrer $(\dagger)$ purement syntaxiquement, sans théorie des modèles, est un défi (essayez!!).
    Un autre exemple spectaculaire est la déskolémisation, qui est l'énoncé suivant (on se place désormais dans le cas sans contexte, qui est celui habituel de tout le monde): 
    $(\dagger \dagger)$Soit $L$ un langage du premier ordre. Soit $f$ un symbole de fonction d'arité $d\in \N$ n'appartenant pas à $L$. Soit $P(x_1,x_2,\dots,x_d,y)$ un énoncé de $L$ à variables libres dans $x_1,...,x_d,y$. Soit $Q$ un énoncé de $L$.
    Si $\underset{L \cup \{f\}}{\vdash} \left [\forall x_1\forall x_2 ... \forall x_d, P\left (x_1,...,x_d, f(x_1,...,x_d)) \right) \right ] \Rightarrow Q$ alors $\underset{L}{\vdash} \left [\forall x_1\forall x_2 ... \forall x_d \exists y, P\left (x_1,...,x_d, y) \right) \right ] \Rightarrow Q$
    À nouveau il est possible de démontrer $(\dagger \dagger)$ en une ligne avec le théorème de complétude, ou d'autres sémantiques (celles à valeurs booléennes. D'ailleurs on pourra consulter le fantastique article de Thierry Coquand: https://www.researchgate.net/profile/Thierry-Coquand/publication/2787064_Two_Applications_of_Boolean_Models/links/56b08e4f08ae9f0ff7b53e72/Two-Applications-of-Boolean-Models.pdf
    En deux pages cet article démontre la déskolémisation et le théorème de Herbrand avec un argument intuitionniste/constructif car les sémantiques algébriques envisagées permettent vraiment de faire ça).
    Quant à une preuve syntaxique de $(\dagger \dagger)$, le seul exemple de "preuve" que j'ai en tête est celle présente dans le livre de Schoenfield de logique (où l'auteur montre la procédure sur un exemple et le résultat est une usine à gaz peu digeste).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Merci pour vos interventions @Martial et @Foys .
    Family, mathematics, friends
  • Congru
    Modifié (19 Feb)
    @Foys, la formule suivante donne la classe des fonctions: 
    $((\forall z (z\in f \to  z=[couple]\pi _{_1}z\pi _{_2}z))\wedge \forall x\forall y ((x\in f\wedge y\in f\wedge \pi _{_1}x=\pi _{_1}y)\to x=y);f)$
    Family, mathematics, friends
  • Congru
    Modifié (19 Feb)
    La définition de formule avec la quelle je travaille fait que si tu as deux langages $L$ et $K$ tels que $L\subseteq K$, on a $\mathcal F L\subseteq \mathcal F K$.
    Donc, tu ne peux pas, en regardant une formule, deviner le langage avec lequel on travaille.
    Peut-être que tu travailles avec une autre construction des formules, c'était mon cas aussi avant mais c'est très accomodant d'avoir des propriétés comme $\mathcal F L\subseteq \mathcal F K$ donc j'ai pris cette construction.
    Family, mathematics, friends
  • Congru
    Modifié (19 Feb)
    [Inutile de recopier un message présent sur le forum. Un lien suffit. AD]
    Si tu n'ajoutes pas de formules à $T$ (pour obtenir $T'$) alors je suppose que tu rajoutes des axiomes au système de déduction. C'est le cas pour $ZFC$.
    Qu'entends-tu par "démontrer la même chose". Veux-tu dire : $\bigcap \{Cons(T');\mathcal F L_0\} =Cons(T)$
    En supposant que le langage de base utilisé pour  $T$ et qui sera élargi pour $T'$ est noté $L_0$.
    Family, mathematics, friends
  • Congru
    Modifié (19 Feb)
    Comme a dit Martial, on ne travaille jamais avec deux langages différents en pratique donc on ne mentionne pas $K$ et $L$.
    Les résultats de conservation sous-jacents sont d'ailleurs très frustrants car ils ont des preuves sémantiques (via mettons le théorème de complétude) triviales et des preuves syntaxiques très difficiles à trouver.
    Il est sémantiquement évident que si $K$ est un sous-langage de $L$ et si $\varphi$ est un énoncé de $K$ alors $(\dagger)$ $\underset {L} \vdash \varphi$ si et seulement si $\underset {K} \vdash \varphi$ (si vous utilisez le calcul des prédicats classique sans contexte; pour le calcul des prédicats classique avec contexte -qui est moins connu ni usité certes- ce n'et vrai qu'à condition que $K$ contienne au moins un symbole de constante: un contre exemple serait donné sinon par $K:= \{P\}$, $L:= \{P,c\}$ où $P$ est un symbole de relation à un argument, $c$ est une constante et $\varphi := (\forall x P(x)) \Rightarrow (\exists x P(x))$: en fait le formalisme sans contexte usuel n'est destiné qu'à décrire des modèles non vides quand celui avec contexte permet des modèles vides comme non vides).
    C'était une digression mais en tout cas démontrer $(\dagger)$ purement syntaxiquement, sans théorie des modèles, est un défi (essayez!!).
    C'est précisément ce que je suis en train de faire. Je fais une preuve alternative du théorème de complétude et je passe par cela.
    Family, mathematics, friends
  • @Congru : j'utilise la même construction des formules que tout le monde : plus petite classe qui contient les formules atomiques et qui est close par les connecteurs binaires et les quantifications au premier ordre. Donc oui, $FL \subseteq FK$.
    Maintenant, si tu regardes une formule tu es quand même capable de dire si oui ou non elle elle est dans $FL$ ou pas, non ?
    Mais ce qui m'intéresse ce sont les démonstrations. Ce que je dis c'est qu'avec ZFC, en notant $L_0$ le langage de base et $L$ n'importe quel langage étendu, si $\varphi$ est une formule de $L_0$ et s'il en existe une démonstration utilisant les symboles de $L$, alors il en existe aussi une n'utilisant que les symboles de $L_0$. Pour l'essentiel cela revient à dire qu'on peut éliminer tout symbole de fonction $f \in L \setminus L_0$ dans une démonstration. (Idem avec symboles de constante et de relation). Et c'est précisément ce qu'a expliqué @Foys plus haut.
  • Médiat_Suprème
    Modifié (19 Feb)
    Bonjour Martial,

    Je mettrai un minuscule bémol (ou plutôt un ajout) : soit un langage $L$ dans lequel on définit une théorie $T$, on peut ajouter à $L$ un symbole définissable (donc la théorie n'est pas modifiée), il est possible d'utiliser des propriétés du nouveau langage pour démontrer des choses sur la théorie (par exemple si elle admet l'élimination des quantificateurs dans le langage enrichi).
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Foys
    Modifié (19 Feb)
    On peut tenter une preuve syntaxique du résultat souhaité (je pense) par @congru. Ce qui suit est valable aussi bien en logique classique qu'en logique intuitionniste.
    Soient $K\subseteq L$ deux langages du premier ordre avec $K\subseteq L$; soit $F$ un énoncé de $K$ tel que $\underset{L} {\vdash} F$. Alors $\underset{K} {\vdash} F$
    Preuve:
    -On suppose dans un premier temps que $L$ ne rajoute aucun symbole de constante à $K$ ou bien que $K$ contient au moins un symbole de constante et le cas échéant on note $\kappa \in K$ ce symbole.
    On considère alors la traduction suivante pour les termes puis les formules de $L$: 
    Termes:
    $\theta^T(x):= x$ si $x$ est une variable
    $\theta^T(c):= c$ si $c$ est un symbole de constante de $K$
    $\theta^T(c):= \kappa$ si $c$ est un symbole de constante de $L \backslash K$
    $\theta^T(f(t_1,...,t_n)):= f \left ( \theta^T (t_1), ... \theta^T (t_n)\right )$ si $f$ est un symbole de fonction appartenant à $K$.
    $\theta^T(f(t_1,...,t_n)):=  \theta^T (t_1)$ si $f$ est un symbole de fonction appartenant à $L \backslash K$.
    Formules:
    $\theta^F(R(t_1,...,t_n)):= R\left ( \theta^T (t_1), ... \theta^T (t_n)\right)$ si $R$ est un symbole de relation appartenant à $K$.
    $\theta^F(R(t_1,...,t_n)):= \top$ si $R$ est un symbole de relation apartenant à $L \backslash K$.
    $\theta^F(\top):= \top$, $\theta^F(\bot):= \bot$.
    Pour toutes formules $A,B$, $\theta^F(\neg A):= \neg \theta^F(A)$ et $\theta^F(A * B ):= \theta^F(A) * \theta^F(B )$ (où $* \in \{\wedge, \vee, \Rightarrow \}$);
    Pour tout quantificateur $Q \in \{\forall, \exists\}$, toute formule $C$ et toute lettre $x$, $\theta^F(QxC):= Qx\theta^F(C)$.
    ***********
    L'idée intuitive de cette traduction est bien sûr que chaque nouvelle constante du langage s'interprète par $\kappa$, chaque nouveau symbole de fonction s'interprète par une projection sur la première coordonnée et chaque nouveau symbole de relation s'interprète par le prédicat constant égal à vrai (on peut faire librement de tels choix puisque les preuves envisagées sont sans hypothèses et donc les symboles du langage ont un sens arbitraire).
    Par récrrence sur la longueur de la preuve on a alors que pour tout énoncé, $P$ de $L$, si $\underset{L} {\vdash} P$ alors $\underset{K} {\vdash} \theta^F(P)$.
    Lorsque $P$ est dans $K$, on a automatiquement $\theta^F(P) = P$ et le résultat voulu tombe.
    ##################################################################
    Cas où $K$ ne contient aucun symbole de constante et où $L$ en rajoute au moins un:
    -si on travaille avec des systèmes de preuves avec contexte alors le résultat est faux (possibilité de modèles vides): on a $\underset{L} {\vdash} \exists x \top$ mais pas $\underset{K} {\vdash} \exists x \top$
    -si on travaille avec des systèmes sans contexte (où les modèles envisagés ne sont jamais vides et où mettons $\forall x P \Rightarrow \exists x P$ est prouvable pour tout $P$): dans ce cas soit $\pi$ une preuve formelle de $\underset{L} {\vdash} P$ et $k$ une lettre qui ne figure nulle part dans $\pi$. On reprend la traduction précédente avec $k$ au lieu de $\kappa$ et le même argument marche.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • @Médiat : Oui tu as raison, j'aurais dû préciser que si on veut que l'extension soit conservative il faut (et d'ailleurs il suffit) que les nouveaux symboles soient définissables dans la théorie $T$.
  • Congru
    Modifié (20 Feb)
    @Martial je crois qu'il y a une confusion. Je crois que @Médiat_Suprème parle de définissable au sens de la théorie des modèles. Je ne sais pas vraiment ce que définissable par la théorie signifierait. Mais bon, quand tu travailles avec un modèle, tu peux enrichir son langage en rajoutant un symbole de fonction pour chaque fonction définissable et un symbole de relation pour chaque relation définissable, et tu interprètes ces derniers comme il se doit. Mais là on ne travaille que en théorie des modèles sans se soucier de la théorie de la démonstration.
    Si tu veux travailler avec la théorie de la démonstration, alors quand tu ajoutes un symbole qui est sensé signifier quelque chose de particulier comme $\bigcup$, il faut alors ou bien rajouter un axiome qui définit le symbole au système de déduction ou rajouter un énoncé qui définit le symbole à la théorie de base.
    Pour $\bigcup$ ce sera $\forall a\forall z(z\in \bigcup a\iff \exists b(b\in a \wedge z\in b))$.
    Family, mathematics, friends
  • Foys
    Modifié (2 Apr)
    Ci dessous on explique brièvement pourquoi dès qu'une théorie sur le langage $\{\in\}$ satisfait (possède parmi ses axiomes ou démontre) l'axiome d'extensionnalité alors la notation de classe ensembliste $\{x \mid F\}$ y est utilisable de manière intuitive. Cette notation désigne une classe propre a priori, mais aussi un ensemble (nécessairement unique) si $EXT \Rightarrow \exists y, \forall x, x \in y \Leftrightarrow F$ est prouvable dans le système considéré.
    En effet, pour ajouter des définitions et des termes à ZF/ZFC le plus simple est encore de poser (comme dans "Topoi" de R.Goldblatt ou encore "introduction to axiomatic set theory" de G.Takeuti et W.M. Zaring) $"y \in \{x \mid P\}":= P[x:= y]$, $A = B:= "\forall z (z \in A) \Leftrightarrow (z \in B )"$ et enfin $\{y \mid Q\}\in A:= \exists t \left ( t = \{y \mid Q\} \wedge t \in A\right )$ avec $A,B$ qui désignent des lettres ou des termes de la forme $\{w \mid R\}$, $z$ une lettre ne figurant ni dans $A$, ni dans $B$ et enfin $t$ une lettre ne figurant ni dans $\{y \mid Q\}$ ni dans $A$.
    Soit $EXT$ l'énoncé $\forall x \forall y \left [ \left ( \forall z (z \in x \Leftrightarrow z \in y)\right) \Rightarrow \forall t (x \in t \Leftrightarrow y \in t) \right ]$ ("axiome d'extensionalité")
    Il est alors possible de montrer par induction mutuelle sur la taille des termes $T$ et des formules $F$, que les énoncés suivants sont des théorèmes de calcul des prédicats ($(x_i)_{1\leq i \leq m}$ étant la liste des variables libres de $F$; $(y_j)_{1\leq j \leq n}$ celle de $T$ et $(A_i)_{1 \leq i \leq m}, (B_i)_{1 \leq i \leq m},(C_j)_{1 \leq j \leq n}, (D_j)_{1 \leq j \leq n} $ des listes de termes):
    $EXT \Rightarrow \left (\bigwedge_{i=1}^m A_i = B_i \right ) \Rightarrow F\left [x_i:= A_i; 1 \leq i \leq m\right ] \Leftrightarrow F\left [x_i:= B_i; 1 \leq i \leq m\right ] $ et
    $EXT \Rightarrow \left (\bigwedge_{j=1}^n C_j = D_j \right ) \Rightarrow T\left [y_j:= C_j; 1 \leq j \leq n\right ] = T\left [y_j:= D_j; 1 \leq i \leq n\right ] $
    En particulier on a toujours $\vdash EXT \Rightarrow \left (A = B \Rightarrow  G[x:= A] \Leftrightarrow G[x:= B] \right )$ et $\vdash EXT \Rightarrow \left (A = B \Rightarrow  U[x:= A] = U[x:= B] \right )$ pour tout énoncés $G$, tous termes $U,A,B$ et toute lettre $x$ libre ni dans $A$ ni dans $B$.
    Autrement dit que $=$ vérifie la propriété de Leibniz dès que l'axiome d'extensionalité est satisfait et on en déduit facilement (l'énoncé "$\exists a, a = T$" voulant intuitivement dire "$T$" est un ensemble lorsque $a$ n'est pas libre dans le terme $T$) que les énoncés $EXT \Rightarrow \exists a, a = T \Rightarrow \forall b P \Rightarrow P[b:= T]$ et $EXT \Rightarrow \exists a, a = T  \Rightarrow P[b:= T] \Rightarrow \exists b P$ sont des théorèmes de calcul des prédicats pour tous termes $T$, formules $P$ et lettres distinctes $a,b$ libres ni dans $T$ ni dans $P$ (ici $\Rightarrow$ est consiidérée comme prioritaire à droite pour les parenthèses: $A \Rightarrow B \Rightarrow C$ veut dire $A \Rightarrow (B \Rightarrow C)$, $A \Rightarrow B \Rightarrow C \Rightarrow D$ veut dire $A \Rightarrow (B \Rightarrow (C \Rightarrow D))$ etc).
    Exemples (des axiomes - comme mettons ZF ou ZFC - sont bien sûr à rajouter pour que les abréviations suivantes aient le comportement souhaité et en particulier soient des ensembles et non des classes propres): 
    $\{X, Y\}:= \{t \mid t = X \vee t = Y\}$;$\{W\}:= \{x \mid x = W\}$; 
    $(A,B):= \{\{A\}, \{A,B\}\}$; 
    $\bigcap X:= \{y \mid \forall t, t \in X \Rightarrow y \in t\}$; 
    $\bigcup X := \{t \mid \exists u, t \in u \wedge u \in X\}$;
    $A\cup B:= \{x \mid x \in A \vee x \in B\}$; 
    $X \subseteq Y:= \forall z (z \in X \Rightarrow z \in Y)$; 
    $\mathcal P (X):= \{y \mid y \subseteq X\}$; 
    $\emptyset:= \{x \mid x \neq x\}$; 
    $\N:= \bigcap \{x \mid \emptyset \in x \wedge \forall t, t \in x \Rightarrow t \cup \{t\} \in x\}$; 
    $F(X):= \bigcup \{y \mid (X,y) \in F\}$ (lorsque $F$ est une fonction et $X$ est dans le domaine de $F$, $F(X)$ désigne l'image de $X$ par $F$)
     etc.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • @Congru : Définissable dans une théorie, je ne vois pas ce que cela veut dire et je parlais de définissable dans le langage (même si l'intérêt peut exister pour une théorie et pas pour une autre) par exemple dans un langage avec $=$ et $+$, il est courant de définir $\leq$ : 
    $$ ((x\leq y) \Leftrightarrow \exists z (x+z=y))$$
    Cette définition a du sens (sémantique) pour Peano ou Presburger, pas pour la théorie des groupes, mais elle y est quand même valide.

    L'exemple auquel je pensais concerne le même langage : pour tout entier $n$ on définit $\equiv_n$ par 

    $$a \equiv_n b \Longleftrightarrow \exists x(n\cdot x + a = b)$$

    Note : on pourrait faire deux reproches à cette définition :smile:
    1. La multiplication n'existe pas dans le langage de Presburger.
    2. Les entiers n'existe pas dans le langage de Presburger
    Le $n\cdot x$ n'est qu'une abréviation non mathématique servant à la communication entre moi et vous (et à l'écriture des formules), on peut facilement remplacer la définition de $\equiv_5$ par : 
    $$a \equiv_5 b \Longleftrightarrow \exists x(x + x + x + x +x + a = b)$$

    Toute formule n'utilisant qu'un nombre fini de symboles, il n'y a pas de problème.

    Il est clair que la théorie n'est pas modifiée, par contre, à l'aide de ces $\aleph_0$ nouveaux symboles, on peut montrer que Presburger admet l'élimination des quantificateurs avec un procédé de construction de la formule équivalente à une formule avec quantificateur.
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • Merci à vous tous d'avoir enrichi ce fil.
    J'avais dû m'absenter pour plus d'un mois pour des raisons personnelles.
    C'est seulement maintenant que je lis vos réponses, (ça fait un peu près 5 jour que je suis revenu sur le forum).
    Family, mathematics, friends
  • Sinon, j'ai une nouvelle preuve pour le théorème de complétude. Est-ce qu'une telle chose serait intéressante ?
    Family, mathematics, friends
Connectez-vous ou Inscrivez-vous pour répondre.