Non-prouvabilité en déduction naturelle propositionnelle

Par des moyens syntaxiques

a marqué ce sujet comme résolu.
Auteur du sujet

Bonjour,

Je m’intéresse aux démonstrations (niveau méta) de non-prouvabilité de formules propositionnelles simples en déduction naturelle qui se basent sur des arguments syntaxiques. Je me souviens vaguement de la propriété de la sous-formule pour le calcul des séquents, et j’ai vu qu’on pouvait montrer que la déduction naturelle intuitionniste vérifiait une propriété similaire.

Cependant je n’ai pas compris ce qu’il en était pour la logique classique : comment montrer que des énoncés logiques simples ne peuvent pas être prouvés sans avoir recours à la sémantique ?

En tombant sur différents morceaux de cours de Frank Pfenning j’ai également reconnu quelque chose que j’avais étudié il y a longtemps dans un contexte différent, à savoir le « principe d’inversion », qui a l’air d’être un corollaire du théorème d’élimination des coupures. Est-ce que ça peut m’aider ?

Je n’ai pas accès pour l’instant au livre de Prawitz sur la déduction naturelle.

Un avis ?

+0 -0

Bonjour,

Je m’intéresse aux démonstrations (niveau méta) de non-prouvabilité de formules propositionnelles simples en déduction naturelle qui se basent sur des arguments syntaxiques. Je me souviens vaguement de la propriété de la sous-formule pour le calcul des séquents, et j’ai vu qu’on pouvait montrer que la déduction naturelle intuitionniste vérifiait une propriété similaire.

Cependant je n’ai pas compris ce qu’il en était pour la logique classique : comment montrer que des énoncés logiques simples ne peuvent pas être prouvés sans avoir recours à la sémantique ?

En tombant sur différents morceaux de cours de Frank Pfenning j’ai également reconnu quelque chose que j’avais étudié il y a longtemps dans un contexte différent, à savoir le « principe d’inversion », qui a l’air d’être un corollaire du théorème d’élimination des coupures. Est-ce que ça peut m’aider ?

Je n’ai pas accès pour l’instant au livre de Prawitz sur la déduction naturelle.

Un avis ?

Première question, je suis curieux de savoir pourquoi tu t’intéresses à ce genre de problème. En général, la sémantique est justement là pour résoudre ton problème.

Dans le cas de la déduction naturelle pour des formules propositionnelles (donc sans quantificateur), savoir s’il existe une preuve de $P$ est décidable. À partir de là, tu peux essayer d’énumérer toutes les preuves et si à la fin tu n’en as pas trouvé, tu as ta réponse.

Le problème est que tu n’as pas de critère syntaxique ici.

Après, savoir si une formule propositionnelle est prouvable ou non est NP-Complet, donc ton critère syntaxique va être compliqué à vérifier, ou bien sinon tu prouveras P=NP.

Bref, je ne suis pas sûr de bien comprendre ce que tu cherches.

+0 -0
Auteur du sujet

Première question, je suis curieux de savoir pourquoi tu t’intéresses à ce genre de problème. En général, la sémantique est justement là pour résoudre ton problème.

Dans le cas de la déduction naturelle pour des formules propositionnelles (donc sans quantificateur), savoir s’il existe une preuve de $P$ est décidable. À partir de là, tu peux essayer d’énumérer toutes les preuves et si à la fin tu n’en as pas trouvé, tu as ta réponse.

Oui mais je sais déjà qu’il n’existe aucune preuve. Effectivement c’est décidable : il suffit d’avoir recours à une méthode sémantique (par exemple une table de vérité) et de dire oui ou non.

Moi je veux une démonstration qui s’appuie uniquement sur la théorie des preuves du système considéré, pas un algorithme.

+0 -0

Première question, je suis curieux de savoir pourquoi tu t’intéresses à ce genre de problème. En général, la sémantique est justement là pour résoudre ton problème.

Dans le cas de la déduction naturelle pour des formules propositionnelles (donc sans quantificateur), savoir s’il existe une preuve de $P$ est décidable. À partir de là, tu peux essayer d’énumérer toutes les preuves et si à la fin tu n’en as pas trouvé, tu as ta réponse.

Oui mais je sais déjà qu’il n’existe aucune preuve. Effectivement c’est décidable : il suffit d’avoir recours à une méthode sémantique (par exemple une table de vérité) et de dire oui ou non.

Moi je veux une démonstration qui s’appuie uniquement sur la théorie des preuves du système considéré, pas un algorithme.

Ben Dover

Tu peux écrire la preuve en théorie des ensembles en utilisant la sémantique de la déduction naturelle. Tu auras bien un terme de preuve, dans un système méta en théorie des ensembles. De plus, en utilisant la correspondance de Curry-Howard, il est certainement possible de voir cet algorithme comme une preuve dans un système logique ;).

Encore une fois, précise ta question car ce n’est pas clair ce que tu demandes. Et connaître les motivations de ta question permettrait peut-être de mieux te répondre.

+0 -1

Cette réponse a aidé l’auteur du sujet

Après avoir plus réfléchi, je pense que c’est "facile" (mais c’est dur de se convaincre que c’est facile !), et que comme ton intuition le dit une approche purement syntactique marche. Par contre, c’est nettement plus clair en utilisant le calcul des séquents que la déduction naturelle – et comme les deux sont logiquement équivalents, il n’y a pas de raison de ne pas.

Dans toutes les logiques raisonnables, séquents pour la logique classique compris, tu peux prouver l’élimination des coupures. Pour montrer qu’une forme n’est pas prouvable revient alors à montrer qu’il n’existe pas de preuve sans coupure, et ça c’est plus facile car elles sont plus petites (en particulier, sous-formule et tout, il y en a un nombre fini).

Ce qui est encore mieux qu’énumérer toutes les preuves, c’est de regarder leur structure pour réduire l’espace de recherche : c’est ce que fait le focusing. En logique classique (slides sur LKF, la présentation standard des séquents classiques avec focusing), c’est particulièrement peu prise de tête parce que tu peux traiter tous les connecteurs de la logique comme inversibles; ça donne des preuves grosses mais extrêmement automatiques et avec peu de backtracking.

Par exemple si tu veux prouver P /\ not(P) (ou voir qu’il n’est pas prouvable), on part de

1
2
3
   ?
————————
⊢ P ∧ ¬P

on peut, sans perte de généralité, dire qu’une preuve sans coupure commence par une introduction du connecteur ∧ :

1
2
3
4
5
 ?     ?
———   ———— 
⊢ P   ⊢ ¬P
——————————
⊢ P ∧ ¬P

et là on peut encore faire une étape de raisonnement inversible dans la branche droite, mais après on est bloqué :

1
2
3
4
5
6
7
        ?
      ———— 
 ?    P ⊢
———   ———— 
⊢ P   ⊢ ¬P
——————————
⊢ P ∧ ¬P

Il n’existe pas de preuve de (P ⊢) ou (⊢ P) quand P est un atome. Comme les étapes que j’ai faites sont inversibles (elles préservent la prouvabilité), s’il n’existe pas de preuve qui les utilise alors il n’existe pas de preuve du tout. Par complétude du calcul des séquents, cela veut dire que la formule n’est pas prouvable.

Je pense que quelqu’un qui s’y connaîtrait mieux que moi en méthodes sémantiques pourrait pointer du doigt le fait que la recherche de preuve de cette forme correspond à la construction d’un contre-modèle, ou un truc comme ça.

Un dernier point de rappel sur "prouvabilité" et "satisfiabilité" que j’ai besoin de me répéter à chaque fois que je lis un truc fait par des classicistes :

  • "P satisfiable" ça veut dire que si on déclare proprement les variables X₁,..,Xₙ utilisées dans P, on parle de la formule ∃X₁,…,∃Xₙ, P
  • "P prouvable" ça veut dire ∀X₁,..,∀Xₙ, P

C’est pour ça que les gens disent qu’une formule est satisfiable quand sa négation n’est pas prouvable, ou l’inverse : c’est les lois de commutation de la négation et de ∃/∀.

Édité par gasche

+1 -0

@Gasche: ce que tu proposes est tout de même un algorithme avec l’espace de recherche restreint car en déduction naturelle, $A \lor B$ n’est pas inversible si je ne me trompe pas.

Édité par Saroupille

+0 -0
Auteur du sujet

Merci pour ta réponse gasche, on y voit plus clair.

Après avoir plus réfléchi, je pense que c’est "facile" (mais c’est dur de se convaincre que c’est facile !), et que comme ton intuition le dit une approche purement syntactique marche. Par contre, c’est nettement plus clair en utilisant le calcul des séquents que la déduction naturelle – et comme les deux sont logiquement équivalents, il n’y a pas de raison de ne pas.

Malheureusement si : c’est pour des L3 qui n’ont vu que la déduction naturelle.

Dans toutes les logiques raisonnables, séquents pour la logique classique compris, tu peux prouver l’élimination des coupures. Pour montrer qu’une forme n’est pas prouvable revient alors à montrer qu’il n’existe pas de preuve sans coupure, et ça c’est plus facile car elles sont plus petites (en particulier, sous-formule et tout, il y en a un nombre fini).

Je me souviens de ces arguments pour les séquents. Malheureusement on ne les a pas tels quels pour la déduction naturelle classique.

Un dernier point de rappel sur "prouvabilité" et "satisfiabilité" que j’ai besoin de me répéter à chaque fois que je lis un truc fait par des classicistes :

  • "P satisfiable" ça veut dire que si on déclare proprement les variables X₁,..,Xₙ utilisées dans P, on parle de la formule ∃X₁,…,∃Xₙ, P
  • "P prouvable" ça veut dire ∀X₁,..,∀Xₙ, P

C’est pour ça que les gens disent qu’une formule est satisfiable quand sa négation n’est pas prouvable, ou l’inverse : c’est les lois de commutation de la négation et de ∃/∀.

gasche

Hmm je n’ai pas compris si tu disais ça pour me reprendre ou pas. Qu’est-ce que j’aurais dû dire ? Sans hypothèse, |- A n’est pas prouvable, pas plus que sa négation.

Merci pour les slides. Je n’ai pas encore eu le temps de pratiquer, et de toute façon je ne peux pas les utiliser pour répondre à la question originale, mais c’est intéressant quand même.

Oh et quant au focusing, comment se compare-t-il aux techniques à base de preuves par résolution ? Est-ce que c’est une version plus moderne et explicite ?

Édité par Ben Dover

+0 -0

Saroupille : si, en logique classique, la disjonction peut être présentée comme inversible aussi, puisqu’on a un contexte à droite, pas juste une seule formule.

$$ \dfrac {\Gamma, A \vdash \Delta \qquad \Gamma, B \vdash \Delta} {\Gamma, A \vee B \vdash \Delta} \qquad \dfrac {\Gamma \vdash \Delta, A, B} {\Gamma \vdash \Delta, A \vee B} $$

(Mais de toute façon, oui, c’est un algorithme, indépendamment de la question de s’il faut savoir back-tracker ou pas. L’idée c’est qu’on n’utilise que des méthodes syntactiques, pas de modèles.)

Ben Dover : pour le point sur satisfiabilité/prouvabilité, ce n’était pas en référence à ce qui a été dit, mais juste parce que moi j’ai besoin de me le rappeler de temps en temps pour réfléchir à ce que disent les gens de la logique classique.

Pour les étudiants, je dirais deux choses. D’une part, ce n’est pas très difficile de présenter le calcul des séquents à des gens qui connaissent déjà la déduction naturelle (pendant un exposé je le fais en dix minutes, dans un court clair et détaillé c’est l’affaire d’une heure). Ce serait intéressant pour les étudiants.

D’autre part, tu peux te cacher et voir la recherche de preuve dans le calcul des séquents comme une construction de preuve en déduction naturelle. Le plus simple, c’est de s’autoriser à couper sur les sous-formules du judgement (donc une utilisation limitée de la règle de coupure qui vérifie la règle de la sous-formule), et de s’en servir pour montrer que la règle gauche des produits est admissible dans ce cadre (on élimine $A \wedge B$ en coupant successivement sur $A$ puis sur $B$), et pareil pour la négation (on élimine $\neg A$ en coupant sur $A$). Toutes les autres règles sont identiques ou admissibles sans coupure. Ensuite tu fais ta recherche façon séquent, et tu obtiens des jugements aux feuilles qui ne contiennent que des atomes, donc là le raisonnement sur la prouvabilité est le même en déduction naturelle ou en séquents.

Édité par gasche

+0 -0

Pour le focusing, je pense que pour cette application particulière on n’a pas besoin de l’introduire en détail ou du tout, l’important c’est la notion d’inversibilité des règles : montrer que les règles sont inversibles en montrant que la règle inverse est dérivable dans le système avec coupure, et donc que l’algorithme de recherche déterministe qui n’utilise que des règles inversibles préserve la prouvabilité. (Ça paraît un peu magique vu comme ça; regarder le focusing en général donne un cadre global explicatif sur pourquoi ce cas particulier marche comme cela.)

+0 -0

Saroupille : si, en logique classique, la disjonction peut être présentée comme inversible aussi, puisqu’on a un contexte à droite, pas juste une seule formule.

$$ \dfrac {\Gamma, A \vdash \Delta \qquad \Gamma, B \vdash \Delta} {\Gamma, A \vee B \vdash \Delta} \qquad \dfrac {\Gamma \vdash \Delta, A, B} {\Gamma \vdash \Delta, A \vee B} $$
gasche

Je parle bien de la déduction naturelle ici. Les règles que tu donnes sont des règles du calcul des séquents. Pourtant la question posée par Ben Dover est sur la déduction naturelle.

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte