🚀 go-pugleaf

In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|> In article  <BxzG21.Gnr@unx.sas.com> Gary Merrill writes:
|> ]
|> ]In article <26788@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (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.

"Defined formally by its usage"?? "They seemed uninteresting"?
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?  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.

As it is, all we have is the proposed Axiom of Definition, which we can
take as a *partial* formalization of ':='.  This is not enough.

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.

Either a little more precision and formalization or, failing that, some
specific examples of such "definitions" would be an aid to the understanding.
-- 
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

In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|> 
|> 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.

I have a vague recollection of a result that any recursive definition
is eliminable in favor of an explicit definition (Scott? Montague?  A faulty
memory?).  At any rate, concerning the claim that mathematics cannot
be done with "such a sparse notion of definition", it is interesting
to inspect Chapters X and XI of Kalish and Montague where the theory
of commutataive ordered fields is definitionally extended to the theory
of real numbers which in turn is definitionally extended to the
theory of convergence.  A sketch is then given of how this can be
extended to the integral calculus (including an explicit definition
of the Riemann integral).  In passing, it is observed that the 'recursive
definition' of sigma (the summation operator) used in the theory can be
replaced by an explicit definition.  All this rests in part on the work
of Scott on arbitrary variabe binding operators.

Perhaps you really want to avoid talk of "definition" and simply speak
of "axiomatization".
-- 
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

In article <By174J.JBM@unx.sas.com> sasghm@theseus.unx.sas.com (Gary Merrill) writes:

   In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
   |> 
   |> 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.

   I have a vague recollection of a result that any recursive definition
   is eliminable in favor of an explicit definition (Scott? Montague?  A faulty
   memory?).  ...

Beth's theorem ("Padoa's method is general"), a more-or-less immediate
consequence of the Craig interpolation lemma.  (No doubt Mr. Gudeman
will be unimpressed, however.)

                                                        -- rar

In article <1emo86INN4de@roche.csl.sri.com>, rar@csl.sri.com (Bob Riemenschneider) writes:
|> In article <By174J.JBM@unx.sas.com> sasghm@theseus.unx.sas.com (Gary Merrill) writes:
|> 
|>    In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|>    |> 
|>    |> 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.
|> 
|>    I have a vague recollection of a result that any recursive definition
|>    is eliminable in favor of an explicit definition (Scott? Montague?  A faulty
|>    memory?).  ...
|> 
|> Beth's theorem ("Padoa's method is general"), a more-or-less immediate
|> consequence of the Craig interpolation lemma.  (No doubt Mr. Gudeman
|> will be unimpressed, however.)
|> 
|>                                                         -- rar

Also, apparently the general technique of converting recursive definitons
to explicit definitions is provided by Frege.  There is an old paper
of Quine's ("Tarski's Theory of Truth", reprinted in _Selected Logic
Papers_) in which he demonstrates a theory containing a "recursive
definition" that cannot be eliminated without rendering the theory
inconsistent.  However, since the extended theory contains the protosyntax
of the base theory, it is not clear what can be made of this for
claims about eliminability or uneliminability in general.
-- 
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

In article <26841@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <BxzG21.Gnr@unx.sas.com> Gary Merrill writes:
>]In article <26788@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (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
>]
>]... 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.

This statement is at best misleading.  The proposed notion of definition,
with the axiom given, *is* eliminable (and hence non-creative), as I have
noted in another posting.  *Without* the axiom given, it is of course also
eliminable -- you can prove something about X given X := E iff you can
prove it about a free variable X.  Only with the naive axiom of definition
is it not eliminable -- and then it is inconsistent.

There are other axioms which could be added which would make this kind of
definition non-eliminable, and David may have some such in mind.  No such
have been presented, however.