Russel, There is a somewhat brief section in this article:
http://plato.stanford.edu/entries/goedel/#SpeUpThe The section gives 2 forms of the theorem, the 2nd of which is the more interesting ("theorem 6"). I came across this subject in the book "logic, logic, and logic" by Boolos. Boolos describes 1st-order logic as "practically incomplete" (complete, but astronomically slow in some cases). He also discusses astronomical differences between different first-order deduction systems. A fascinating topic. --Abram On Sat, Dec 27, 2008 at 2:55 AM, Russell Wallace <russell.wall...@gmail.com> wrote: > On Fri, Dec 26, 2008 at 11:56 PM, Abram Demski <abramdem...@gmail.com> wrote: >> That's not to say that I don't think some representations are >> fundamentally more useful than others-- for example, I know that some >> proofs are astronomically larger in 1st-order logic as compared to >> 2nd-order logic, even in domains where 1st-order logic is >> representationally sufficient. > > Do you have any online references handy for these? One of the things > I'm still trying to figure out is to just what extent it is necessary > to go to higher-order logic to make interesting statements about > program code, and this sounds like useful data. > > > ------------------------------------------- > agi > Archives: https://www.listbox.com/member/archive/303/=now > RSS Feed: https://www.listbox.com/member/archive/rss/303/ > Modify Your Subscription: https://www.listbox.com/member/?&; > Powered by Listbox: http://www.listbox.com > -- Abram Demski Public address: abram-dem...@googlegroups.com Public archive: http://groups.google.com/group/abram-demski Private address: abramdem...@gmail.com ------------------------------------------- agi Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/ Modify Your Subscription: https://www.listbox.com/member/?member_id=8660244&id_secret=123753653-47f84b Powered by Listbox: http://www.listbox.com
