Re: recursive definitions and paradoxes

Thread View: sci.logic

2 messages

[T] Back to Threads [V] Tree View [G] Group Articles

2 total messages Started by David Gudeman Sat, 21 Nov 1992 01:52

#563

Author: David Gudeman
Date: Sat, 21 Nov 1992 01:52

101 lines
4858 bytes

In article  <By140L.G6z@unx.sas.com> Gary Merrill writes:
]
]"Defined formally by its usage"?? "They seemed uninteresting"?

I guess I am being too terse.  What I meant by the first statement is
that once you put down the rules for introducing definitions and the
rules for using definitions, there is nothing more needed for a formal
definition.  The rules for _using_ the X := E notation are entirely
subsumed by the axiom of definition.  The rules for introducing such
notations are rather complex and strange, but since you insist...

First, notice that most formal logics have no rule for introducing
definitions.  In other words, if you define some name X by introducing
an equality X = E, you are technically adding an axiom to the system
since this equality cannot be proven from the original axioms.  So
when you show that some logic L proves a formula P by introducing a
definition X = E, you are really showing that L+{X=E} proves P.
Clearly, just because L is consistent, there is no reason to suppose
that L+{X=E} is consistent.  This difficulty can be ignored for
eliminable definitions X=E because any occurence of X can in principle
be replaced by E, so that the proof in L+{X=E} directly corresponds to
a proof in L.

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.

The rule of definition introduction might look like

  true -> X := E, given that X does not appear previously in the
                  proof.

The condition on this axiom schema is strange because it refers to an
entire proof rather than to just a formula, but it is necessary to
prevent name clashes.  The condition I give above is also overly
strict since it should really only refer to free variables whose scope
(using the word in a broad sense) contains the context of the
definition.

]Things are particularly confusing since in the proposed Axiom of Definition
]it appears that what is "defined" in
]
]	X := E
]
]is a 0-place operation symbol (X) (i.e., a term).  What does it mean to
]provide a recursive definition for such an expression?

Please the see the original article for the answer to this.  The
answer is long enough that it would not be reasonable to repeat it
here.

]If ':=' is a
]binary relation symbol, it would be nice to have some clue concerning the
]properties of the relation in question.  This is not uninteresting, but
]essential.

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

]For example, it is possible to think of the Axiom of Definition as being
]proposed in a free logic where '=' has the usual semantics according to
]which
]
]	x = y
]
]is true just in case x and y both denote and have the same extension,
]but where ':=' has the semantics that
]
]	x := y
]
]is true just in case either both denote and have the same extension *or*
]both are denotationless.  The Axiom of Definition is sound under such
]an interpretation (given the usual interpretation of the quantifiers).
]I am sure that this is not your intention, but nothing you say appears
]to rule it out.

It might be possible to develop the notion of definition along the
lines of ':=' being a binary relation, and if so, this looks like a
good characterization of it.  But I have not really thought about that
possibility.
-- 
					David Gudeman
gudeman@cs.arizona.edu

Re: recursive definitions and paradoxes

#588

Author: Gary Merrill
Date: Mon, 23 Nov 1992 15:48

117 lines
5587 bytes

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

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads