Non-prouvabilité en déduction naturelle propositionnelle

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 ?

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.

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.

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.

@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.

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.

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 ?

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.

(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.

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.)

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.