Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Full-Name: Joshua D. Guttman
Posted-Date: Thu, 09 Sep 1993 11:06:39 -0400
Message-Id: <9309091506.AA02840@nausicaa>
To: info-hol@cs.uidaho.edu
Cc: borm@cs.ubc.ca, guttman@linus.mitre.org
Subject: Re: a little proof challenge
In-Reply-To: Your message of "Thu, 09 Sep 1993 10:45:32 EDT." <9309091445.AA02828@nausicaa>
Date: Thu, 09 Sep 1993 11:06:39 -0400
From: "Joshua D. Guttman" <guttman@linus.mitre.org>
Content-Length: 976

Actually, may I bother you with one further point? 

I really didn't understand the content of this formula until I had
Imps simplify it.  The result of simplifying the original, puzzling
formula is:

forall(p,q:[ind,prop],
  nonvacuous_q{p} and nonvacuous_q{q}
   implies 
  forall(r:[ind,prop],
    forsome(v:ind,
      (p(v) or nonvacuous_q{r})
       and 
      (nonvacuous_q{r} implies q(v)))))

This makes it clear that what we're assuming is that the predicates p
and q are non-vacuous, and we're looking for a value v that will
satisfy one of them, where *which* one depends on whether r is
non-vacuous.  So the instantiation 

v |=>  if(nonvacuous_q{r},y_$0,x_$0) 

is obvious when Imps provides x_$0 and y_$0 as the witnesses for p and
q.  

So I think that this illustrates the idea that a good proof (whether
a mechanized proof or an ordinary rigorous mathematical argument) is
one that makes it transparent what the theorem says, and why that's
true.  

	Josh