Homework 6 Solutions

Prove the following sequents using only Peano's axioms:

  1. (3 points) 
    |- -(0'=0'')
  1 (1) 0'=0''            A
  1 (2) 0=0'              1 SUCC
    (3) -(0=0')           NOT0
  1 (4) (0=0') & -(0=0')  2,3 &I
    (5) -(0'=0'')         1,4 RAA
  2. (3 points) 
    |- 0'''×0''=0''''''
  (1)  0'''×0''=(0'''×0')+0'''  MULT1
  (2)  0'''×0'=(0'''×0)+0'''    MULT1
  (3)  0'''×0=0                 MULT0
  (4)  0'''×0'=0+0'''           3,2 SUBST
  (5)  0+0'''=(0+0'')'          PLUS1
  (6)  0+0''=(0+0')'            PLUS1
  (7)  0+0'=(0+0)'              PLUS1
  (8)  0+0=0                    PLUS0
  (9)  0+0'=0'                  8,7 SUBST
  (10) 0+0''=0''                9,6 SUBST
  (11) 0+0'''=0'''              10,5 SUBST
  (12) 0'''×0'=0'''             11,4 SUBST
  (13) 0'''×0''=0'''+0'''       12,1 SUBST
  (14) 0'''+0'''=(0'''+0'')'    PLUS1
  (15) 0'''+0''=(0'''+0')'      PLUS1
  (16) 0'''+0'=(0'''+0)'        PLUS1
  (17) 0'''+0=0'''              PLUS0
  (18) 0'''+0'=0''''            17,16 SUBST
  (19) 0'''+0''=0'''''          18,15 SUBST
  (20) 0'''+0'''=0''''''        19,14 SUBST
  (21) 0'''×0''=0''''''         20,13 SUBST
  3. (3 points) We choose to do induction on c, since it always occurs as the right-hand operand, which matches the given rules for + and ×: 
    |- a×(b+c)=(a×b)+(a×c)
  (1) a×(b+0)=(a×b)+(a×0)                               TI 1, below
  (2) (a×(b+x)=(a×b)+(a×x)) -> (a×(b+x')=(a×b)+(a×x'))  TI 2, below
  (3) a×(b+c)=(a×b)+(a×c)                               1,2 IND

    This depends on the following two ``subroutine'' theorems:

    1. Base case: 
      |- a×(b+0)=(a×b)+(a×0)
  (1) a×(b+0)=a×(b+0)          REFL
  (2) b+0=b                    PLUS0
  (3) a×(b+0)=a×b              2,1 SUBST
  (4) (a×b)+(a×0)=(a×b)+(a×0)  REFL
  (5) a×0=0                    MULT0
  (6) (a×b)+0=(a×b)+(a×0)      5,4 SUBST
  (7) (a×b)+0=a×b              PLUS0
  (8) a×b=(a×b)+(a×0)          7,6 SUBST
  (9) a×(b+0)=(a×b)+(a×0)      8,3 SUBST
    2. Inductive case: 
      |- (a×(b+x)=(a×b)+(a×x)) -> (a×(b+x')=(a×b)+(a×x'))
  1 (1)  a×(b+x)=(a×b)+(a×x)                               A
    (2)  a×(b+x')=a×(b+x')                                 REFL
    (3)  b+x'=(b+x)'                                       PLUS1
    (4)  a×(b+x')=a×(b+x)'                                 3,2 SUBST
    (5)  a×(b+x)'=(a×(b+x))+a                              MULT1
    (6)  a×(b+x')=(a×(b+x))+a                              5,4 SUBST
  1 (7)  a×(b+x')=((a×b)+(a×x))+a                          1,6 SUBST
    (8)  (a×b)+(a×x')=(a×b)+(a×x')                         REFL
    (9)  a×x'=(a×x)+a                                      MULT1
    (10) (a×b)+((a×x)+a)=(a×b)+(a×x')                      9,8 SUBST
    (11) (a×b)+((a×x)+a)=((a×b)+(a×x))+a                   TI(S) ASSOC
    (12) ((a×b)+(a×x))+a=(a×b)+(a×x')                      11,10 SUBST
  1 (13) a×(b+x')=(a×b)+(a×x')                             12,7 SUBST
    (14) (a×(b+x)=(a×b)+(a×x)) -> (a×(b+x')=(a×b)+(a×x'))  1,13 CP
  4. (3 points, extra credit) This proof has a very similar structure to the previous one; again, we will proceed by induction on c: 
    |- a×(b×c)=(a×b)×c
  (1) a×(b×0)=(a×b)×0                           TI 1, below
  (2) (a×(b×x)=(a×b)×x) -> (a×(b×x')=(a×b)×x')  TI 2, below
  (3) a×(b×c)=(a×b)×c                           1,2 IND
    1. Base case: 
      |- a×(b×0)=(a×b)×0
  (1) a×(b×0)=a×(b×0)  REFL
  (2) b×0=0            MULT0
  (3) a×(b×0)=a×0      2,1 SUBST
  (4) a×0=0            MULT0
  (5) a×(b×0)=0        4,3 SUBST
  (6) (a×b)×0=(a×b)×0  REFL
  (7) (a×b)×0=0        MULT0
  (8) 0=(a×b)×0        7,6 SUBST
  (9) a×(b×0)=(a×b)×0  8,5 SUBST
    2. Inductive case: 
      |- (a×(b×x)=(a×b)×x) -> (a×(b×x')=(a×b)×x')
  1 (1)  a×(b×x)=(a×b)×x                           A
    (2)  a×(b×x')=a×(b×x')                         REFL
    (3)  b×x'=(b×x)+b                              MULT1
    (4)  a×(b×x')=a×((b×x)+b)                      3,2 SUBST
    (5)  a×((b×x)+b)=(a×(b×x))+(a×b)               TI(S) problem 3
    (6)  a×(b×x')=(a×(b×x))+(a×b)                  5,4 SUBST
  1 (7)  a×(b×x')=((a×b)×x)+(a×b)                  1,6 SUBST
    (8)  (a×b)×x'=(a×b)×x'                         REFL
    (9)  (a×b)×x'=((a×b)×x)+(a×b)                  MULT1
    (10) ((a×b)×x)+(a×b)=(a×b)×x'                  9,8 SUBST
  1 (11) a×(b×x')=(a×b)×x'                         10,7 SUBST
    (12) (a×(b×x)=(a×b)×x) -> (a×(b×x')=(a×b)×x')  1,11 CP