ontolog-forum
[Top] [All Lists]

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

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Wed, 29 Feb 2012 10:30:35 +0100
Message-id: <8F27F393-1B02-4ED0-AEA1-E78A2D8F584C@xxxxxxxx>
Am Feb 28, 2012 um 7:44 PM schrieb William Frank:
It seems to me that beyond their being a *parallel* in mathematics,
the concepts of term, primitive term, and construct (or open
_expression_) come from and are standard in formal mathematics and
model theory, since Tarski's "introduction to logic and scientific
method", continuing today, and applied carefully in formal renditions
of everything from arithmetic to set theory to category theory, and in
such collections as "Explanation and Proof in Mathematics."

For example, in an axiomatic arithmetic for the natural numbers, "0"
and "successor" are usually primitive terms, while "+" and "1" are usually
introduced as defined terms,

1 might have the definition
 1 = successor (0)

and the open sentence

x+successor(y) = successor(x+y)

might be one of the constructs used in the definition of "+"

This isn't quite correct. It is impossible to define addition in terms of zero and successor. The reason for this, in a nutshell, is that the addition symbol is not eliminable; given the axioms for addition along with the axioms for zero and successor, you can "say" things that you cannot say in terms of the axioms for zero and successor alone; likewise multiplication vis-á-vis zero, successor, and addition. "x+s(y) = s(x+y)" is one of the standard axioms for the primitive operator "+" (the other, of course, being "x + 0 = x") but it is not a definition of "+" (or part of one). By contrast, "1 = s(0)" is a legitimate definition, as anything you can say using "1" can be said just as well (i.e., provably) using "s(0)" instead.

Granted, the ontology community often uses the word "definition" in reference to the axiomatization of a primitive concept — an understandable usage, of course, as axioms do "define" a primitive in the sense of characterizing its logical properties. But this usage runs two importantly distinct notions together and, as a consequence, muddies the distinction between primitive and defined vocabulary.

Chris Menzel

*****

For those who are interested in this sort of thing, here's how the theory of definitions works a bit more exactly: Suppose we have a theory T in a language L and that we wish to define a new _expression_ ε. Let Lε be the result of adding ε to L. A definition for ε is then actually a new axiom D that we add to T, resulting in a new theory T+D in the extended language Lε. In order for the purported definition to pass muster, the defined _expression_ must be eliminable in the following sense: For any sentence φ of language Lε that involves our defined _expression_ ε, there must a sentence ψ of the original language L that is provably equivalent to φ in T+D. Moreover, the addition of D to T must not enable us to prove anything in the original language L that we couldn't already prove in T alone. (This condition on definitions is known as conservativeness.) Thus, if in fact T+D ⊢ φ, where φ involves the defined _expression_ ε, if our definition D is legitimate, then, where ψ is our sentence of L such that T+D ⊢ φ ↔ ψ, it follows that T ⊢ ψ. The definition of ε thus doesn't allow us to "say" (or, in particular, prove) anything in terms of the definition that (but perhaps for economy of _expression_) we couldn't just as well have said (or proved) without it.

For the special case of the definition of "1", let ε be "1", let L be the usual language {0.s,+,•} of number theory and let T be Peano Arithmetic (PA). Then where φ is any sentence of L involving "1", and ψ is the result of replacing every occurrence of "1" in φ with "s(0)", then by eliminability we have PA+"1 = s(0)" ⊢ φ ↔ ψ and, moreover, by conservativeness, if in fact PA+"1 = s(0)" ⊢ φ, then PA ⊢ ψ.



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