[FOM] Another pair of historical queries ...
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!
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