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