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

Concernant la saveur topologique des résultats de Gödel, on peut poser T l'ensemble des théories non-contradictoires et suffisamment riches pour encoder l'arithmétique. On prend alors la topologie sur T engendrée par les voisinages ouverts élémentaire suivants : pour chaque axiomatique énumérable par une machine de Turing vérifiée par une théorie t, on pose comme voisinage de t l'ensemble de toutes les théories t' dans T qui vérifient aussi cette axiomatique. Le théorème d'incomplétude dit alors que T n'a aucun point isolé.

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

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.

> 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?

C'était super !

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

@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 ?

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

Excellent, merci !

Merci beaucoup !!

@ 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).

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 :)

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 ?