Discussion:Logique monadique du second ordre

	Tâches à accomplir pour Logique monadique du second ordre	aide
	Votre aide est la bienvenue pour corriger les liens, présents dans l'article, vers les pages d'homonymie Convexité ⇒ Quelques explications pour effectuer ces corrections. -- 20 octobre 2016 à 12:59 (CEST)

Article en cours de fabrication

Je me sers du chapitre "Monadic Second-Order Theories" de Gurevich pour étoffer l'article. Si vous avez d'autres références à me conseiller, n'hésitez pas. --Fschwarzentruber (discuter) 16 septembre 2016 à 10:43 (CEST)

Satisfaisabilité/décidabilité

Je vois dans l'introduction : À l'instar de la logique du premier ordre, le problème de satisfiabilité de MSO est indécidable, je ne connais pas MSO (et trouve donc que l'initiative de cet article est une très bonne chose !), mais concernant le premier ordre, il me semble qu'il faudrait préciser, afin que la différence soit plus claire avec MSO, sauf erreur (?) :

• 1/ décidabilité du 1er ordre monadique
• 2/ semi-decidabilité du 1er ordre général (= dyadique car les prédicats binaires suffisent), soit
  • 2.1/ indécidabilité de la satisfaisabilité
  • 2.2/ décidabilité de la non-satisfaisabilité (= de l'incohérence)

... mais p.-e. que cela déborderait le cadre du présent article.

Je vais regarder par ailleurs si je possède des références. Cordialement, --Epsilon0 ε₀ 26 septembre 2016 à 17:49 (CEST)

ːBonsoir Epsilon0. Merci pour ton message. Tes points parlent de fragments du logique du premier ordre. Pour 1/, c'est fait dans "Harrison, Handbook of Practical Logic and Automated Reasoning, je crois." Pour 2 et 2.1 c'est fait dans un livre de logique, par exemple Ben-Ari, Mathematical Logic for Computer Science sans doute. Le point 2.2 est faux ː la non-satisfiabilité de FO est indécidable car la satisfiabilité l'est. Je pense que les points 1., 2. et 2.1 doivent être clairement mis dans l'article sur la logique du premier ordre. Par contre, ton message m'a aidé à améliorer le texte introductif. J'espère qu'il est plus limpide. N'hésite pas à critiquer. Bonne soirée. --Fschwarzentruber (discuter) 26 septembre 2016 à 21:15 (CEST)

Bonjour Francois,

Bon, ceci concerne sans doute d'autres articles dont, pour exemple Problème de la décision ou le nouvel article que tu as initié Logique monadique du premier ordre, néanmoins car je ne veux pas laisser de l'inachevé dans cette présente pdd, je reviens sur ce que tu as dis.

Tu dis : "Le point 2.2 est faux ː la non-satisfiabilité de FO est indécidable car la satisfiabilité l'est."

Je me suis sans doute mal exprimé mais, sauf à ce que quelque chose m'échappe depuis longtemps et que tu m'éclaires sur le sujet, nous allons tomber d'accord sur les faits que, pour une théorie du premier ordre :

• si elle est cohérente, on ne peut pas toujours le démontrer ... intuitivement car elle peut avoir des modèle infinis.
• si elle est incohérente, on peut toujours le démontrer ... intuitivement car "être incohérent" signifie démontrer le faux, qu'une démonstration est toujours finie et qu'à chaque étape d'une tentative de démontrer du faux (ou quoique ce soit) un nombre fini de règles d'inférence sont en jeu.

C'est en ce strict sens, exprimé ci-dessus, que la logique du 1er ordre (générale) est, comme je l'ai dis ci-dessus, semi-decidable.

Maintenant, même si je peux relire, et parler comme ici en pdd, je n'ai plus l'énergie que tu manifestes pour exprimer tout cela dans les articles.

Bien à toi --Epsilon0 ε₀ 19 octobre 2016 à 20:51 (CEST)