[FOM] Another pair of historical queries ...

[Peter Smith]

OK, OK, I know this hardly cutting-edge stuff, but I was wondering ...

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].

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.]

c) I assume whoever first saw (b) also saw you could put together (a) and 
(b) to show suff. strong. etc. theories are negation-incomplete. Is that 
right?

Cheers -- and thanks in advance!

Peter S. 

-- 
Dr Peter Smith: Faculty of Philosophy, University of Cambridge
www.logicbook.net | www.godelbook.net
--
http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/   
(for the "LaTeX for Logicians" page)