Introduction                      <------  User Comment (blue)

------------

We want to "prove" that no dolphins are fish.

We make the following assumptions:

(a) No fish are mammals.

(b) All dolphins are mammals.

Logical Symbols

---------------

Fish(x)    means "x is a fish"

Mammal(x)  means "x is a mammal"

Dolphin(x) means "x is a dolphin"

ALL(x):    means "for all x, we have..."

=>         means "implies"

~          means "not"

Proof

-----

Suppose that all fish are not mammals.

1     ALL(a):[Fish(a) => ~Mammal(a)]    <------   Line#, Statement  (black)

      Premise                                    <------   Rule                          (gray)

Suppose further that all dolphins are mammals.

2     ALL(a):[Dolphin(a) => Mammal(a)]

      Premise

     Now, prove that is x is a dolphin then x is not a fish.

     Suppose that x is a dolphin.

      3     Dolphin(x)                   <------ Free variable (red or green)

            Premise

     From our second assumption, we have...

      4     Dolphin(x) => Mammal(x)

            U Spec, 2

     Therefore, x is a mammal.

      5     Mammal(x)

            Detach, 4, 3

     From our second premise, we have...

      6     Fish(x) => ~Mammal(x)

            U Spec, 1

     Obtain the contrapositive...

      7     ~~Mammal(x) => ~Fish(x)

            Contra, 6

     Remove the double negation...

      8     Mammal(x) => ~Fish(x)

            Rem DNeg, 7

     Therefore x is not a fish.

      9     ~Fish(x)

            Detach, 8, 5

As Required, if x is a dolphin, then x is not a fish.

10    Dolphin(x) => ~Fish(x)             <-------- Universal generalization

      4 Conclusion, 3                                          possible for green variables,

                                                                not for red variables.

Generalizing, all dolphins are not fish.

11    ALL(a):[Dolphin(a) => ~Fish(a)]    <-------- Universal generalization

      U Gen, 10