No-counterexample interpretation et sp\'{e}cification des th\'{e}or\`{e}mes de l'arithm\'{e}tique
逻辑
2007-05-23 v1
摘要
This paper presents two different ways of extracting the computational content of formal proofs in arithmetic. The first one corresponds to Kreisel's No-counterexample Interpretation. based on Ackermann consistency proof. We show the link with recent work by Krivine on classical realizability. Finally, we discuss the various degrees of modularity of both approaches.
引用
@article{arxiv.math/0501476,
title = {No-counterexample interpretation et sp\'{e}cification des th\'{e}or\`{e}mes de l'arithm\'{e}tique},
author = {Denis Bonnay},
journal= {arXiv preprint arXiv:math/0501476},
year = {2007}
}
备注
in french