What level of our proofs is "correct"?

[jdiamond]

This was a good email reply from Sandip to a general question I had
about this class that I thought might be useful for everyone. It
includes a formal proof of "plug in the booleans."

Sandip Ray wrote:
> Hi Jeff,
>
> Thanks for explaining the issue. Here are some comments which I
hope
> will be beneficial.
>
> One goal of the course (and the key goal at least for the first
part)
> is to develop enough logical machinery so that we can write down
some
> steps which correspond almost to the informal argument and still
make
> sure that there's a derivation in the logic. We sometimes (as in
the
> case of deduction law) do that outside the logic, but typically
the
> only thing we do is skip some steps. It is to ensure that the
> skipping of steps is sound that the derived rules of inference
are
> for. But whenever we do so, we must be confident in our mind
that,
> if challenged, we can produce a formal derivation by filling out
all
> the skipped steps.
>
> Whenever anyone does a proof in class, I tend to ask the whole
class
> whether they believe in the derivation. What I mean is that,
everyone
> is convinced, given the steps written down, that they can fill in
the
> gaps and produce a formal derivation if challenged. When I ask
that,
> if you or anyone else has a doubt or confusion that they cannot
do
> that (at least in principle), then you should say so and ask the
> person doing the proof to elaborate. I do that some time, but I
don't
> do it if nobody in the class seems to have a problem because I
then
> assume that everyone has understood how to do it. Actually, to
be
> objective, I let people write a proof at the level at which ACL2
can
> fill the gaps, but that is my personal choice and what is
important is
> that everyone sitting should participate and ask questions as
long as
> it is unclear why a given step corresponds to a derivation (or
can be
> refined into a sequence of steps that does). When everyone is
> convinced, we feel it's justified not to go into the details that
> everyone understands.
>
> Now back to the question about HW2. Why is it true that we can
check
> the cases and be done with it?
>
> Remember that we learnt the derived rule of inference "Case
> splitting": Derive B from (A => B) and (~A => B)
>
> Thus, say the formula P we want to prove has the variables x and
y.
> Then we can derive P by proving
>
> Case 1: (x = nil) => P and
> Case 2: ~(x = nil) => P.
>
> By the deduction law, we can prove Case 1 by proving:
>
> Case 1' Given X = NIL Prove P.
>
> While proving Case 1' we can substitute NIL for x, by the
> instantiation rule.
>
> Similarly we can break Case 1' further by doing the same thing
for y,
> namely
>
> Case 1.1 Given X = NIL prove (Y = NIL) => P
> Case 1.2 Given X = NIL prove ~(Y = NIL) => P
>
> And so on. This lets us prove the theorem by checking these
cases.
>
> One point to note is about the "clever derivations" that we did
> earlier. The point of those derivations is _not_ that we go on
doing
> derivations of that kind, but provide you with enough derived
rules of
> inference (such as case splits) so that in the later proofs we
can do
> a proof to mimic the way in which your informal intuition goes,
while
> feeling confident that each such step can be made completely
formal
> steps in the derivation.
>
> Hope this helps. If you think it's worthwhile please feel free
to
> post some part of the reply to the class group (or ask me to do
so).
>
> Thanks,
>
> -- Sandip
>
> Date: Fri, 19 Sep 2008 21:13:15 -0500
> From: Jeffrey R Diamond <jeffrey...@yahoo.com>
> X-Server-Quench: b06159f9-86b9-11dd-8155-001185d377ca
> X-AuthRoute: OCdxaQwWC1ZXQQoU EC4VFiNBQAAiIBFk
EBYDKgwcK10MQx9Y NEpbNnJYKxsBWVxJ UiUVDgARHl9xRgAg KxVTbQVVckpNVQRp
WklODFFQCgxvHx0A BgAfVhttdQBEfWFw KxtqJXIvK0MpdUR7 SkZXW2kBZGYuOmAZ
UUVRIQpJeAUYdwJE awQrSXsMZGAaZnph Rl9uM2tuYj5WPh5Y EEk2MVMWRQ4XBC89
QR9KATJnEkAZDzkz IlQmI1gTVEEfelky MF0uQhRedXdp
> X-Authentic-SMTP: 61633239343338.squirrel.dmpriest.net.uk:1186/
Kp
> X-Report-SPAM: If SPAM / abuse - report it at: http://www.authsmtp.com/abuse
> X-Virus-Status: No virus detected - but ensure you scan with
your own anti-virus system!
> X-SpamAssassin-Status: No, hits=0.1 required=5.0
> X-UTCS-Spam-Status: No, hits=-90 required=165
> X-Status:
> X-Keywords:
> X-UID: 2
>
> Thanks so much for your help, Sandip, and I hope I didn't
sound pessimistic.
> Whenever we write a proof on the board, I do understand the
proof. But
> what I don't know (as you see when students have to amend
things) is
> whether more or less steps were needed. Certainly my first
instinct
> would be to go about it in an "easier way", which I interpret
as less
> formal. But then at the same time I see steps written down
that I
> wouldn't think would be legal jumps.
>
> As you say, this may just be my inability to tell when we're
really
> outside the logic. I really don't mind hand waiving as long
as I can
> tell we weren't after a "derivation" but just a "proof."
>
> On the other extreme lies the Homework #2 proofs - I was
attempting them
> all symbolically like we did in class. But the official
answers did
> nothing but look at the four possible boolean inputs,
evaluated the
> expressions in each case, and declared the problem solved.
It's not
> that I think what they did was wrong, but how does this fit in
with all
> our clever proofs?