| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 6424814 | Annals of Pure and Applied Logic | 2012 | 13 Pages |
Abstract
Relying on the extension of the bounded functional interpretation to bar recursive functionals of finite type, we prove that the scheme of bar induction has a bounded functional interpretation via bar recursors. As a consequence, the axiom of dependent choices also has a bounded functional interpretation.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
PatrÃcia Engrácia,