lim+, delta+, and Non-Permutability of beta-Steps
arXiv:0902.3635 · doi:10.1016/j.jsc.2011.12.035
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.
ii + 36 pages
References in corpus (2)
Cited by in corpus (5)
- Hilbert's epsilon as an Operator of Indefinite Committed Choice
- A Simplified and Improved Free-Variable Framework for Hilbert's epsilon as an Operator of Indefinite Committed Choice
- Automation of Mathematical Induction as part of the History of Logic
- Progress in Computer-Assisted Inductive Theorem Proving by Human-Orientedness and Descente Infinie?
- Herbrand's Fundamental Theorem: The Historical Facts and their Streamlining