A Note on Goodman's Theorem |
| |
| Authors: | Kohlenbach Ulrich |
| |
| Affiliation: | (1) Department of Computer Science, University of Aarhus, Ny Munkegade 540, DK-8000 Aarhus C, Denmark |
| |
| Abstract: | Goodman's theorem states that intuitionistic arithmetic in all finite types plus full choice, HA + AC, is conservative over first-order intuitionistic arithmetic HA. We show that this result does not extend to various subsystems of HA, HA with restricted induction. |
| |
| Keywords: | Goodman's theorem intuitionistic arithmetic axiom of choice restricted induction |
| 本文献已被 SpringerLink 等数据库收录！ |
|
