We present a proof (of the main parts of which there is a formal version, checked with the Isabelle proof assistant) that, for a G3-style calculus covering all of intuitionistic zero-order logic, with an associated term calculus, and with a particular strongly normalising and confluent system of cut-reduction rules, every reduction step has, as its natural deduction translation, a sequence of zero or more reduction steps (detour reductions, permutation reductions or simplifications). This complements and (we believe) clarifies earlier work by (e.g.) Zucker and Pottinger on a question raised in 1971 by Kreisel.
CITATION STYLE
Dyckhoff, R. (2015). Cut Elimination, Substitution and Normalisation. In Outstanding Contributions to Logic (Vol. 7, pp. 163–187). Springer. https://doi.org/10.1007/978-3-319-11041-7_7
Mendeley helps you to discover research relevant for your work.