Re: [ontolog-forum] PROF Swartz ON DEFINITIONS

[Alex Shkotin <alex.shkotin@xxxxxxxxx>]

Chris,

you are right:

- I should be more careful using FOL term abbreviation. It should be "In First order language  to get definition..." or even "In First order language with definition feature to get definition...".

- and we do need theorem of existence and uniqueness. 
This is why I have mentioned transitive closure: If we keep in mind that systems we describe are algebraic systems, then in set theory (as you mentioned) we may prove that for that kind of models we do have definition.

- and in FOL we do can only introduce an axiom 
R_(x,y) <-> R(x,y) or there_exists z such_that R_(x,z) and R(z,y)
as representative of our definition.

and anyway may I summarize that definition is more then just axiom;-)
Even context of "definition" may be beyond just language (and logic) - may be we need to keep in mind referent itself or at least class of models (math speaking).

For ex- if an infinite in one direction, properly directed chain  (node -> node ->...) is an existing thing for us then "+", "*" arithmetic operations has recursive definition on it.

Alex

2010/9/20 Christopher Menzel <cmenzel@xxxxxxxx>

On Sep 20, 2010, at 5:29 AM, Alex Shkotin wrote:

In FOL to get definition (for R_ in my case) we need additional clause, just as Doug has written.
And putting all that clauses together we do get recursive definition for R_
(as it is written by Prof. Swartz at http://www.sfu.ca/philosophy/swartz/definitions.htm#part5.6):

R_(x,y) =_df (R(x,y) or there_exists z such_that R_(x,z) and R(z,y))

Actually, recursive definitions are not proper definitions in FOL, so the "=_df" is in fact misplaced here (Prof Swartz's use of the notation notwithstanding).  In a genuine definition, the defined term is in a certain (rigorous) sense dispensable; it is a convenience that one could, in principle, do without.  Unlike a recursive definition, then, in a genuine definition, the defined _expression_ cannot occur in the definiens.

A recursive definition, by contrast, asserts that a certain unique function or relation (i.e., in set theoretic terms, a certain set of ordered n-tuples) satisfying the definition exists.  As the paradoxes of set theory taught us, one cannot simply go about asserting the existence of sets, functions, and relations willy-nilly.  Hence, recursive definitions in general must be justified by a theorem to the effect that the functions or relations asserted to exist by such definitions do exist.  (This is, unsurprisingly, called the "definition by recursion" theorem, which was first proved by von Neumann (who also first recognized the need for such a proof) in the 1920s and generalized by Tarski in the 1950s).

From a formal perspective, then, both ordinary definitions and recursive definitions in general are best thought of as axioms that one adds to an existing theory that introduce one's new function/relation symbols.  In the case of ordinary definitions, that such axioms are "safe" is demonstrated by showing  that anything that can be proved using the defined expressions could be proved by replacing the defined expressions with their definitions.*  In the case of recursive definitions, such axioms are guaranteed to be "safe" by the definition by recursion theorem, which, once again, shows that the functions/relations that the axioms explicitly name and characterize do, in fact, exist.

to say frankly I still doubt - may be we need to keep in mind something like "smallest transitive relation" like in "In mathematics, the transitive closure of a binary relation R on a set X is the smallest transitive relation on X that contains R."

Good example.  That there exists a unique, smallest such set for every binary relation is a nontrivial theorem of set theory.

Chris Menzel

*To count as genuine definitions, one also has to prove that the new axioms are "conservative", i.e., that they don't permit one to prove theorems not involving the new symbols that one couldn't prove before.

_________________________________________________________________
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
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx
 

_________________________________________________________________
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
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (01)