NetNews Usenet Archive 1992 #27/NN_1992_27.iso/spool/sci/logic/2122

Internet Message Format | 1992-11-20 | 2.3 KB

Path: sparky!uunet!destroyer!ncar!noao!arizona!gudeman
From: [e-mail] (David Gudeman)
Newsgroups: sci.logic
Subject: Re: recursive definitions and paradoxes
Message-ID: <[e-mail]>
Date: 20 Nov 92 17:30:34 GMT
Organization: U of Arizona CS Dept, Tucson
Lines: 46

In article  <[e-mail]> Gary Merrill writes:
]
]In article <[e-mail]>, [e-mail] (David Gudeman) writes:
]
]|> I propose for discussion the
]|>
]|>   Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E
]|>
]|> where "Exist! x" means "there exists a unique x such that".  What if you
]
]I have not *carefully* read the rest of this posting.  However, on
]the face of it, it appears that this "axiom of definition" is quite
]suspect.  I'm not sure what
]
]    X := E
]
]means.  If it is really intended to represent a *definition* of X,
]then why is the new axiom necessary? What exactly is the symbol
]':=' meant to express beyond (or short of) '='?

The symbol '=' alone does not point out what variable is being
defined, but ':=', (which is defined formally by its usage) does.  I
did not discuss the rules for introducing X := E because they seemed
uninteresting.  It is clear that you need syntactic rules to avoid
naming conflicts and that rules must cover a range of clauses in a
proof.  That is, a definition has a scope that includes more than just
the clause in which it is introduced.  Clearly, no axiom or normal
rule of inference is adequate to specify this.

]... Definitions must
]satisfy such criteria as non-creativity (you can't prove something
][in "old" notation] by using the definition that you couldn't
]without it) and eliminability (the defined notation must be eliminable
]in *all* contexts).  The fact that the above axiom is being suggested
]seems to imply that the proposed "definition" does not satisfy the
]criterion of eliminability...

Exactly.  Actually, my notion of definition does not satisfy either of
the two notions you mention.  Recursive definitions are creative and
non-eliminable, and for that reason they have to be protected with an
axiom that limits their use.  Non-creative, eliminable definitions are
no more than abbreviations, and mathematics cannot be done with such a
sparse notion of definition.
--
                    David Gudeman
[e-mail]