### Abstract

Following Aehlig [3], we consider a hierarchy F^{p} = {F^{p} _{n}}_{n∈ℕ} of parameter-free subsystems of System F, where each F^{p} _{n} corresponds to ID_{n}, the theory of n-times iterated inductive definitions (thus our F^{p} _{n} corresponds to the n + 1th system of [3]). We here present two proofs of strong normalization for F^{p} _{n}, which are directly formalizable with inductive definitions. The first one, based on the Joachimski-Matthes method, can be fully formalized in IDn+1. This provides a tight upper bound on the complexity of the normalization theorem for System F^{p} _{n}. The second one, based on the Gödel-Tait method, can be locally formalized in IDn. This provides a direct proof to the known result that the representable functions in F^{p} _{n} are provably total in IDn. In both cases, Buchholz' Ω-rule plays a central role.

Original language | English |
---|---|

Title of host publication | 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 |

Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |

Volume | 52 |

ISBN (Electronic) | 9783959770101 |

DOIs | |

Publication status | Published - 2016 Jun 1 |

Event | 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal Duration: 2016 Jun 22 → 2016 Jun 26 |

### Other

Other | 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 |
---|---|

Country | Portugal |

City | Porto |

Period | 16/6/22 → 16/6/26 |

### Keywords

- Computability predicate
- Infinitary proof theory
- Polymorphic lambda calculus
- Strong normalization

### ASJC Scopus subject areas

- Software

### Cite this

*1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016*(Vol. 52). [5] Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2016.5