logical symbols

[Tril]

On Wed, 21 Oct 1998, RE01 Rice Brian T. EM2 wrote:

> 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:

Quantifiers and lambdas use naming because names are required when writing
an expression sequentially (using strings).  Alpha-conversion in lambda
calculus shows that the actual name picked is irrelevant.  In predicate
calculus, we find that the inference rules for adding and removing
quantifiers (UG, EG, UI, and EI) need to have qualifiers such as "x is not
flagged", "t is free to replace x in w" and "x is not subscripted".  These
rules are only needed because variables have names associated with them.
Once we get rid of linear, written forms we can get rid of variable names.
So the representation of "\x.x x" would not even remember the variable was
named x (except for user sugar in printing out the expression later).
Instead the expression would simply store the information that there is an
input at two places.  You can think of it replacing x with a hole, or a
dependency to the outside world.  I think I'm doing a bad job of
explaining this, so I'll stop.  Maybe this will help: Instead of storing
that "this is the variable x" in each place where x occurs, all the
computer has to do is remember that each occurence of x is "the same" and
the name can be left out.  "The same" can be represented by pointers, or a
number, or anything.  I hope that was understandable.

> [...] 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.

I don't really understand what you mean, here.  After you define
extensions and intentions I may have a better idea.  But could you clarify
"independent of their component formulae" (what formulae?) and some more
detail of statements becoming uncountable?

Perhaps it is better to make the abstraction explicit.  I have an
expression "x ^ y" (with all variables free).  It has some structure,
which can be described by a tree.  The operation in the expression with
the lowest precedence is at the root of the tree (^). 

Then, I apply the UG rule to "x ^ y" (add a forall quantifier), I have
just created a new expression (because the tree changed).  

What if I did negation to "x ^ y" instead of applying UG?  Then I also
would have changed the expression, but in a different way.

When I negate "x ^ y", I end up with "not(x ^ y)".  The "not" is now at
the top of the tree, because it has to be performed last.  However, in the
expression "forall[x](x ^ y)" (I just made up some notation here), the
change is not describable in the same way.  "forall" is not an operator
with less precedence than "and".  In fact, "forall" would have modified
the meaning of the expression in more than one place, if x had occured
more than once.

Without getting any more detailed, I agree, "forall" is a more powerful
operator than, say, "not".  "Forall x" seems to be defining a property of
every "x" that appears in the expression (the property that it is
universally quantified).  It also defines a property of the expression: 
the property of all x's being universally quantified.  I think forall
really is multiple things. (In TUNES any object that is multiple things is
a compound object, of multiple objects that are only one thing) 1. It says
what is being universally quantified.  2. It says something is being
universally quantified.  and 3. The scope in which (1) applies.  [(3)
being implicit in the syntax.]  Our job is to orthogonalize these 3
properties, make sure they are all explicit and can be adjusted
independently.  Hope this helps.

David Manifold <dem@tunes.org>