[Top] [All Lists]

Re: [ontolog-forum] Constructs, primitives, terms

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Thu, 1 Mar 2012 20:00:40 +0100
Message-id: <CAO_JD6Mm4Oq2ij8CGS5CcCDFt3zGy=3+GXgNXA5gHW-x0uDDHA@xxxxxxxxxxxxxx>
On Thu, Mar 1, 2012 at 5:50 PM, William Frank <williamf.frank@xxxxxxxxx> wrote:
...a basic feature of any defined term  is the principle of substitutability: you can always replace the defined term with its definition.

However, just to keep things accurate, this principle applies to recursive functions as well, quite simply, if a little awkwardly, when using higher order (undecidable) languages.

Yes, of course, but that's where the miscommunication is here.
Here is how it works, for addition:

1. theorem

There is exactly one function f such that f(x,y) = f(y,x), f(0,x) = x, and for every x, y (successor f(x,y) = f (x, successor(y)))

Very important to note that you are in a framework powerful enough to quantify over functions and prove the existence of recursive functions. This was missing from your original post.

2. definition

'+' means that unique function f such that …….

so, every time one encounters the symbol “+”, one replaces that symbol with the definiens: “that unique function f such that …."

thus, the principle of substitutability of defined terms with their definiens is sustained in recursive definitions

this example and its equivalents are easy to find in the literature.
so, I was most surprised to find someone saying:

"It is impossible to define addition in terms of zero and successor."

Nonetheless it is entirely true in the context I set. The context you set in your original note was "an axiomatic arithmetic for the natural numbers" which I (apparently hastily) took to mean (first-order) Peano Arithmetic (PA) — which does not quantify over functions and, in particular, is not capable of proving your theorem above. I was explicit about this in the more formal exposition of my point, which I put below my more informal message. And, in the context of PA, it is indeed quite impossible to define addition in terms of zero and successor; if you take the usual recursive axioms for "+" to be a definition, the purported definition is neither eliminable nor conservative. However, as I'd intended the more informal part of my message to be self-contained, it was an expository error on my part not to make the context of my assertion more explicit when I made it.

Chris Menzel

Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)

<Prev in Thread] Current Thread [Next in Thread>