Studia Logica 73 (1):21 - 49 (2003)
AbstractIn the 80's Pierangelo Miglioli, starting from motivations in the framework of Abstract Data Types and Program Synthesis, introduced semiconstructive theories, a family of large subsystems of classical theories that guarantee the computability of functions and predicates represented by suitable formulas. In general, the above computability results are guaranteed by algorithms based on a recursive enumeration of the theorems of the whole system. In this paper we present a family of semiconstructive systems, we call uniformly semiconstructive, that provide computational procedures only involving formulas with bounded complexity. We present several examples of uniformly semiconstructive systems containing Harrop theories, induction principles and some well-known predicate intermediate principles. Among these, we give an account of semiconstructive and uniformly semiconstructive systems which lie between Intuitionistic and Classical Arithmetic and we discuss their constructive incompatibility.
Added to PP
Historical graph of downloads
References found in this work
No references found.
Citations of this work
No citations found.
Similar books and articles
A Negationless Interpretation of Intuitionistic Theories. I.Victor N. Krivtsov - 2000 - Studia Logica 64 (1-2):323-344.
On Maximal Intermediate Predicate Constructive Logics.Alessandro Avellone, Camillo Fiorentini, Paolo Mantovani & Pierangelo Miglioli - 1996 - Studia Logica 57 (2-3):373 - 408.
Correspondence Results for Relational Proof Systems with Application to the Lambek Calculus.Wendy MacCaull & Ewa Orłlowska - 2002 - Studia Logica 71 (3):389-414.
Interpretive Praxis and Theory-Networks.L. E. E. Sangwon - 2006 - Pacific Philosophical Quarterly 87 (2):213–230.
Interpreting Classical Theories in Constructive Ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
Counting the Maximal Intermediate Constructive Logics.Mauro Ferrari & Pierangelo Miglioli - 1993 - Journal of Symbolic Logic 58 (4):1365-1401.