Créations logiques pour un système imprédicatif dans une méta-théorie prédicative

Les relations logiques pour les langages imprédicatifs comme le système F semblent s'appuyer de manière critique sur l'imprédicativité de la logique ambiante. Plus précisément, l'interprétation du forall-type sera définie en termes de toutes les relations typées. Dans un système imprédicatif (comme CiC / Coq) c'est bien, mais cela semble impossible dans un système prédicatif (comme Agda).

Comment cela peut-il être fait? Par exemple, comment prouveriez-vous la normalisation du système F à Agda? Devez-vous construire votre propre univers imprédicatif?

lo.logic pl.programming-languages type-theory automated-theorem-proving Max nouveau
la source

Réponses:

En général, ce que nous appelons habituellement l' argument des relations logiques n'est pas vraiment lié à l'imprédicativité: l'idée principale est simplement d'interpréter les termes dans une algèbre abstraite , et de représenter les types comme une relation ( -ary) . $\cal A$ $n$ $R \subseteq \cal A^n$

$\lambda$

$\mathrm{PA}_2$

Cependant, il est instructif de déterminer exactement où la preuve se passe mal à Agda. Cela se produit en effet lorsque vous essayez de définir l'interprétation des relations logiques de la quantification imprédicative. Cependant, l'interprétation des connecteurs non imprédicatifs (y compris la quantification "dépendante") est casher dans une théorie comme Agda.

cody
la source

Oh vraiment? Vous ne pouvez pas prouver que le système F se normalise dans Agda? Avez-vous une citation pour cela?

Max Nouveau

@MaxNew: C'est en fait assez difficile à trouver une citation. Le plus proche que je puisse trouver est La force de certaines théories de type Martin-Löf qui règle définitivement la question d'une théorie prédicative avec un seul univers et une sorte d'induction. Mais Agda a la récursion d'induction terrifiante qui la rend beaucoup plus puissante.

cody

Je dois ajouter cependant que la récursion d'induction est connue pour être plus faible que la quantification imprédicative dans certains cas, comme cela est bien expliqué ici: fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html

cody

@cody Malheureusement, le lien ne fonctionne plus. Pouvez-vous retrouver ce contenu? Connaissez-vous de nouvelles publications dans le domaine de la formalisation de l'imprédicativité?

Łukasz Lew