From hierarchies to well-foundedness |
| |
Authors: | Dandolo Flumini Kentaro Sato |
| |
Institution: | 1. School of Engineering, Zurich University of Applied Sciences, Technikumstrasse 9, 8400, Winterthur, Switzerland 2. Institut für Informatik und angewandte Mathematik, Universit?t Bern, Neubrückstrasse 10, 3012, Bern, Switzerland
|
| |
Abstract: | We highlight that the connection of well-foundedness and recursive definitions is more than just convenience. While the consequences of making well-foundedness a sufficient condition for the existence of hierarchies (of various complexity) have been extensively studied, we point out that (if parameters are allowed) well-foundedness is a necessary condition for the existence of hierarchies e.g. that even in an intuitionistic setting \({(\Pi_1^0-\mathsf{CA}_0)_\alpha \vdash \mathsf{wf}(\alpha)\, {\rm where}\, (\Pi_1^0-\mathsf{CA}_0)_\alpha}\) stands for the iteration of \({\Pi^0_1}\) comprehension (with parameters) along some ordinal \({\alpha}\) and \({\mathsf{wf}(\alpha)}\) stands for the well-foundedness of \({\alpha}\) . |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|