Child pages
  • CSU 290 (Spring 2008)
Skip to end of metadata
Go to start of metadata

You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 6 Next »

This is the resource page for Section 2 of Logic and Computation, CSU 290 (Spring 2008). Welcome.

The purpose of this page is to simply complete the lectures, partly to keep us in sync with the other section, partly because there is only so much time and much interesting things to discuss.

These notes are meant to supplement the lectures, the readings and the lecture notes (available on the course web site) and not replace them.

Feel free to comment at the bottom of the page if you have any questions or anything is unclear. (Select "Add Comment" under "Add Content" down below.) I will generally merge your comments and questions into the main text when I get to them.

What you should do right now: Make sure you are logged into the wiki. (Select "Log In" under "Your Account" below if not, use you CCIS credentials to log in.) Look at the bottom of the page, under "Other Features", top right icon is an envelope. Press that button. That will register you as watching this page. Basically, every time the page changes, you get an email saying so. Keeps you from having to check the page regularly.

February 15: Formal proof for ~(t=nil)

Here is a complete formal proof for ~(t=nil) using the axioms I gave in class. (This is the proof that I started on Monday, but ran out of time 5 steps into the proof.)

You should be able to understand all the steps in that proof, if not be able to come up with the proof yourself. We will not ask you to come up with these kind of formal proofs in this course. Instead, we will use the more informal "chain of equals" or "chain of relations" approach I presented in class.

In the proof below, I write ~A for "not A" and A & B for "A and B".

1. ~(equal (car (cons x y) x) x) = nil        [ axiom for equal/car/cons 
2. ~(equal (car (cons a b) a) a) = nil)       [ instantiation of 1 with x->a, y->b 

Okay, so 2 is something we will use later on. Let's remember it.

3. ~(x = y) => (equal x y) = nil              [ axiom for equal 
4. ~(car (cons a b)) = a =>
         (equal (car (cons a b)) a) = nil     [ instantiation of 3 with x->(car (cons a b)), y->a 
5. ~(~(car (cons a b)) = a)                   [ by MT applied to 4 and 2 
6. ~(~A) => A                                 [ tautology of Boolean logic 
7. ~(~(car (cons a b)) = a) =>
      (car (cons a b)) = a                    [ instantiation of 6 with A->(car (cons a b)) 
8. (car (cons a b)) = a                       [ by MP applied to 7 and 5 
9. x=y => (equal x y) = y                     [ axiom for equal 
10. (car (cons a b)) = a =>
        (equal (car (cons a b)) a) = t        [ instantiation of 9 with x->(car (cons a b)),y->a 
11. (equal (car (cons a b)) a) = t            [ by MP applied to 10 and 8

Excellent. So now we can see that 2 and 11 together essentially give us that t /= nil.
We just have to work some to get that to come out of the proof.

12. (A & B => C) => (A & ~C => ~B)            [ tautology of Boolean logic (check it!) 
13. ((equal (car (cons a b)) a) = t
      & t = nil => 
          (equal (car (cons a b)) a) = nil))  [ instantiation of 12 with 
     => ((equal (car (cons a b)) a) = t       [  A->(equal (car (cons a b)) a) = t
        & ~(equal (car (cons a b)) a) = nil)) [  B->(t=nil)
             => ~(t = nil))                   [  C->(equal (car (cons a b)) a) = nil 
14. x = y & y = z => x = z                    [ axiom of transitivity 
15. (equal (car (cons a b)) a) = t            [ instantiation of 14 with 
     & t = nil =>                             [   x->(equal (car (cons a b)) a)
         (equal (car (cons a b)) a) = nil     [   y->t  and z->nil
16. (equal (car (cons a b)) a) = t            [ by MP applied to 13 and 15
    & ~(equal (car (cons a b)) a) = nil
          => ~(t = nil)

And we are just about done. We have both antecedents of the implication in 16.

17. ~(t=nil)                                  [ by MP applied to 16, 11, and 2
  • No labels