Theories very close to PA where Kreisel's conjecture is false

We give four examples of theories in which Kreisel's Conjecture is false: (1) the theory PA(-) obtained by adding a function symbol minus, '-', to the language of PA, and the axiom for all x for all y for all z (x - y = z) equivalent to (x = y + z boolean OR(x < y boolean AND z 0)); (2) the theory-E of integers; (3) the theory PA (q) obtained by adding a function symbol q (of arity >= 1) to PA, assuming nothing about q; (4) the theory PA (N) containing a unary predicate N(x) meaning 'x is a natural number'. In Section 6 we suggest a counterexample to the so called Sharpened Kreisel's Conjecture.