🚀 go-pugleaf

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