Quand la CS théorique se soucie-t-elle (ou devrait-elle) des preuves intuitionnistes?

D'après ce que je comprends (ce qui est très peu, corrigez-moi donc là où je me trompe!), La théorie des langages de programmation s'intéresse souvent aux preuves "intuitionnistes". Dans ma propre interprétation, l'approche nous oblige à prendre au sérieux les conséquences du calcul sur la logique et la prouvabilité. Une preuve ne peut exister que s'il existe un algorithme construisant les conséquences des hypothèses. Nous pourrions rejeter comme axiome le principe du milieu exclu, par exemple, parce qu'il présente un objet, qui est soit soit , non constructif.¬ $X$$\lnot X$

La philosophie ci-dessus pourrait nous conduire à préférer des preuves intuitivement valables à celles qui ne le sont pas. Cependant, je n'ai vu aucune inquiétude quant à l'utilisation réelle de la logique intuitionniste dans des articles dans d'autres domaines de la théorie théorique. Nous semblons heureux de prouver nos résultats en utilisant la logique classique. Par exemple, on pourrait imaginer utiliser le principe du milieu exclu pour prouver qu'un algorithme est correct. En d'autres termes, nous nous soucions et prenons au sérieux un univers limité par les calculs dans nos résultats, mais pas nécessairement dans nos preuves de ces résultats.

1. Les chercheurs en CS théorique se préoccupent-ils jamais d'écrire des preuves intuitivement valables? Je pourrais facilement imaginer un sous-domaine de l'informatique théorique qui cherche à comprendre quand les résultats TCS, en particulier algorithmiques, tiennent dans la logique intuitionniste (ou plus intéressant, quand ils ne le font pas). Mais je n'en ai pas encore rencontré.

2. Y a-t-il un argument philosophique selon lequel ils devraient le faire? Il semble que l'on puisse affirmer que les résultats de l'informatique doivent être prouvés intuitivement lorsque cela est possible, et nous devons savoir quels résultats nécessitent par exemple PEM. Quelqu'un at-il essayé de faire un tel argument? Ou peut-être existe-t-il un consensus sur le fait que cette question n'est tout simplement pas très importante?

3. En guise de question secondaire, je suis curieux de connaître des exemples de cas où cela importe réellement: existe-t-il des résultats importants du TCS connus pour tenir dans la logique classique mais pas dans la logique intuitionniste? Ou soupçonné de ne pas tenir dans la logique intuitionniste.

Toutes mes excuses pour la douceur de la question! Cela peut nécessiter une reformulation ou une réinterprétation après avoir entendu les experts.

Comme je l'ai dit dans les commentaires, la logique intuitionniste n'est pas le point principal. Le point le plus important est d'avoir une preuve constructive. Je pense que la théorie des types de Martin-Löf est beaucoup plus pertinente pour la théorie du langage de programmation que la logique intuitionniste et il y a des experts qui ont soutenu que le travail de Martin-Löf est la principale raison de la renaissance de l'intérêt général pour les mathématiques constructives.

L'interprétation calculable de la constructivité est une perspective possible, mais ce n'est pas la seule. Nous devons être prudents ici lorsque nous voulons comparer des preuves constructives à des preuves classiques. Bien que les deux puissent utiliser les mêmes symboles, ce qu'ils signifient par ces symboles sont différents.

Il est toujours bon de se rappeler que les preuves classiques peuvent être traduites en preuves intuitionnistes. En d'autres termes, en un sens, la logique classique est un sous-système de la logique intuitionniste. Par conséquent, vous pouvez réaliser (par exemple en utilisant des fonctions calculables) des preuves classiques dans un sens. D'un autre côté, nous pouvons considérer les mathématiques constructives comme un système mathématique dans un cadre classique.

$A \lor B$$A \lor B$$\lor$

$\forall x \ \exists y \ \varphi(x,y)$$x$$y$$\varphi(x,y)$$y$$y$$x$$A$$x$$\varphi(x,A(x))$$A$

Maintenant pourquoi nous n'utilisons pas la logique intuitionniste dans la pratique? Il y a plusieurs raisons. Par exemple, la plupart d'entre nous ne sont pas formés avec cet état d'esprit. Trouver une preuve classique d'une déclaration pourrait également être beaucoup plus facile que d'en trouver une preuve constructive. Ou nous pouvons nous préoccuper des détails de bas niveau qui sont cachés et non accessibles dans un cadre constructif (voir aussi la logique linéaire ). Ou nous pourrions tout simplement ne pas être intéressés à obtenir les éléments supplémentaires fournis avec une preuve constructive. Et bien qu'il existe des outils pour extraire les programmes des preuves, ces outils ont généralement besoin de preuves très détaillées et n'ont pas été suffisamment conviviaux pour le théoricien général. Bref, trop de douleur pour trop peu d'avantages.

$\Pi^0_2$$PA$$PA$$PA$

Je me souviens que Douglas S. Bridges, dans l'introduction de son livre sur la théorie de la calculabilité, a soutenu que nous devrions prouver nos résultats de manière constructive. Il donne un exemple dont l'IIRC est essentiellement le suivant:

Supposons que vous travaillez pour une grande société de logiciels et que votre responsable vous demande un programme pour résoudre un problème. Serait-il acceptable de revenir avec deux programmes et de dire à votre manager une de ces deux solutions correctement mais je ne sais pas lequel?

À la fin, nous devons garder à l'esprit que bien que nous utilisons les mêmes symboles pour les logiques classiques et intuitionnistes, ces symboles ont des significations différentes, et celui à utiliser dépend de ce que nous voulons exprimer.

Pour votre dernière question, je pense que le théorème de Robertson-Seymour serait un exemple de théorème dont nous savons qu'il est vrai classiquement, mais nous n'en avons aucune preuve constructive. Voir également

• Existe-t-il des preuves d'existence d'algorithmes non constructifs?

Il vaut la peine de réfléchir POURQUOI la logique intuistioniste est la logique naturelle du calcul, car trop souvent les gens se perdent dans les détails techniques et ne parviennent pas à saisir l'essence du problème.

Très simplement, la logique classique est une logique d'information parfaite: toutes les déclarations au sein du système sont supposées connues ou connaissables comme étant sans ambiguïté vraies ou fausses.

La logique intuitionniste, en revanche, a de la place pour des déclarations avec des valeurs de vérité inconnues et inconnaissables. Ceci est essentiel pour le calcul, car, grâce à l'indécidabilité de la terminaison dans le cas général, il ne sera pas toujours certain de la valeur de vérité de certaines déclarations, ni même si une valeur de vérité peut jamais être affectée à certaines déclarations .

$\neg\neg P \implies P$

À mon avis, ces raisons "sémantiques" sont une motivation beaucoup plus importante pour l'utilisation de la logique intuistioniste pour le calcul que toute autre raison technique que l'on pourrait rassembler.

Les fonctions de hachage cryptographique du monde réel comme MD5 et SHA sont sans clé. En tant que tel, il est assez difficile d'appliquer des techniques de cryptographie théorique pour raisonner sur leur sécurité. La raison simple pour laquelle: pour toute fonction de hachage sans clé, il existe un très petit programme / adversaire qui génère une collision sous cette fonction de hachage; à savoir, un programme qui a une telle collision - qui doit exister! - codé en dur.

L'article de Phil Rogaway Formaliser l'ignorance humaine: le hachage résistant aux collisions sans les clés traite de ce problème. Il y montre que certains théorèmes très standard pour les fonctions de hachage à clé (comme le paradigme de construction et de hachage de Merkle-Damgård) peuvent être adaptés et prouvés avec des déclarations de théorème "intuitionnistes" s'appliquant aux fonctions de hachage sans clé.

voici un joli chapitre sur la logique intuitive d'un livre en ligne complet Logic for Computer Science , 300pp. [1] sec 9.5, p210, résumé sur p220:

La logique intuitionniste est née du mouvement constructiviste en mathématiques qui rejetait les preuves d'existence non constructives ou celles basées sur la loi du milieu exclu. Récemment, un lien entre les mathématiques intuitionnistes et la programmation est né de l'observation que les propositions et les types (au sens de la programmation) sont équivalents. Le développement d'algorithmes dans ce système formel, qui est basé sur la déduction naturelle, consiste à écrire une spécification en notation logique puis, en la considérant comme un type, à prouver qu'elle n'est pas vide. Parce que la logique sous-jacente est constructive la preuve, si elle peut être réalisée,

une autre perspective proche vient de TCSist Andrej Bauer écrivant sur "Mathématiques et calcul; mathématiques pour les ordinateurs" [2] qui propose fondamentalement que "les mathématiques intuitionnistes sont bonnes pour la physique". la présentation est principalement en termes de physique, mais pour ceux qui considèrent CS étroitement couplé à la physique, l'idéologie sera généralement appliquée au TCS.

Interprétation informatique. Il s'agit de l'interprétation de la logique intuitionniste couramment présentée en informatique. Nous considérons tous les ensembles comme représentés par des structures de données appropriées - un point de vue raisonnable pour un informaticien. Ensuite, une déclaration est considérée comme vraie s'il existe un programme (preuves informatiques) témoignant de sa vérité.

[1] Logique pour l'informatique, Reeves et Clark

[2] Mathématiques intuitionnistes pour la physique Bauer