On Uniformly Constructive and Semiconstructive Formal Systems

We propose a formalization of two notions of uniformly constructive formal system, we call uniform e-constructivity and uniform r-constructivity. On an intuitive ground, the first (extended) notion concerns formal systems characterized by calculi with the following properties: any proof of a formula such as A {vee} B (of a formula such as xA(x)) contains sufficient information to build up a proof of A or a proof of B (respectively, a proof of A(t) for some term t). On the other hand, the second (restricted) notion takes into account the same properties only for A {vee} B, xA(x) and t closed. Our treatment allows us to analyze both "weak" systems (containing only purely logical principles or, at most, weak mathematical axioms) and "powerful" ones (comparable with Intuitionistic Arithmetic or extensions of it), and exceeds the class of intuitionistic systems, as well as the class of systems for which normalization or cut-elimination theorems can be stated; moreover, it allows us to tackle systems to which the variants of recursive realizability interpretation most known in literature are not applicable. We also introduce a weaker notion of uniformly semiconstructive formal system, requiring classical logic to complete the "constructive content" involved in its proofs. We give examples of uniformly constructive and uniformly semiconstructive systems. Finally, we provide an example of a system which is not uniformly constructive (more than this, not uniformly semiconstructive), yet satisfying the disjunction property and the explicit definability property.