Tyrrell_McAllister comments on Notion of Preference in Ambient Control - Less Wrong

14 Post author: Vladimir_Nesov 07 October 2010 09:21PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (45)

You are viewing a single comment's thread.

Comment author: Tyrrell_McAllister 08 October 2010 12:43:46AM *  1 point [-]

The new symbols extend the language, while their definitions, obtained from agent and world programs respectively by standard methods of defining recursively enumerable functions, extend the theory.

I haven't yet read beyond this point, but this is a kind of confusing thing to write. Definitions can't extend a theory, because they don't give you new theorems. My assumption is that you will add axioms that incorporate the new symbols, and the axioms will extend the theory.

Comment author: Vladimir_Nesov 08 October 2010 07:02:22AM 3 points [-]

Definitions can't extend a theory, because they don't give you new theorems.

A conservative extension of a language/theory doesn't introduce new theorems in the old language, but could introduce new theorems that make use of new symbols, although in the case of extension by definitions, all new theorems can also be expressed in the smaller (original) language and would be the theorems of original theory.

Comment author: Tyrrell_McAllister 08 October 2010 05:15:30PM 1 point [-]

Okay, thanks. I didn't know that adding certain kinds of axioms was called "extension by definitions".

Comment author: Will_Sawin 08 October 2010 01:23:27AM 0 points [-]

Some axioms are definitions.

Previous theorem: All unmarried men are not married New definition: "Bachelor" means "unmarried man" New theorem: All bachelors are unmarried men.

I'm pretty sure that's what he means. Hopefully clarified, if not made perfectly in accord with standard definitions.

Comment author: Tyrrell_McAllister 08 October 2010 03:21:44AM 1 point [-]

I'm pretty sure that's what he means.

I think that he means something analogous to the way that we can add some axioms involving the symbol "+" to the Peano axioms, and then show in second-order logic that the new axioms define addition uniquely.