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

[William Frank <williamf.frank@xxxxxxxxx>]

All that you say below is correct, Chris, 

so, perhaps we can add another important observation about definitions versus primitives, as a correlary to what John Sowa was saying about the importance of the language used in an ontology:

"what terms can be defined versus those that are primitive depends in part on the power of the language in which the ontology is expressed"


this is why, in my original posting on this, I tried to be careful to say:

an axiomatic arithmetic for .. 

instead of 

the axiomatic arithmetic for .. 

and to say 

might be used in a definition of '+", 

instead of 

is used in a definition of '+'

emphasizing that there are a large number of different axiomatizations possible for a given theory, even in the same language, (for example, we could use '+' and '1" as primitives, and instead define "successor") as well as emphasizing that what can be said depends on the language it is to be said in.


I know neither of us intends to use this forum to debate matters of axiomatic arithmetic, but only to see what they might teach us about ontology.   I believe that an ontology is often usefully viewed as a kind
 of formal theory, so I believe that all this discussion applies to ontologies. And, axiomatic arithemetic happens to be an extremely well-studied example. 

Best

Wm

On Thu, Mar 1, 2012 at 2:00 PM, Christopher Menzel <cmenzel@xxxxxxxx> wrote:

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
 

-- 
William Frank

413/376-8167

_________________________________________________________________
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)