# FOLQP

## Jack Waugh — 2001-09-05 14:55:51

    It hit me that what Manfred von Thun has done with the lambda

    calculus, we could extend to the first-order logic of quantification

    and predication (FOLQP).  That is, he has produced a notation of

    equivalent power to the lambda calculus but without bound (or any)

    variables.  This can facilitate mechanical inference, because we can

    avoid the headaches of dealing with variables.  FOLQP also people

    usually notate it with bound variables.  But the same transform as

    von Thun has done to the lambda calculus we can apply similarly to

    the notation of for-alls and there-exists.  The result can be a

    notation for expressing logical truths that submits more easily to

    machine reasoning than the conventional notation does.

    Participants in this forum have been using the Joy notation to

    express programs.  But a similar notation can express truths

    instead.  For example, we could write

        2 2 =

    to express the truth that 2 = 2, instead of to express a program that

    transforms one stack to a another stack with "true" on top of it and

    the original stack elements underneath.  Then using this idea of

    expressing truths in Joy-like notation, we can express statements in

    FOLQP without using bound variables.  For example,

        nats dup [all] dip any successor

    says that every natural number has a successor that is also a natural

    number, if we accept that:

    'nats' "pushes" the set of natural numbers,

    'all' "takes" a set "from the stack" and "pushes" in its place a

    variable universally quantified as a member of the set,

    'any' "takes" a set "from the stack" and "pushes" in its place a

    variable existentially quantified as a member of the set, and

    'successor' denotes the function that pops a number from the stack

    and pushes its successor (equivalent to 1 + in Joy).

    So with a stack-oriented-looking notation that gave no names to any

    bound variables, we have expressed the equivalent of "for all X an

    element of nats, there exists Y an element of nats, such that Y is

    the successor of X".

    Perhaps there are laws of substitution that we can derive that would

    always transform true statements in this notation into other true

    statements?  Would a body of such laws realize all the power of FOLQP?

    Combinators could extend this concept to second-order logic.

## Manfred von Thun — 2001-09-06 06:22:38

    On Wed, 5 Sep 2001, Jack Waugh wrote:

     > It hit me that what Manfred von Thun has done with the lambda

    > calculus, we could extend to the first-order logic of quantification

    > and predication (FOLQP).  That is, he has produced a notation of

    > equivalent power to the lambda calculus but without bound (or any)

    > variables.  This can facilitate mechanical inference, because we can

    > avoid the headaches of dealing with variables.  FOLQP also people

    > usually notate it with bound variables.  But the same transform as

    > von Thun has done to the lambda calculus we can apply similarly to

    > the notation of for-alls and there-exists.  The result can be a

    > notation for expressing logical truths that submits more easily to

    > machine reasoning than the conventional notation does.

     [more details deleted]

    You are exactly right. In fact, what you are describing is just about

    the history of Joy in reverse. The elimination of variables of quanti-

    fication is due to Schoenfinkel, then was taken up by Curry and applied

    to the elimination of variables of the lambda calculus, then again

    by Quine for variables of quantification.

    [Quine uses two stack operators: swap (lower case) the top two elements,

     and Swap (upper case) the top and the bottom element of the stack.

     This is just from memory, it is ages since I read his paper.]

    There are some references to this in the "Rationale for Joy" paper and

    in the "Mathematical Foundations of Joy" paper. My starting point was

    Quine, then Backus. The true (pre-)history of Joy was tortuous and

    nothing to brag about.

      -Manfred