<foo> simply produces <foo>in the text).
<URL: http://somewhere.tld/ >,
and it will be automatically made into a link.
(Do not try any other way or it might count as an attempt to spam.)mailto: URI,
e.g. mailto:my.email@somewhere.tld,
if you do not have a genuine Web site).
eisaru (2014-07-02T15:35:39Z)
> Bruno Barras a un travail de traduction de Coq dans IZF (qui n'est pas CZF…). Malheureusement, il n'a pas encore de documents publics qui décrive ce travail.
Faux! C'est bien caché mais déjà cité dans certains papiers donc on cherche, on cherche et…
http://www.lix.polytechnique.fr/~barras/habilitation/
Arnaud Spiwack (2014-06-19T20:53:39Z)
Dans la version d'Aczel, tu n'as plus le remplacement si tu fais une traduction par double-négation (d'où le fait qu'ajouter le tiers-exclu est infiniment plus puissant). La compréhension est, en revanche, très limitée (dans tous les cas).
Dans la version de Werner, tu as toute la compréhension. En revanche, le remplacement est très limité. Et tu peux interpréter tout Z sans axiome grâce à la double-négation.
La comparaison avec ZF est apparemment ouverte. On ne sait pas interpréter IZF(R) (avec l'axiome du remplacement plutôt que la collection) est plus faible que IZF avec collection (où la double-négation permet d'interpréter ZF). Mais on ne sait même pas si IZF(R) et IZF(C) sont équiconsistents…
Ruxor (2014-06-19T16:23:00Z)
@Arnaud Spiwack: Dans sa formulation classique, le schéma de remplacement implique le schéma de compréhension, mais il y a évidemment des variantes (dont des formulations du schéma de collection ; il faut se méfier parce qu'il y a mille et une variantes) qui ne l'impliquent pas. Le schéma de remplacement a une très grande force logique : déjà, on en a besoin pour montrer que le niveau ω·2 de la hiérarchie de von Neumann est un ensemble, et ça donne un modèle de Z (:=ZF sans remplacement), donc remplacement implique la consistance de Z, mais ce n'est qu'un tout petit bout de sa puissance. Sa grande force, c'est qu'il montre (non uniformément) que n'importe quel ensemble fini d'énoncés vrais est modélisé par un niveau de la hiérarchie de von Neumann (« lemme de réflexion »), et ça, c'est extrêmement puissant.
Bon, bref, au final, si j'ai bien suivi, la question n'est pas totalement claire : Coq sans aucun axiome supplémentaire prouve-t-il la consistance de ZFC (vue comme un énoncé arithmétique) ?
Arnaud Spiwack (2014-06-19T15:39:52Z)
Après mûres réflexions, le codage d'Aczel (aussi utilisé par Werner) nous laisse le choix entre interpréter l'axiome de remplacement/collection ou celui de compréhension. Pour avoir les deux, dans Coq, Werner utilise un axiome de description. C'est pour avoir la compréhension qu'on utilise la sorte Prop imprédicative. Après, personnellement, je n'ai jamais trop compris à quoi sert le remplacement, alors je ne trouve pas forcément ça troublant. Mais je soupçonne que le remplacement a quand-même une importante force logique (cela dit, on n'est pas limité, dans Coq, à la logique du premier ordre, et on peut interpréter une version du remplacement où, au lieu d'avoir une relation fonctionnelle, on utilise une fonction Coq. Je doute que ça compense, mais on ne sait jamais).
Le tiers-exclu, en tout cas, n'a rien à voir là-dedans. Tu peux définir en Coq le type CProp = { P:Prop | ¬¬P→P }. Presque toutes les propositions s'interpètent alors dans CProp. Les exceptions sont essentiellement l'égalité et l'accessibilité, l'impact sur la force logique de perdre ces deux proposition n'est pas clair, mais ça a l'air suffisamment anodin pour qu'il y ait des gens qui (pour d'autres raisons) ont suggéré de les enlever de Prop de toute façon. Et CProp supporte le tiers-exclu. On obtient donc un presque-Coq avec le tiers exclu dedans. Comme ni l'égalité ni l'accessibilité ne jouent un rôle dans l'interprétation de (presque) ZF, on peut se passer d'un axiome pour le tiers exclu.
Ruxor (2014-06-18T17:16:01Z)
@Arnaud Spiwack: Merci, ça éclaircit pas mal certaines choses. Juste une clarification : si on sait interpréter ZF, on sait interpréter ZFC et d'ailleurs ZFC + GCH (on construit l'univers constructible de Gödel L dans ZF, et on interprète tout énoncé en restreignant les quantificateurs à L : c'est comme ça que Gödel prouve la consistance de l'axiome du choix et de GCH). Du coup, je veux bien vérifier que j'ai compris : tu dis bien que tu penses que Coq, avec un univers mais sans supposer le tiers exclu (c'est surtout ça qui m'importe), interprète ZF(C) classique ? (Note : il suffit d'interpréter IZF, parce qu'il donne ZF sous la traduction double-négation.) Effectivement, si c'est le cas, l'axiome du tiers exclu n'est pas important dans le papier de Werner, mais alors je me demande pourquoi il l'a mis !
C'est d'ailleurs quelque chose que les livres sur l'intuitionnisme devraient souligner trois fois, parce que je me suis beaucoup embrouillé avant de comprendre ceci : si on a une théorie intuitionniste T, on peut fabriquer canoniquement deux théories classiques : (1) celle qui s'obtient en ajoutant le postulat de tiers exclu à T, et (2) celle qui s'obtient en interprétant la logique classique par la traduction double-négation de Kolmogorov-Gödel. A priori, (1) peut être beaucoup plus forte que (2), donc il ne faut pas les confondre. D'ailleurs c'est le cas pour CZF (alors que pour IZF, comme je le dis ci-dessus, c'est pareil) ; peut-être que pour Coq, c'est pareil, je n'ai pas du tout les idées claires (pour commencer, sur comment faire la traduction…).
Nick Mandatory (2014-06-18T17:15:46Z)
C'est ça que je voulais dire, et je te remercie.
Arnaud Spiwack (2014-06-18T16:10:12Z)
Notons que je suis constructiviste. Mais je fais parti de cette faction qui n'ont rien à faire de la prédicativité. Martin-Löf a un avis très tranché dessus. Mais puisqu'on parlais de Bishop au début, je ne pense pas que lui avait des scrupules (mais peut-être en aurait-il eu si il avait travaillé après les mésaventures des années 70).
Pour ce qui est de Mahlo, je pensais aux cardinaux dans ZF (par contre j'ai écrit n'importe quoi : je voulais parler de constructions inductives-récursives (pas primitives récursives… il faut que je retrouve le chemin de mon lit)). Mais après une lecture un peu plus attentive, il s'agit effectivement de quelque chose de l'ordre KP+ordinal récursivement Mahlo. I stand corrected.
Pour ce qui est des théories des types. On a donc plusieurs variétés : MLTT, CC, CIC (et encore CIC, ça désigne plusieurs théories des types)… Elles sont toutes assez différentes. (je ne pas parler en terme d'analyse ordinale, parce que je ne parle pas cette langue, malheureusement).
Le calcul des constructions c'est la plus faible de toute apparemment (je ne sais pas le faire, mais il paraît qu'on peut prouver sa cohérence dans un sous-système assez faible de HA). Mais il y a un trick: la normalisation de CC est difficile (en fait on peut la réduire à la normalisation de Fω : il y a un théorème d'effacement), ce qui fait que CC est faible, c'est qu'on ne peut rien prouver dedans. En revanche CC+0≠1, tout de suite, ça envoie (c'est plus puissant que MLTT), mais ça ne normalise plus. Au passage, CC+EM est cohérent, mais il prouve que 0=1.
Le but des vieux CIC c'est, en somme, de pouvoir montrer 0≠1. Au lieu d'utiliser des codage pour représenter les types de donnée, et on leur donne des règles d'élimination qu'on ne pouvait pas obtenir par codage. C'est plus ou moins la même chose que CC+0≠1, je crois.
Dans les versions modernes de CIC, le principe est un peu différent, on a en gros une variante de MLTT avec plus de types de données et la hiérarchie d'univers. Et on adjoint CC (en vrai une version du vieux CIC, mais où on ne peut pas prouver 0≠1) tout en bas.
Toutes les variantes de CIC sont des extensions de MLTT (généralement avec une hiérarchie d'univers) en tout cas. Et je ne vois pas particulièrement d'autre façon de tomber en dessous de PA2 à part se restreindre à la dite MLTT.
À vrai dire, si j'ai un univers, les types inductifs et une sorte Prop imprédicative, il me semble que je peux implémenter ZF (probablement pas ZFC) dans Coq.
Dans CC+0≠1, je ne saurais pas identifier un fragment non-trivial qui soit plus faible que PA2.
Après, pincée de sel, tout ça : ces histoires ne sont franchement pas ma tasse de thé (en plus je ne sais pas si ça t'avance le moins du monde…).
Ruxor (2014-06-18T15:44:13Z)
@Nick Mandatory: Si par Martinlöferies tu veux parler de la théorie des types de Martin-Löf, à part le texte de Martin-Löf vers lequel j'ai fait un lien (<URL: http://www.csie.ntu.edu.tw/~b94087/ITT.pdf >, je ne sais pas ce qu'il fait sur un site à Taïwan), il y a une description un peu informelle et plutôt pour débutants de cette théorie dans <URL: http://www.cllc.vuw.ac.nz/talk-papers/whatisit.ps >. Il y en aussi une dans l'article d'Aczel ("The Type Theoretic Interpretation of Constructive Set Theory: Choice Principles") dans le Brouwer Centenary Symposium (Troelstra & van Dalen eds., 1982). Enfin, l'article de Kamareddine et Laan, "A Correspondance between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems" (<URL: http://www.jstor.org/stable/40180289 >) contient une description de la théorie des types de Martin-Löf sur un modèle vaguement semblable à la description faite dans l'article de Barendregt que j'ai cité (et qui est lui-même très lisible).
Mais bon, même avec tout ça, je reste assez flou sur le rapport entre la théorie des types de Martin-Löf et, les différents coins du lambda-cube de Barendregt. Pourtant, les deux sont très standards, mais il ne semble pas y avoir un seul auteur qui se soit sorti les doigts du cul pour écrire clairement une comparaison !
Nick Mandatory (2014-06-18T14:05:06Z)
Et pour un matheux normal, tu connais une référence sur les Martin-Löferies ?
Ruxor (2014-06-18T12:44:09Z)
@Arnaud Spiwack: Moi aussi je pensais que la constructivité n'avait pas grand rapport avec la force logique (notamment selon l'idée un peu vague que la traduction de Dragalin-Friedman permettrait de ramener une théorie classique à une théorie intuitionniste de même force). Mais l'article de Martin-Löf que je cite au début (*The Hilbert-Brouwer controversy*) affirme clairement le contraire : pour lui, il y a un fossé que ne peut pas franchir la force logique d'une théorie qu'il considère comme constructive. Et de ce que je comprends, ce fossé se situe à peu près au niveau de la Π¹₂-compréhension côté arithmétique du second ordre, ou de la Σ₁-séparation côté théorie des ensembles à la KP (ces différentes théories sont assez bien expliquées dans l'article de Rathjen intitulé *Explicit Mathematics with Monotone Inductive Definitions: a Survey*, <URL: http://www1.maths.leeds.ac.uk/~rathjen/fest.pdf >). Ce que j'essaie de comprendre, donc, c'est comment le calcul des constructions et le calcul inductif des constructions s'articulent par rapport à ça (par exemple : quels sont les sous-systèmes du calcul des constructions inductifs qui sont en-deçà de l'arithmétique classique du second ordre pour ce qui est de la force logique ?).
Il faut faire attention avec la terminologie, aussi. Par exemple, ce qu'on appelle « Mahlo » peut être terriblement confusant : il y a les cardinaux Mahlo qu'on peut ajouter à ZF, et il y aussi les ordinaux récursivement Mahlo qu'on peut ajouter à KP, et qui sont beaucoup beaucoup plus faibles (tout cardinal régulier de ZF est récursivement inaccessible, récursivement Mahlo, récursivement faiblement compact, etc. ; et en tout cas, KP + « il existe un ordinal récursivement Mahlo » reste bien en-deçà du fossé dont parle Martin-Löf alors que ZF est bien au-delà) ; et là où ça devient très confusant, c'est qu'on peut ajouter à CZF des hypothèses qui, en présence de tiers exclu, ont la force des cardinaux Mahlo de ZF (ce sont même exactement la même chose) alors qu'en l'absence de tiers exclu, ils ont la force des ordinaux récursivement Mahlo de KP, donc on peut avoir superficiellement l'impression qu'ajouter le tiers exclu ne change rien (c'était Mahlo, ça reste Mahlo), mais c'est un sens totalement différent du mot, et en tout cas une force logique qui n'a rien à voir !
Arnaud Spiwack (2014-06-18T11:20:28Z)
Quelques remarques en vrac:
La question de la constructivité n'a pas vraiment de rapport avec la force logique des fondements. Ce qui est important c'est le comportement de la disjonction et du quantificateur existentiel (dont la démonstration doit permettre de dériver un témoin). Globalement, on pense plus en terme de "tabous" qu'en terme d'une définition positive : si on arrive à démontrer, par exemple, que toute machine de Turing termine ou ne termine pas, on aura clairement passé les bornes strictes des mathématiques constructives.
Après, il y a diverses écoles qui se bouffent plus ou moins le pif gentiment. Dont les prédicativistes, qui refusent l’existence des ensembles de parties et tout un tas d'autre joyeuseté. Cela dit, si quelqu'un te dit que les ensembles de parties ne sont pas constructifs, tu peux admettre qu'il est de mauvaise foi.
Mais ce n'est toujours pas un problème de force logique: les prédicativistes n'ont typiquement pas de soucis avec les constructions primitives récursives qui, nous explique Anton Setzer, permettent de construire des cardinaux de Mahlo.
Dans la plupart des systèmes constructifs, le principe de Markov est admissibles. C'est-à-dire que les formules Π₂ démontrables sont les mêmes qu'en supposant le tiers-exclu. Ça échoue dans CZF à cause des axiomes de la théorie (mais en choisissant un autre ensemble d'axiomes similaire, il me semble que le problème disparaît).
Un autre système où le tiers-exclu a un effet spectaculaire c'est une des variantes du CIC : y ajouter le tiers-exclu est incohérent. Cela dit, dans le cas du papier de Werner, le tiers exclu a un effet modeste.
Bruno Barras a un travail de traduction de Coq dans IZF (qui n'est pas CZF…). Malheureusement, il n'a pas encore de documents publics qui décrive ce travail.