Comments on Une version de Gödel sur l'inséparabilité des théorèmes et antithéorèmes

jonas (2017-02-12T11:55:03Z)

Is this a good place to forward the sad news that Raymond Smullyan has died in 2017-02?

jonas (2016-12-10T20:45:31Z)

You are right about that Robinson arithmetic isn't enough for proving a particular execution trace as unique, and you need something stronger than that but weaker than Peano arithmetic for that.

I think the axiom system called $ \\mathbf{Q}_0 $ Serény György gives in lecture notes <URL: http://www.math.bme.hu/%7Esereny/JEGYZETEK/1.ps.gz > page 4 might be enough. I don't know where that system comes from or whether it has some well-known name. That system is recursive, and is implied by Peano arithmetic if you replace its operators and relations with the Peano arithmetic definitions, and I think it has logical strength incomparable to Robinson arithmetic.

Ruxor (2016-12-06T13:06:04Z)

@jonas: Yes, you're right, your proof works, and I agree it's probably simpler. Two comments, thought: (a) what I did is tantamount to proving the quinian self-reference trick (though it is probably not worth it), and (b) you need a wee bit more than Robinson arithmetic to hold your proof, because you need the system to prove that if a Turing machine halts-and-outputs-no, then it is not true that it halts-and-outputs-yes, and I don't think Robinson's arithmetic proves this (although Peano is far overkill).

Recursively inseparable sets are (moderately) interesting in their own right, though; I introduced them in this context because I thought it was more appropriate to parallel the proof of Gödel's theorem I had given from the undecidability of the halting problem.

jonas (2016-12-05T23:58:35Z)

> Il faut partir de l'existence d'ensembles récursivement énumérables et récursivement inséparables : […] qu'il existe deux machines de Turing (=algorithmes) $ A_1 $ et $ A_2 $ qui énumèrent des ensembles respectivement $ S_1 $ et $ S_2 $, tels que ces ensembles soient disjoints […], et que de plus, il n'existe pas de machine de Turing $ U $ qui termine toujours, répond « 1 » sur les entiers de $ S_1 $ (i.e., énumérés par $ A_1 $) et « 2 » sur ceux de $ S_2 $ (i.e., énumérés par $ A_2 $) (sur les entiers qui ne sont ni dans $ S_1 $ ni dans $ S_2 $, la machine $ U $ peut répondre ce qu'elle veut).

I wasn't familiar with this theorem or the concept of recursively inseparable sets. It might be a concept useful on its own right, but I don't see how you motivate its use in this article. Maybe I'm overlooking some subtlety here, but it seems like your third fact is easier to prove without passing through this theorem, with a proof similar to how you'd prove the second fact.

> Il n'existe pas d'algorithme qui, quand on lui donne un énoncé mathématique $ P $, ou même simplement un énoncé arithmétique $ \\Pi_1 $, (1) termine toujours, et ce (2) en répondant « oui » lorsque $ P $ est un théorème, et (3) en répondant « non » lorsque $ P $ est un antithéorème […].

Fix $ V $ as any machine. We want to prove that it can't satisfy the three conditions above. Choose $ P $ as the following statement: if you run the machine $ V $ with $ P $ as the input, it either doesn't halt, or doesn't output “yes”. This statement can be formalized with some quinian self-reference magic. In fact, it can also be formalized as a $ \\Pi_1 $ statement, and using only such operations that the $ \\mathbf{Q} $ axioms allow proving or disproving it if the machine in fact halts. Now run the machine $ V $ on $ P $. If it doesn't halt, then the condition 1 fails. If it halts and prints “yes”, then $ P $ is an antitheorem, because a full trace of running $ V $ disproves it, so condition 3 fails. Similarly if it halts but doesn't print “yes”, then $ P $ is a theorem, so condition 2 fails.

Does this proof work? If so, can you tell me why it's worth learning about recursively inseparable sets in this context?

SM (2016-12-03T23:10:52Z)

C'était super !

"en revnache" -> "en revanche"
"cas tour à tour" -> "tour à tour"

Touriste (2016-12-02T18:39:31Z)

@SB : je ne le connaissais pas et suis allé le feuilleter en bibliothèque. Le principe de la réédition des papiers originaux, pour mes goûts personnels c'est plutôt bof bof je ne suis pas passionné d'histoire des mathématiques donc je préfére regarder des trucs plus récents et plus synthétiques.

Le texte philosophique de Girard, en lecture rapide c'est intéressant voire rigolo vu le style assez truculent de Girard (mais à bien des égards opaque pour moi, parce que je n'ai pas assez de connaissances en logique pour le suivre en philosophie de la logique) ; ça reste assez pointu, je ne le recommanderais pas comme un ouvrage de vulgarisation à regarder en priorité non, sauf peut-être pour un lecteur qui aurait des réticences à choisir un livre en anglais, mais existè-ce encore ce genre de lecteur ?

SB (2016-12-01T19:06:08Z)

@Touriste: quid du livre de Girard: http://web.archive.org/web/20140408084955/http://www.lygeros.org/articles?n=37&l=fr ?

JML (2016-11-30T20:09:19Z)

Excellent, merci !

SM (2016-11-30T07:31:26Z)

Merci beaucoup !!

Touriste (2016-11-29T16:42:10Z)

@ Bob

j'ai été très favorablement impressionné par "An Introduction to Gödel's Theorems" de Peter Smith qui est de la très bonne vulgarisation, sachant glisser sur les technicités trop rasantes tout en mettant en relief les difficultés. La curiosité de ce livre est qu'il fait partie de la collection "Cambridge Introductions to Philosophy" : c'est en principe un livre de vulgarisation destiné à un public de philosophes, disons que ses lecteurs ne doivent pas ressembler aux philosophes qui dissertent dans les pages "Débats" de notre presse nationale.

Je recommande chaudement (et recommande aussi la lecture et relecture de ce blog, cela va sans dire).

Ruxor (2016-11-29T13:34:44Z)

@SM: On peut au moins trouver moyen d'introduire le vocabulaire topologique en calculabilité en parlant de calculabilité synthétique (en logique intuitionniste) et/ou de topoï (le topos effectif fournit un modèle de la calculabilité synthétique, et il y a toutes sortes de notions de topologie qu'on peut formuler pour les topoï). Voir par exemple l'article d'Andrej Bauer, "First Steps in Synthetic Computability Theory" (2006), qui est une bonne introduction à la calculabilité synthétique, et notamment la section 3.5 intitulée "the topological view" : on peut considérer les parties récursivement énumérables de ℕ comme les ouverts d'une topologie (ce n'en est pas une au sens classique, mais ç'en est une dans le cadre de la calculabilité synthétique) : dans ces conditions, il n'est pas vrai que ℕ soit connexe (on peut bien le partitionner en deux ouverts non triviaux, par exemple {0} et son complémentaire), mais l'existence de deux ensembles récursivement énumérables non récursivement séparables signifie qu'il existe deux ouverts disjoints qu'on ne peut pas élargir en une partition de ℕ en deux ouverts. L'article de Bauer relie aussi le théorème de Rice à la connexité de l'ensemble des valeurs de vérité « semi-calculables », mais je ne sais pas si ça a un rapport avec ce que je raconte.

@Bob: Concernant la logique, j'ai entendu beaucoup de bien sur les bouquins de Smullyan, même si je n'ai pas vérifié moi-même. Il y a aussi deux livres de Franzén qui sont intéressants : l'un sur le théorème de Gödel, qui est de la vulgarisation bien faite (mais évidemment il ne va pas très loin), l'autre sur l'inépuisabilité (inexhaustibility), qui est moins de la vulgarisation (mais ça reste très accessible) ; en revanche, ses notations sont pénibles (notamment le fait d'utiliser le signe ⊃ pour l'implication, je trouve ça vraiment difficile à supporter).

Bob (2016-11-29T11:23:28Z)

Ce blog est le seul endroit où l'on peut lire ce genre de discussions sur la calculabilité et la logique, et qui fasse preuve d'un effort tout particulier pour les rendre accessibles au néophyte.

Je crois que la phrase ci-dessus est vraie, mais si elle ne l'est pas, et qu'il est possible de le prouver, je serais intéressé par une preuve constructive :)

SM (2016-11-29T11:16:17Z)

Voici une "question" que je me pose depuis quelque temps. De mémoire (faillible), il ne me semble pas l'avoir déjà posée sur ce blog, donc c'est parti…

Le paradoxe du barbier qui s'incarne chez Gödel a une saveur point fixe, et il me semble que le formalisme point fixe derrière est bien développé et connu. Par ailleurs, Gödel incomplétude dit que la répartition des énoncés en théorèmes et antithéorèmes (deux ensembles clos par déduction) n'est pas une partition (intersection non-vide dans le cas contradictoire, complémentaire de l'union non-vide sinon).

Je trouve qu'il y a là de la connexité qui semble vouloir montrer son nez sous deux déguisements différents : point fixe <-> valeur intermédiaire <-> connexité d'une part, et d'autre part connexité <=> "quand on veut répartir les points en deux ensembles ouverts (clos par prise de voisinage infinitésimal de chacun de leurs points), ça ne forme pas une partition".

Le mot "inséparabilité" dans le titre aussi évoque la connexité, d'ailleurs.

Que cela t'évoque-t-il ?


You can post a comment using the following fields:
Name or nick (mandatory):
Web site URL (optional):
Email address (optional, will not appear):
Identifier phrase (optional, see below):
Attempt to remember the values above?
The comment itself (mandatory):

Optional message for moderator (hidden to others):

Spam protection: please enter below the following signs in reverse order: 424817


Recent comments