Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 10 Sep 1993 08:48:00 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA27000;
          Fri, 10 Sep 93 00:38:44 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA26996; Fri, 10 Sep 93 00:38:43 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA16768;
          Fri, 10 Sep 93 00:38:48 -0700
Message-Id: <9309100738.AA16768@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: Re: jjj proof challenge
Cc: borm@cs.ubc.ca
Date: Fri, 10 Sep 93 00:38:44 PDT
From: chou@cs.ucla.edu

Konrad Slind wrote:

> Indeed, as Josh mentioned, the main problem in the proof is
> the confusion caused by quantifiers having loose scopes.

Indeed, I can't help wondering how the theorem came up in the first place.
Perhaps Eric Borm can enlighten us?

- Ching Tsun