lim+, delta+, and Non-Permutability of beta-Steps

TL;DR

This paper presents a formal proof example of the (lim+) theorem, highlighting the non-permutability of beta-steps and delta+-steps in certain logical calculi, and discusses the importance of step order in proof search.

Contribution

It demonstrates the non-permutability of beta-steps and delta+-steps in a formal proof, emphasizing the significance of step order in logical calculi.

Findings

Non-permutability of beta-steps and delta+-steps shown in a formal proof.

Order of beta-steps critically affects proof search in certain calculi.

Delta++-rule mitigates non-permutability issues.

Abstract

Using a human-oriented formal example proof of the (lim+) theorem, i.e. that the sum of limits is the limit of the sum, which is of value for reference on its own, we exhibit a non-permutability of beta-steps and delta+-steps (according to Smullyan's classification), which is not visible with non-liberalized delta-rules and not serious with further liberalized delta-rules, such as the delta++-rule. Besides a careful presentation of the search for a proof of (lim+) with several pedagogical intentions, the main subject is to explain why the order of beta-steps plays such a practically important role in some calculi.