Logical Approaches to Computational Barriers

Primitive Recursive Selection Functions over Abstract Algebras

Speaker:
| Jeffery Zucker |

Slot: |
Array, 10:50-11:10, 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
&Sigma^{0}_{1}),
provable in Peano

arithmetic with
&Sigma^{0}_{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 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 |