Analysis of Case Splitting in an Arithmetical System

Abstract

Investigations in this paper concern the analysis of case splitting in an arithmetical system. It is shown that the case splitting can be done according to a thicker class of formulas (quantifier-free formulas) instead of decidable formulas. The latter includes the class of quantifier-free formulas. Some approaches to the case splitting, promoted by other authors, have been investigated, and some corrections concerning the selection of quantifier-free formulas instead of decidable formulas have been done. According to these corrections, a new derivation of case splitting is suggested