Home
Scholarly Works
Primitive Recursive Selection Functions over...
Conference

Primitive Recursive Selection Functions over Abstract Algebras

Abstract

We generalise to abstract many-sorted algebras the classical proof-theoretic result due to Parsons and Mints that an assertion $${\forall} x {\exists} y {\it P}(x,y)$$ (where P is ∑$$^{\rm 0}_{\rm 1}$$), provable in Peano arithmetic with ∑$$^{\rm 0}_{\rm 1}$$ induction, has a primitive recursive selection function. This involves a corresponding generalisation to such algebras of the notion of primitive recursiveness. The main difficulty encountered in carrying out this generalisation turns out to be the fact that equality over these algebras may not be computable, and hence atomic formulae in their signatures may not be decidable. The solution given here is to develop an appropriate concept of realisability of existential assertions over such algebras, and to work in an intuitionistic proof system. This investigation gives some insight into the relationship between verifiable specifications and computability on topological data types such as the reals, where the atomic formulae, i.e., equations between terms of type real, are not computable.

Authors

Zucker JI

Series

Lecture Notes in Computer Science

Volume

3988

Pagination

pp. 595-606

Publisher

Springer Nature

Publication Date

January 1, 2006

DOI

10.1007/11780342_61

Conference proceedings

Lecture Notes in Computer Science

ISSN

0302-9743

Labels

View published work (Non-McMaster Users)

Contact the Experts team