Pourquoi la solidité implique-t-elle la cohérence?

12

Je lisais la question La cohérence et l'exhaustivité impliquent la solidité? et la première déclaration y dit:

Je comprends que la solidité implique la cohérence.

Ce qui m'a laissé perplexe parce que je pensais que la solidité était une affirmation plus faible que la cohérence (c'est-à-dire que je pensais que les systèmes cohérents devaient être solides mais je suppose que ce n'est pas vrai). J'utilisais la définition informelle que Scott Aaronson utilisait dans son cours 6.045 / 18.400 au MIT pour la cohérence et la solidité:

  1. Solidité = Un système de preuve est solide si toutes les déclarations qu'il prouve sont réellement vraies (tout ce qui est prouvable est vrai). c'est-à-dire SI ( est prouvable) ( est Vrai). Donc SI (il y a un chemin vers une formule) ALORS (cette formule est vraie)ϕϕ
  2. Cohérence = un système cohérent ne prouve jamais A et NON (A). Donc, un seul A ou sa négation peut être vrai.

En utilisant ces définitions (peut-être informelles) à l'esprit, j'ai construit l'exemple suivant pour démontrer qu'il existe un système qui est solide mais pas cohérent:

CharlieSystem{Axioms={A,¬A},InferenceRules={NOT()}}

La raison pour laquelle je pensais que c'était un système de sonorisation est que, par hypothèse, les axiomes sont vrais. Donc A et non A sont tous les deux vrais (oui je sais que la loi du milieu exclu n'est pas incluse). Puisque la seule règle d'inférence est la négation, nous obtenons que nous pouvons atteindre A et non A à partir des axiomes et nous atteindre. Ainsi, nous n'atteignons des déclarations vraies qu'en ce qui concerne ce système. Cependant, bien sûr, le système n'est pas cohérent car nous pouvons prouver la négation de la seule déclaration du système. Par conséquent, j'ai démontré qu'un système de son peut ne pas être cohérent. Pourquoi cet exemple est-il incorrect? Qu'ai-je fait de mal?

Dans ma tête, cela a un sens intuitivement parce que la solidité dit simplement qu'une fois que nous partons de et axiome et manivelle les règles d'inférence, nous n'atteignons que les destinations (c'est-à-dire les déclarations) qui sont vraies. Cependant, cela ne dit pas vraiment quelle destination nous arrivons. Cependant, la cohérence dit que nous ne pouvons atteindre que les destinations qui atteignent ou (les deux pas les deux). Donc, chaque système cohérent doit inclure la loi du milieu exclu comme axiome, ce que bien sûr je n'ai pas fait et ensuite juste inclure la négation du seul axiome comme seul autre axiome. Donc, je n'ai pas l'impression d'avoir fait quelque chose de trop intelligent, mais quelque chose ne va pas?A¬A


Je me rends compte que cela pourrait être un problème parce que j'utilise la définition informelle de Scott. Même avant d'écrire la question, j'ai vérifié wikipedia mais leur définition n'avait pas de sens pour moi. En particulier la partie qu'ils disent:

par rapport à la sémantique du système

leur citation complète est:

chaque formule qui peut être prouvée dans le système est logiquement valable par rapport à la sémantique du système.

Charlie Parker
la source
Tous les systèmes qui nous intéressent peut contradiction TIRENT et . ¬ AA¬A
Yuval Filmus
@YuvalFilmus Je ne pense pas comprendre ce que signifie votre commentaire ... cela signifie-t-il qu'avec mes axiomes, vous pouvez toujours tirer une contradiction? C'était en quelque sorte mon point de vue non? Désolé, je ne comprends pas. Je pense que ma question porte uniquement sur la sémantique du mot «solidité» et «cohérence», car mon exemple concerne uniquement la catégorisation du «système logique» que j'ai inventé.
Charlie Parker
Cela signifie que votre système n'est pas si intéressant. Tous les systèmes qui apparaissent dans la recherche sont suffisamment solides pour dériver la contradiction dans ce contexte.
Yuval Filmus
1
@YuvalFilmus mon système n'est pas supposé être "intéressant" pour faire de vrais maths, bien sûr que je le sais. Mon système a été défini pédagogiquement pour rendre ma question claire et simple bien sûr et clarifier la confusion que j'ai en ce qui concerne la solidité et la cohérence. Mais dans cette conférence que j'ai liée, Scott dit plus tard que Soundness puisqu'il parle de "vraie" vérité, doit être cohérent parce que la vérité doit être cohérente avec elle-même (c'est-à-dire que True ne peut pas être égal à False). Il semble donc que le système sonore hérite automatiquement par axiome du milieu exclu automatiquement. Est ma compréhension actuelle.
Charlie Parker
Est-ce que et tous les deux vrais? Sinon, comment est-ce que ça sonne? ¬ AA¬A
user253751

Réponses:

16

Je recommande d'examiner la logique formelle au-delà des descriptions vagues et ondulées. C'est intéressant et très pertinent pour l'informatique. Malheureusement, la terminologie et la focalisation étroite de même les manuels spécifiquement sur la logique formelle peuvent présenter une image déformée de ce qu'est la logique. Le problème est que la plupart du temps, lorsque les mathématiciens parlent de «logique», ils signifient (souvent implicitement) la logique propositionnelle classique ou la logique classique du premier ordre. Bien qu'il s'agisse de systèmes logiques extrêmement importants, ils sont loin de la largeur de la logique. Quoi qu'il en soit, ce que je vais dire se déroule en grande partie dans ce contexte étroit, mais je tiens à préciser que cela se produit dans un contexte particulier et n'a pas besoin d'être vrai en dehors de celui-ci.

Premièrement, si la cohérence est définie comme ne prouvant pas à la fois et , que se passe-t-il si notre logique n'a même pas de négation ou si¬ A ¬A¬A¬signifie autre chose? De toute évidence, cette notion de cohérence fait certaines hypothèses sur le contexte logique dans lequel elle opère. Typiquement, c'est que nous travaillons dans la logique propositionnelle classique ou dans une extension de celle-ci comme la logique classique du premier ordre. Il existe de multiples présentations, c'est-à-dire des listes d'axiomes et de règles, que l'on pourrait appeler la logique propositionnelle / de premier ordre classique mais, pour nos besoins, cela n'a pas vraiment d'importance. Ils sont équivalents dans un certain sens approprié. Typiquement, lorsque nous parlons d'un système logique, nous entendons une théorie (classique) du premier ordre. Cela commence par les règles et les axiomes (logiques) de la logique classique du premier ordre, auxquels vous ajoutez des symboles de fonction, des symboles de prédicat et des axiomes donnés (appelés axiomes non logiques). Ces théories de premier ordre sont généralement ce que nous '

Ensuite, la solidité signifie généralement la solidité par rapport à une sémantique. La cohérence est une propriété syntaxique liée aux preuves formelles que nous pouvons faire. La solidité est une propriété sémantique qui a à voir avec la façon dont nous interprétons les formules, les symboles de fonction et les symboles de prédicat en objets et déclarations mathématiques. Pour même commencer à parler de solidité, vous devez donner une sémantique, c'est-à-dire une interprétation des choses susmentionnées. Encore une fois, nous avons une séparation entre les connecteurs logiques et les axiomes logiques, et les symboles de fonction, les symboles de prédicat et les axiomes non logiques. Ce qui fait des connecteurs des connecteurs et des axiomes logiques des axiomes logiques du point de vue sémantique, c'est qu'ils sont traités spécialement par la sémantique, contrairement aux symboles de fonction, aux symboles de prédicat et aux axiomes non logiques.[[[φψ]]=[[φ]][[ψ]] où j'utilise comme interprétation de la formule . En particulier, Où est l'ensemble de domaines. L'idée est qu'une formule est interprétée comme l'ensemble des (tuples d'éléments) de domaine qui satisfont la formule. Une formule fermée (c'est-à-dire sans variable libre) est interprétée comme une relation nulle, c'est-à-dire un sous-ensemble d'un ensemble singleton qui ne peut être que ce singleton ou l'ensemble vide. Une formule fermée est "vraie" si elle n'est pas interprétée comme l'ensemble vide. La solidité est alors la déclaration que chaque formule prouvable (fermée) est "vraie" dans le sens ci-dessus.φ [[[φ]]φD[[¬φ]]=D[[φ]]D

Il est facile à partir d'ici, même à partir du croquis que j'ai donné, de prouver que la solidité implique la cohérence (dans le contexte de la logique classique du premier ordre et de la sémantique que j'ai esquissée). Si votre logique est solide, alors chaque formule prouvable interprète comme un ensemble non vide, mais est toujours interprété comme l'ensemble vide quelle que soit la formule , et donc ne peut pas être prouvée, c'est-à-dire que votre logique est cohérente.[

[[φ¬φ]]=[[φ]](D[[φ]])=
φ[[φ¬φ]]φ
Derek Elkins a quitté SE
la source
2
n'hésitez pas à me recommander un livre sur la logique, je ne sais pas vraiment ce qu'est une bonne référence, surtout pour les débutants en logique. Le plus drôle, c'est que j'ai pris des algorithmes et une analyse réelle, donc je n'ai jamais vraiment réfléchi à la logique elle-même.
Charlie Parker
1
intéressant, j'ai toujours pensé que "vérité" signifiait que nous mappions une déclaration aux valeurs booléennes 0 et 1. Mais il semble que ce soit incorrect. Je suppose que nous pouvons en quelque sorte réparer mon mauvais modèle en ayant vide la carte définie à 0 et non vide à 1. Sinon, je ne suis pas sûr de savoir comment on peut réécrire votre preuve dans "ma définition de la vérité comme fonction mappage sur 1 ou 0 ".
Charlie Parker
1
C'est la sémantique typique de la logique propositionnelle classique , qui peut être considérée comme un cas particulier de la logique classique du premier ordre où tous les prédicats sont nuls. Les valeurs booléennes de «vérité» sont effectivement mappées à l'ensemble vide et à l'ensemble singleton dans cette vue. Un des points moins flagrants de mon premier paragraphe était de suggérer que différentes logiques ont des notions différentes de sémantique. Même pour une logique fixe, il existe plusieurs sémantiques possibles qui pourraient lui être données. Il y a une raison pour laquelle je dis "la sémantique typique" et pas seulement "la sémantique".
Derek Elkins a quitté SE le
1
Derek, si vous avez le temps, ça vous dérange peut-être de faire un exemple concret du domaine et comment cela mène-t-il effectivement à l'ensemble vide? (Je suis également heureux de poser une nouvelle question si vous préférez) J'avais en tête un exemple mais je ne savais pas comment le compléter. L'exemple montrait que 2 est rationnel ET 2 est irrationnel conduisent à l'ensemble vide (ou avec ). Je pensais que D est un tuple d'entiers. Ensuite, Mappé à mais je ne savais pas à quoi Mappé. Savez-vous comment terminer cet exemple de manière sensée ou me montrer un exemple? [2( 2 , 1 ) [[[2 is rational]](2,1)[[2 is irrational ]]
Charlie Parker
1
C'est là que la philosophie des mathématiques peut entrer en jeu. Les platoniciens croient que la vérité des énoncés théoriques définis (par exemple) est tout simplement connaissable sans avoir recours à la logique. On peut dire que les expressions théoriques définies sont la signification des formules logiques. Les formalistes utiliseront des approches syntaxiques plutôt que sémantiques, c'est-à-dire "true" = "provable". Les constructivistes ont une notion différente de la «vérité» et leur sous-école plus orientée vers le calcul serait témoin de la «vérité» via un programme.
Derek Elkins a quitté SE le
3

La solidité et la cohérence sont des propriétés des systèmes déductifs. La solidité ne peut être définie que par rapport à certaines sémantiques supposées être données indépendamment du système déductif.

Dans le domaine de la sémantique, les deux propriétés sont liées

Définition 1 ( solidité [sémantique] - empruntée à Wikipédia ) est basé.

Définition 2 ( cohérence [Sémantique] ) Un ensemble de phrases dans la langue est cohérente si et seulement s'il existe une structure de la langue qui satisfait toutes les phrases . Un système déductif est cohérent s'il existe une structure qui satisfait toutes les formules qui y sont prouvables.L L AALLA

Avec les deux définitions données ci-dessus, il est clair que la solidité implique la cohérence. C'est-à-dire que si l'ensemble de toutes les phrases prouvables est valable dans toutes les structures du langage, alors il existe au moins une structure qui les satisfait.

Dmitri Chubarov
la source
1
en fait, j'ai évité explicitement wikipedia parce que je ne comprends pas ce que signifie "par rapport à la sémantique". Pourriez-vous clarifier ce que cela signifie? Cela vous dérange-t-il également d'expliquer un peu plus clairement pourquoi sa clarté implique une cohérence? Bien sûr, ce n'est pas clair pour moi puisque cette question existe: p
Charlie Parker
@CharlieParker J'ai lu vos commentaires sous d'autres articles. Je ne suis pas sûr qu'il existe un texte pour les débutants qui explique mieux les bases des systèmes de preuve et de la théorie des modèles que les chapitres d'introduction de "Model Theory" de Hodges. Une exception étant "A Shorter Model Theory" du même auteur. J'avoue, dans mon article, j'ai triché et défini la cohérence comme satisfiabilité , car l'intérêt de parler de cohérence est d'avoir une caractérisation de la satisfiabilité au sein du système de preuve.
Dmitri Chubarov
Merci! Je vais vérifier ceux-ci! En fait, je n'ai pas besoin d'un "livre débutant" et un bon livre c'est bien. Si le livre met également l'accent sur les intuitions et les idées plutôt que sur les seules preuves, ce serait encore mieux!
Charlie Parker
2

Votre système de preuve n'est ni solide ni cohérent, puisque n'est une proposition vraie que si , auquel cas n'est pas une proposition vraie. Cet argument montre que chaque système insonorisé est également cohérent.A ¬ A AA¬A

Yuval Filmus
la source
Qu'est-ce qui ne va pas avec une fonction qui mappe les choses à Vrai ou Faux. et sont des symboles mappant à la fois True (comme dans le système que j'ai défini). Je ne suis pas sûr de ce qui est techniquement mauvais avec cela au-delà de ne pas être "intéressant" pour faire de vrais maths. Mais définir un véritable système de calcul n'était pas le but de ma question. A ¬ ATruth()A¬A
Charlie Parker
La vérité a une définition sémantique: évaluer à vrai dans toutes les affectations de vérité. Vous ne pouvez pas choisir comment définir ce terme.
Yuval Filmus
C'est peut-être là que je suis confus, d'où ma question. Bien que techniquement, Scott ait mentionné la vérité ne peut pas être définie mathématiquement ... mais permet d'ignorer cette technicité pour des raisons d'argument afin que je puisse comprendre le problème. Pouvez-vous expliquer à nouveau ce que signifie la vérité? Merci pour votre patience. :)
Charlie Parker
1
Dans le contexte de la logique propositionnelle, une formule est une tautologie si elle est vraie dans toutes les affectations de vérité. Un système de preuve propositionnelle est valable si toutes les formules qu'il prouve sont tautologiques.
Yuval Filmus
Je sais que vous essayez d'aider et je l'apprécie, mais en quelque sorte, votre preuve est trop courte pour vraiment m'expliquer ce qui n'a pas fonctionné avec mon exemple dans le message d'origine. Si vous pouvez clarifier ce serait génial. Je suppose que ma question est, quelles affectations de vérité posent des problèmes au système que j'ai suggéré?
Charlie Parker
2

Souvent, lorsque nous proposons des systèmes logiques, ils sont motivés par une tentative de décrire un phénomène préexistant. Par exemple, l'arithmétique Peano est une tentative d'axiomatiser les nombres naturels ainsi que les opérations d'addition et de multiplication.

La solidité ne peut être définie que par rapport au phénomène que vous essayez de décrire, et signifie essentiellement que vos axiomes et règles d'inférence décrivent vraiment la chose en question. Ainsi, par exemple, l'arithmétique de Peano est bonne parce que ses axiomes et ses règles d'inférence sont vraiment vrais pour les nombres naturels.

Ceci, bien sûr, implique que vous avez un concept de "nombres naturels" au-delà de la définition que Peano en a, et une certaine notion de ce qui est vrai ou faux pour les nombres naturels sans avoir dérivé ces vérités à partir d'un ensemble particulier d'axiomes. Essayer d'expliquer d'où viennent ces vérités ou comment elles peuvent être vérifiées peut vous atterrir dans les eaux chaudes philosophiques. Mais si vous considérez qu'il existe des nombres naturels et qu'il existe une collection de faits réels à leur sujet, vous pouvez voir le projet d'axiomatisation comme une simple tentative de proposer une spécification formelle concise à partir de laquelle la plupart des plus importants des vérités peuvent être dérivées. Une axiomatisation est alors valable si tout ce qu'elle peut prouver se trouve réellement dans la collection de vérités prédéfinie, c'est-à-dire

(Notez en particulier que votre spécification formelle ne va pas prouver tout ce qui est vrai sur les nombres naturels, et ne décrira pas non plus de manière unique les nombres naturels dans la mesure où il existe d'autres structures, différentes des nombres naturels, dans lesquelles les axiomes de Peano sont également vrai.)

Dans la logique du premier ordre, au moins, une théorie est cohérente si elle n'a aucun modèle. La solidité signifie qu'il a le modèle spécifique que vous vouliez: la structure particulière que vous tentiez de décrire avec votre théorie est vraiment un modèle de votre théorie. De ce point de vue, il est clair pourquoi la solidité implique la cohérence.

Comme exemple d'une théorie qui est cohérente mais pas solide: l'arithmétique Peano, PA, est capable de coder des formules logiques en tant que constructions arithmétiques, et en particulier vous pouvez coder la phrase "PA est cohérent" ("il n'y a aucune preuve de mensonge de les axiomes de PA "). Appelez cette phrase Con (PA). Vous pouvez également être conscient que (puisqu'il est solide, et donc cohérent), PA ne peut pas prouver Con (PA), par le premier théorème d'incomplétude de Gödel. Cela signifie également que la théorie PA +¬Con (PA) ne peut pas prouver une contradiction, elle doit donc être cohérente. Mais ce n'est pas sain: il prétend qu'il existe un nombre naturel codant une preuve de mensonge des axiomes de PA, mais il ne peut pas y avoir un tel nombre dans les "vrais" nombres naturels, car sinon nous serions en mesure d'extraire une véritable preuve de l'incohérence de l'AP de celui-ci.

PA + Con (PA) a des modèles, mais ce sont des modèles qui doivent inclure des objets "supplémentaires", des "nombres naturels non standard", dont un qui, selon lui, code la "preuve" en question. La théorie n'est tout simplement pas dotée des outils nécessaires pour distinguer ces éléments non standard des véritables membres authentiques de , ni pour démontrer que la preuve n'est pas une preuve légitime.N¬N

Vous pouvez également interpréter ceci comme: PA + Con (PA) est un système logique parfaitement légitime - il ne décrit simplement pas avec précision les nombres naturels, et les nombres naturels n'en sont pas un modèle.¬

Encore une chose: nous ne supposons pas que les axiomes sont vrais par définition. Tous les axiomes ne sont par définition que les éléments de base des preuves. Ce ne sont que des affirmations: elles ne sont vraies ou fausses que lorsqu'elles sont appliquées à des objets mathématiques particuliers. Vous pouvez avoir de faux axiomes, c'est juste assez idiot, car votre système ne sera alors nécessairement et immédiatement pas sain.

Ben Millwood
la source
1

Pour avoir une réponse concise (et intuitive), je paraphraserai ce que Scott Aaronson a dit dans sa conférence MIT 6.045 / 18.400. Il a dit quelque chose comme ceci:

La solidité signifie que tout ce qui est prouvable est vrai. Puisque la cohérence signifie qu'il n'y a pas de contradictions et que la solidité est déjà impliquée, le concept de vérité et de vérité doit être cohérent (c'est-à-dire vrai! = Faux), alors cela doit signifier que les systèmes sonores sont également cohérents. La solidité implique donc la cohérence parce que les choses (vraiment) vraies n'ont pas de contradictions.

Maintenant que je réfléchis, je me rends compte que j'avais des hypothèses / idées incorrectes:

  1. Je ne savais pas que la solidité concernait la sémantique. Ainsi, je n'ai pas réalisé que le simple fait d'utiliser des règles d'inférence à partir des axiomes ne suffit pas pour entraîner de véritables conséquences (et que cela ne le garantit pas, ce que je pensais impossible d'atteindre des choses contradictoires tant que nous partions des axiomes et utilisé des règles d'inférence valides).
  2. J'ai pensé que tant que les axiomes étaient vrais et que les règles d'inférence avaient un sens, tout ce qui se passerait serait vrai. Ce que je réalise maintenant n'est peut-être pas vrai car si nous avons juste une liste géante d'axiomes et de règles d'inférence, il est difficile de raisonner si tout ce qui suit sera vrai. c'est-à-dire qu'il ne suffit pas de partir d'un axiome et d'utiliser une règle d'inférence valide pour garantir que la prochaine étape sera vraie.
  3. Le précédent est essentiellement couplé avec le fait que je ne me suis pas rendu compte qu'il existe deux niveaux de complexité, 1) la sémantique 2) la syntaxe. Lancer le jeu de crunching des symboles peut conduire à des contradictions.
  4. Je ne savais pas que je ne connaissais pas la bonne caractérisation de la vérité, ce que Derek a fait un excellent travail pour caractériser.
Charlie Parker
la source
"Je pensais que tant que les axiomes étaient vrais et que les règles d'inférence avaient un sens, tout ce qui se passerait serait vrai." Pour une notion suffisamment précise de «sens», c'est correct. Si votre système est défectueux, alors (au moins) l'un de vos axiomes est faux ou les règles d'inférence invalides.
Ben Millwood
@BenMillwood mais c'est faux, non? En raison du deuxième théorème d'incomplétude de Godel. Pour tout système formel F qui englobe l'arithmétique, on ne peut pas prouver sa cohérence au sein de F. J'ai pris cela pour signifier que mon hypothèse de solidité est impossible (c'est-à-dire que nous ne pouvons pas avoir un système formel que tout ce qui est prouvable en lui est Vrai parce que cela impliquent une cohérence qui est impossible, semble-t-il, à moins bien sûr que je ne me sois trompé sur le 2ème théorème d'incomplétude). Pour être honnête, je suis d'accord si nous n'avons pas l'exhaustivité, ce qui me dérange, c'est que nous ne pouvons même pas avoir de cohérence.
Charlie Parker
F peut certainement être cohérent, vous ne pouvez tout simplement pas trouver une preuve de ce fait en F. Vous devez faire appel à un système plus puissant ou à des arguments informels, ou simplement accepter une sorte d'incertitude qui, même si F peut être cohérent, vous ne sera pas en mesure de construire un argument étanche qu'il en est ainsi.
Ben Millwood
@BenMillwood Je suppose que c'est ce que je suppose dans ma réponse. Qu'il existe une incertitude sur le fait que les preuves fonctionnent réellement et qu'une prochaine étape pourrait conduire à un mensonge. Si je savais que ce n'était pas vrai, je saurais avec certitude que je ne parviendrai jamais à une contradiction qui viole le deuxième théorème d'incomplétude de Godel. Ou c'est ce que je comprends jusqu'à présent.
Charlie Parker
@BenMillwood Je suppose que j'ai abandonné la croyance selon laquelle l'application des règles d'inférence nous donne les prochaines déclarations qui sont vraies avec 100%. Au lieu de cela, je pense que j'ai implicitement supposé que croire que progresser n'est qu'une question de syntaxe plutôt que de sémantique ... pourrait bien être faux, ce sujet semble déroutant et subtil.
Charlie Parker