Computability in Europe 2006
Logical Approaches to Computational Barriers
|Slot:||Mon, 10:50-11:10, Faraday B (col. 2)|
We generalise to abstract many-sorted algebras the classical proof-theoretic
result due to
Parsons and Mints that an assertion   &forall x &exist yP(x,y)   (where P is &Sigma01), provable in Peano
arithmetic with &Sigma01 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 is to develop an appropriate concept
of realisability of existential assertions over such algebras. This investigation may give
some insight into the relationship between specifiability and computability for data types
such as the reals, where the atomic formulae, i.e., equations between terms of type real,
are not computable.
|websites: Arnold Beckmann||2006-05-07|