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

[Christopher Menzel <cmenzel@xxxxxxxx>]

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)