[FOM] Another pair of historical queries ...

[Neil Tennant]

On 8 Dec 2004, Peter Smith wrote:

> a) Who first noticed that a consistent, axiomatized, negation-complete 
> formal theory is decidable [decidable by the idiot brute force method of 
> enumerating theorems and seeing what turns up].

A. Janiczak, "A remark concerning the decidability of complete theories',
Journal of Symbolic Logic 15, 1950, pp. 277-9.
 
> b) Who first saw that you could show that a `sufficiently strong' 
> axiomatized formal theory T of arithmetic is undecidable [where 
> `sufficiently strong' is defined in terms of the **intuitive** notion of 
> decidability, and the proof proceeds by enumerating open wffs A_n(x) and 
> defining a diagonal property D, where n is D iff T |- not-A_n(n), etc. 
> etc.]

Probably one of Tarski, Mostowski and Robinson---of "Undecidable Theories"
fame?

Neil Tennant