Article ID Journal Published Year Pages File Type
431074 The Journal of Logic and Algebraic Programming 2008 23 Pages PDF
Abstract

We generalize to abstract many-sorted algebras the classical proof-theoretic result due to Parsons, Mints and Takeuti that an assertion (where P is ), provable in Peano arithmetic with induction, has a primitive recursive selection function. This involves a corresponding generalization to such algebras of the notion of primitive recursiveness. The main difficulty encountered in carrying out this generalization turns out to be the fact that equality over these algebras may not be computable, and hence atomic formulas in their signatures may not be decidable. The solution given here is to develop an appropriate concept of realizability of existential assertions over such algebras, generalized to realizability of sequents of existential assertions. In this way, the results can be seen to hold for classical proof systems.This investigation may give some insight into the relationship between specifiability and computability for data types such as the reals, where the atomic formulas, i.e., equations between terms of type real, are not computable.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics