ontolog-forum
[Top] [All Lists]

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

 To: "[ontolog-forum]" Christopher Menzel Thu, 1 Mar 2012 20:00:40 +0100
 On Thu, Mar 1, 2012 at 5:50 PM, William Frank 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 definitionsthis 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) ```
 Current Thread Re: [ontolog-forum] Constructs, primitives, terms, John F. Sowa Re: [ontolog-forum] Constructs, primitives, terms, William Frank Re: [ontolog-forum] Constructs, primitives, terms, Christopher Menzel <= Re: [ontolog-forum] Constructs, primitives, terms, William Frank Re: [ontolog-forum] Constructs, primitives, terms, Patrick Cassidy Re: [ontolog-forum] Constructs, primitives, terms, Amanda Vizedom Re: [ontolog-forum] Constructs, primitives, terms, David Eddy Re: [ontolog-forum] Constructs, primitives, terms, John Bottoms Re: [ontolog-forum] Constructs, primitives, terms, Amanda Vizedom Re: [ontolog-forum] Constructs, primitives, terms, Phil Murray Re: [ontolog-forum] Constructs, primitives, terms, Amanda Vizedom Re: [ontolog-forum] Constructs, primitives, terms, John F. Sowa Re: [ontolog-forum] Constructs, primitives, terms, Ron Wheeler