logical symbols

RE01 Rice Brian T. EM2 BRice@vinson.navy.mil
Wed, 21 Oct 1998 15:53:37 -0700


I have an open question concerning some issues in mathematics with which
I have been working recently.  I was wondering if anybody can give me a
sensible explanation of the reason for basing most logics on several
certain operators.  For instance, the standard predicate logic has
'and', 'imp', 'not'(or false), and 'forall'.  I am particularly
interested in the effects of these symbols on how we think about
declarative programming, particularly the fact that the quantifier is
necessary in some form, leading to the extensionality of the same order
as that due to the lambda-operator of the lambda-calculus.
It seems that this operator-class constitutes some sort of dirty
reflectivity with a limited (unary) scope.  Also, the statement that:

"For all variables x, A(...x...) is true" is equivalent to "There does
not exist a variable x such that A(...x...) is not true"

(natural language use is due solely to the text format. think of the
symbolic form)

seems to make clear the idea that the "forall" and "thereexists"
operators to be statements, at least in common-sense terms.  However,
these operators are declarations about symbols, not intensions.  They
seem also to be declarations of a meta-language sort: they operate on
expressions which are independent of their component formulae.  Because
of the extensionality associated with these operators, evaluators have a
much more difficult time rendering transformations upon structures of
logics and the lambda-calculus, particularly in the interesting
applications of these languages where statements become uncountable,
etc.