Some results on cut-elimination, provable well-orderings, induction and reflection

https://doi.org/10.1016/S0168-0072(98)00020-7Get rights and content
Under an Elsevier user license
open archive

Abstract

We gather the following miscellaneous results in proof theory from the attic.

  • 1.

    1. A provably well-founded elementary ordering admits an elementary order preserving map.

  • 2.

    2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21(X).

  • 3.

    3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.

  • 4.

    4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.

  • 5.

    5. Intuitionistic fixed point theories which are conservative extensions of HA.

  • 6.

    6. Proof theoretic strengths of classical fixed points theories.

  • 7.

    7. An equivalence between transfinite induction rule and iterated reflection schema over n.

  • 8.

    8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.

Each section can be read separately in principle.

MSC

03B25
03D15
03D20
03F05
03F20
03F30
03F35
03F50
68Q42

Keywords

Cut-elimination
Induction
Fixed points
Reflection principles

Cited by (0)

The title has been changed following a referee's suggestion from the old one, ‘From the Attic’.