Abstract

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 notion concerns formal systems characterized by calculi with the following properties: any proof of a formula such as A ∨ B ) contains sufficient information to build up a proof of A or a proof of B for some term t). On the other hand, the second notion takes into account the same properties only for A ∨ B, ∃xA and t closed. Our treatment allows us to analyze both “weak” systems and “powerful” ones , 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 , yet satisfying the disjunction property and the explicit definability property