🚀 go-pugleaf

In article  <1992Nov21.230530.117800@Cookie.secapl.com> Frank Adams 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".
]
]Actually, no.  Unless I am much mistaken, this kind of definition is
]eliminable.  If we have a definition X := E, we can rewrite a wff of
]the form P(X) as (All X.((Ex! X.X=E) => X=E) => P(X)).

I'm not sure what you mean.  If you mean that the definition plus the
axiom is eliminable, then of course you are right.  It is the purpose
of the axiom to make the definition "safe", which makes it eliminable
(although I think that your rewrite is wrong.  I believe it should be
(All X.((Ex! X.X=E) & (X=E)) => P(X)) since the existence of a unique
solution does not by itself imply that some free X _is_ the solution).
If you mean that the definition alone, with the naive assumption that
X:=E => X=E is eliminable, then you are mistaken.  This should be
obvious since naive definitions produce an inconsistent logic.

In any case, I think there is too much emphasis being paid to the
notion of definitions, which notion is really "eliminable" from my
argument.  In fact for Russell's paradox (the purported motivation for
all of this) the notion of definition only applies in a round-about
sense.  I really started thinking in terms of recursive definitions
when I was trying to figure out what would be the minimal machinery
that one would need to add to the propositional calculus to make the
liar's paradox possible.  Clearly recursive definitions are enough
since

  L := ~L

produces the paradox.  This is not quite identical to the original
paradox though.  To state it closer to its traditional form, you need
a way to talk about propsitions of the language in the language.  Then
you can express it something like

  L := "~M(L)"

where M is the meaning function that produces the truth value of a
proposition (it basically strips off the quotes).  So M(L) = ~M(L).
This pair of examples convinced me that this business of
language/meta-language confusion is bogus.  You don't really need to
have quoted propositions in order to express the paradox, and if you
do have quoted propositions, you still need some form of circularity.
Of course, you don't really need definitions as such.  You could use
something like a reflexive pronoun to get a sentence even closer to
the traditional form of the paradox.  Define "P(self)" to represent
the proposition P(self)[self:="P(self)"].  That is, 'self' refers to
the inermost quoted phrase of which it is a part.  Then

  "~self"

is a more traditional expression of the paradox, and one which does
not involve any explicit definitions or recursion.  But there is still
an implicit recursion due to the definition of 'self'.

Many of the traditional paradoxes are usually expressed _without_
explicit definitions, so I am not claiming that explicit definitions
are critical to the paradox.  But in all cases, the paradox can be
easily expressed in an otherwise consistent logic with a recursive
definition added.  It is in this sense that I say the paradoxes are
"caused" by recursion.  Maybe it would be better to say that all the
paradoxes are caused by some error that is equivalent to the
uncritical use of a recursive definition.

I don't think the same can be said for any of the other proposed
"causes" of the paradoxes.  Naive comprehension only applies to the
set theoretic paradoxes.  Impredicativeness only applies to paradoxes
that involve quantification.  Language/meta-language confusion only
applies to the so-called linguistic paradoxes.  Type violation only
applies to paradoxes that involve typed quantities (and not to the
"linguistic" paradoxes).
-- 
					David Gudeman
gudeman@cs.arizona.edu