Practice

{2.2} Here's a proof of B <- A from A -> B.

A -> B |- A -> B   A |- A
-------------------------
     A -> B ; A |- B
     ---------------  [CI]
     A ; A -> B |- B
     ----------------
     A -> B |- B <- A
     

B <- A |- B <- A   A |- A
-------------------------
     A ; B <- A |- B
     ---------------  [CI]
     B <- A ; A |- B
     ----------------
     B <- A |- A -> B
     

{2.3} If 0 |- A and 0 |- A -> B then we have 0 ; 0 |- B, and by Left Pop we have 0 |- B.

Therefore, since 0 |- t, if 0 |- t -> A we have 0 |- A. Conversely, if 0 |- A, then by Left Push we have 0 ; 0 |- A and hence 0 ; t |- A and 0 |- t -> A as desired.

Finally, 0 |- A -> (B -> C) if and only if A |- B -> C if and only if A ; B |- C if and only if A o B |- C if and only if 0 |- A o B -> C as desired. (The case for converse implication is similar.)

{2.4} Here are the proofs.

                   A & C |- A & C
                   --------------
A -> B |- A -> B    A & C |- A
------------------------------
     A -> B ; A & C |- B
     --------------------
     A -> B |- A & C -> B

A -> B |- A -> B     B |- B
----------------------------
      A -> B ; A |- B
    --------------------
    A -> B ; A |- B v C
    --------------------
    A -> B |- A -> B v C

A & B |- A & B
--------------
  A & B |- A
--------------
0 ; A & B |- A
---------------
0 |- A & B -> A

A & B |- A & B
--------------
  A & B |- B
--------------
0 ; A & B |- B
---------------
0 |- A & B -> B

    A |- A
  ----------
  A |- A v B
--------------
0 ; A |- A v B
---------------
0 |- A -> A v B

    B |- B
  ----------
  B |- A v B
--------------
0 ; B |- A v B
---------------
0 |- B -> A v B

{2.5} Here is one family connection:

A -> B |- A -> B   A |- A
-------------------------
      A -> B ; A |- B
     -----------------
     A |- B <- (A -> B)

{2.6}

    
                   A |- A      B |- B    A |- A      C |- C
                   ------------------    ------------------
                      A;B |- A o B         A;C |- A o C
                  --------------------  --------------------
                  A;B |- (AoB) v (AoC)  A;C |- (AoB) v (AoC)   BvC |- BvC
                  -------------------------------------------------------
Ao(BvC) |- Ao(BvC)      A; BvC |- (AoB) v (AoC)
-----------------------------------------------
A o (B v C) |- (A o B) v (A o C)
	

Problems

Projects