🚀 go-pugleaf

In article <26879@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:

|> However, if you want to use non-eliminable definitions, you need to be
|> more careful about them.  I propose that being "more careful" involves
|> the following steps: (1) make a notation to distinguish
|> definitions from other sorts of predicates.  A rule that allows the
|> introduction of a definition must be prevented from introducing
|> arbitrary equalities.  (2) make rules to introduce definitions.  And
|> either (2) introduces only "safe" definitions, or (3) make rules to
|> prevent unsave definitions from having an effect.

First, a "non-eliminable definition" is not really a definition, but
this may be regarded as a simple terminological issue.  It's been a *long*
time since I looked at this stuff, but I took some time over the weekend
to skim over appropriate sections in some musty old books of mine.
What I wonder mostly is whether what you are trying to do hasn't been
done before, and with substantially more precision that your ideas
currently have.

The general theory of definition is covered explicitly in a
number of places:

	_Introduction to Logic_ by Patrick Suppes
	(a chapter is devoted to definition)

	_Mathematical Logic_ by P. Rosenbloom
	(very precise formal criteria are given for definitions)

	_Foundations of Set Theory_ by Frankel and Bar-Hillel
	(the theory of definition and how this may need to be
	modified in non-standard logics is treated in several
	places)

	_Philosophy of Logic_ by Quine
	(a more informal approach, including a discussion of
	"recursive definitions")

There appears to be unanimity in considering "non-eliminable defintions"
*not* to be definitions.  This attitude even seems to be taken in

	_Grundlagen der Mathematik_, vol. II by Hilbert and Bernays

although I have to confess that my German is seriously rusty.

Perhaps the fullest treatment of definitions is to be found in the
writings of Lesniewski -- particularly the theory of definition in
non-standard systems.  Lesniewski appears to have begun the practice
of referring to recursive definitions as "pseudo-definitions", and
this practice became well established in the literature.

It has been a *long* time since I read Liesniewski.  The most accessible
treatment is in

	_The Logical Systems of Lesniewski_, by Eugene Luchei

and this not something the faint of heart should approach.  It looks
to me (via some quick skimming and some fragmentary memories of the
days when I actually understood this stuff) that the approach taken by
Lesniewski in the systems of Ontology and Mereology is perhaps quite
similar to what you are suggesting.  You might profit from looking at
this if you can muster the energy required to fathom the *very*
different perspective that Lesniewski brings to formal systems.  I
believe that you might find Lesniewski's approach via semantic categories
and the way in which his systems blur or eliminate the object language/
metalanguage distinction to be interesting.

	
|> X := E is not really a relation since it behaves in some ways like a
|> quantifier.  Specifically, X is a varialbe of quantification in E just
|> as it is in Forall X.E.  A more general notation for definitions would
|> be "Def X . X = E" to bring out the similarity to a quantifier, or
|> even more generally, "Def X . F(X)" where F(X) is any formula.  This
|> generalized mechanism for definition needs a generalized axiom of
|> definition:
|> 
|>   (Def X . F(X)) /\ (Exist! X . F(X)) => F(X)
|> 
|> And notice that while X is bound by an outer quantifier in the first
|> and second F(X), it is free in the last one.  The interpretation I
|> intend is that in the last F(X), X names the object that has been
|> uniquely specified by F(X), and that all that is known about the
|> object named by X is that F(X).

This appears to be the introduction of yet more unexplained notation
in order to explain the previous set of unexplained notation.  A lot
can be done with variable binding operators (vide Scott).   But each
such operator needs a precise syntax and semantics to be intelligible.

The above looks very much like

	x = IxF(x) ^ \/y/\x(x = y <-> F(x)) -> F(x)

	(If x is the thing which is F and exactly one thing
	is F, then x is F.)

	[where 'I' is used as the definite description operator]

which is in fact a *theorem* of the Theory I in

	"A Free Logic with Intensions as Possible Values of Terms"
	G. H. Merrill, _Journal of Philosophical Logic_ 4 (1975)
	pp. 293-326.

I take it that you don't want a definition to, by itself, imply
the existence of the thing defined.  Theory I accomodates this.
For example,

	x = IxF(x) -> \/xF(x)

	x = IxF(x) -> F(x)

are *not* valid in Theory I.
-- 
Gary H. Merrill  [Principal Systems Developer, C Compiler Development]
SAS Institute Inc. / SAS Campus Dr. / Cary, NC  27513 / (919) 677-8000
sasghm@theseus.unx.sas.com ... !mcnc!sas!sasghm