Comment déterminer si une preuve nécessite des «techniques de raisonnement d'ordre supérieur»?

15

La question:

Supposons que j'ai une spécification d'un problème composé d'axiomes et d'un but (c'est-à-dire que le problème de preuve associé est de savoir si le but est satisfaisable étant donné tous les axiomes). Supposons également que le problème ne contienne aucune incohérence / contradiction entre les axiomes. Existe-t-il un moyen de déterminer à l'avance (c'est-à-dire sans avoir d'abord construit une preuve complète) que la preuve du problème nécessitera un "raisonnement d'ordre supérieur"?

Par «raisonnement d'ordre supérieur», j'entends appliquer des étapes de preuve qui nécessitent que la logique d'ordre supérieur soit écrite. Un exemple typique de «raisonnement d'ordre supérieur» serait l'induction: L'écriture d'un schéma d'induction nécessite en principe l'utilisation d'une logique d'ordre supérieur.

Exemple:

On peut spécifier le problème de preuve "L'addition sur deux nombres naturels est-elle commutative?" en utilisant la logique du premier ordre (c.-à-d. définir le nombre naturel via les constructeurs zéro / succ avec les axiomes standard, ainsi que les axiomes qui définissent récursivement une fonction «plus») La preuve de ce problème nécessite une induction sur la structure du premier ou du deuxième argument de "plus" (selon la définition exacte de "plus"). Aurais-je pu le savoir avant d'essayer de le prouver, par exemple en analysant la nature du problème d'entrée ...? (Bien sûr, ce n'est qu'un exemple simple à des fins d'illustration - en réalité, cela serait intéressant pour des problèmes de preuve plus difficiles que la commutativité de plus.)

Un peu plus de contexte:

Dans mes recherches, j'essaie fréquemment d'appliquer des prouveurs de théorèmes de premier ordre automatisés comme Vampire, eprover, etc. pour résoudre des problèmes de preuve (ou des parties de problèmes de preuve), dont certains peuvent nécessiter un raisonnement d'ordre supérieur. Souvent, les prouveurs ont besoin d'un certain temps pour produire une preuve (à condition qu'il y ait une preuve qui ne nécessite que des techniques de raisonnement de premier ordre). Bien sûr, essayer d'appliquer un prouveur de théorèmes de premier ordre à un problème qui nécessite un raisonnement d'ordre supérieur entraîne généralement un délai d'attente.

Par conséquent, je me suis demandé s'il existe des méthodes / techniques qui peuvent me dire à l'avance si un problème de preuve nécessitera des techniques de raisonnement d'ordre supérieur (ce qui signifie "ne perdez pas de temps à le remettre à un prouveur de théorèmes de premier ordre"). ) ou non, au moins peut-être pour des problèmes d'entrée particuliers.

J'ai cherché dans la littérature une réponse à ma question et j'ai demandé à certains collègues chercheurs du domaine du théorème de le prouver - mais jusqu'à présent, je n'ai reçu aucune bonne réponse. Je m'attendais à ce qu'il y ait des recherches sur ce sujet de la part de personnes qui essaient de combiner la démonstration interactive de théorèmes et la démonstration automatisée de théorèmes (communauté Coq? Communauté Isabelle (Sledgehammer)?) - mais jusqu'à présent, je n'ai rien trouvé.

Je suppose qu'en général, le problème que j'ai décrit ici est indécidable (n'est-ce pas?). Mais peut-être y a-t-il de bonnes réponses pour des versions raffinées du problème ...?

automated-theorem-proving program-verification Sylvia Grewe
la source
2
Ce que vous demandez, c'est essentiellement de décider si une formule donnée est prouvable (dans votre système plus faible), ce qui est en général indécidable même pour une théorie simple comme Q. Mais la prouvabilité n'est en fait pas très utile car une théorie plus forte peut raccourcir les preuves d'un théorème a lot. Décider si un théorème a une preuve courte est NP-complet. Je doute qu'il existe une bonne heuristique.
Kaveh
2
L'arithmétique peano a une induction, et l'arithmétique peano est de premier ordre (c'est-à-dire qu'elle quantifie uniquement sur les individus). Idem pour ZFC. Pour citer Martin Davis: «les logiques d'ordre supérieur ne sont que des variantes de notation des théories d'ensemble formalisées dans une logique de premier ordre, la question de l'utilisation de formalismes d'ordre supérieur dans la démonstration de théorèmes mécaniques est simplement une question de savoir si de tels formalismes suggèrent ou non algorithmes utiles. "
Martin Berger
@MartinBerger Je pense qu'aux fins de cette question, les schémas d'axiomes comptent comme des "techniques de raisonnement d'ordre supérieur"
fread2281
@ fread2281 Il est utile de faire attention à la terminologie. Il existe des théories des ensembles qui ont une axiomatisation finie (par exemple la théorie des ensembles de Neumann – Bernays – Gödel qui est une extension conservatrice du ZFC). En revanche, les schémas d'axiomes de ZFC ne peuvent pas être exprimés par un nombre fini d'axiomes. Je pense, mais je ne suis pas sûr en ce moment que les schémas axiomatiques n'ont pas besoin de toute la puissance de la théorie des ensembles ou de la logique d'ordre supérieur.
Martin Berger

Réponses:

6

En bref, chaque théorème énoncé dans la logique du premier ordre a une preuve du premier ordre.

Dans son livre "An Introduction to Mathematical Logic and Type Theory", Peter B. Andrews développe à la fois une logique de premier ordre et un système de logique d'ordre supérieur Q 0 , qui est généralement considéré comme la base théorique des prouveurs modernes d'ordre supérieur. . (Voir l'introduction à la logique HOL par exemple.)

Pour Q 0 et les systèmes similaires, Andrews montre que les logiques d'ordre supérieur qu'il décrit peuvent être considérées comme des extensions conservatrices de la logique du premier ordre et écrit (deuxième édition, p. 259) que, "En résumé, chaque théorème du premier ordre de la théorie des types a une preuve de premier ordre. "

Compte tenu de vos préoccupations pratiques, je cite également le paragraphe suivant:

"Cependant, certains théorèmes de la logique du premier ordre peuvent être prouvés plus efficacement en utilisant des concepts qui ne peuvent être exprimés que dans une logique d'ordre supérieur. Des exemples peuvent être trouvés dans [Andrews et Bishop, 1996] et [Boolos, 1998, chapitre 25] Statman a prouvé [Statman, 1978, Proposition 6.3.5] que la longueur minimale d'une preuve en logique de premier ordre d'une wff de logique de premier ordre peut être extraordinairement plus longue que la longueur minimale d'une preuve de la même wff en la logique du second ordre. Un résultat connexe de Godel [Godel, 1936] est qu'en général, «passer à la logique du prochain ordre supérieur a pour effet, non seulement de rendre prouvable certaines propositions qui ne l'étaient pas auparavant, mais aussi de faire il est possible de raccourcir, d'une quantité extraordinaire, une infinité de preuves déjà disponibles. "Une preuve complète de cela peut être trouvée dans [Buss,1994]. "

Cris P
la source