[FOM] Another pair of historical queries ...

Peter Smith ps218 at cam.ac.uk
Wed Dec 8 07:18:19 EST 2004

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. 

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 

Cheers -- and thanks in advance!

Peter S. 

Dr Peter Smith: Faculty of Philosophy, University of Cambridge
www.logicbook.net | www.godelbook.net
(for the "LaTeX for Logicians" page) 

More information about the FOM mailing list