The SBPC Logic

SBPC Axioms

• Start with A1, A2, A4, A5, A8, A9
• Add (a and o are logical and and or)

      P(j(x,o(x,y)))                          % A11
      P(i(y,o(x,y)))                          % A12
      P(j(j(x,z),j(j(y,z),j(o(x,y),z))))      % A13
      P(i(a(x,y),x))                          % A14
      P(j(a(x,y),y))                          % A15
      P(i(i(x,y),i(i(x,z),i(x,a(y,z)))))      % A16 

• Proved

      P(j(i(x,y),i(o(x,z),o(y,z))))           % T5
      P(j(i(x,y),i(o(z,x),o(z,y))))           % T6
      P(j(i(x,y),j(i(y,x),i(a(x,z),a(y,z))))) % T7
      P(j(i(x,y),i(a(z,x),a(z,y))))           % T8

  avoiding A3, A6, A7

P(i(j(j(x,y),x),x)) % A7

• A7 proved from A1, A2, A4, A5, A8, A9, A11 A12 A13, A14, A15, A16
  avoiding A3 and A6