Independence of L10 from L1-L9,L11 (L1-L9,L11 - true, L10 - not)



 Negation truth table 

 A  ~A 

 0  2

 1  2

 2  1



 Implication truth table 

 A B  A->B 

 0 0  2

 0 1  2

 0 2  2

 1 0  0

 1 1  2

 1 2  2

 2 0  0

 2 1  1

 2 2  2



 Conjunction truth table 

 A B  A&B 

 0 0  0

 0 1  0

 0 2  0

 1 0  0

 1 1  1

 1 2  1

 2 0  0

 2 1  1

 2 2  2



 Disjunction truth table 

 A B  AvB 

 0 0  0

 0 1  1

 0 2  2

 1 0  1

 1 1  1

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Axiom L1 

 A B  A->(B->A) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Axiom L2 

 A B C  (A->(B->C))->((A->B)->(A->C)) 

 0 0 0  2

 0 0 1  2

 0 0 2  2

 0 1 0  2

 0 1 1  2

 0 1 2  2

 0 2 0  2

 0 2 1  2

 0 2 2  2

 1 0 0  2

 1 0 1  2

 1 0 2  2

 1 1 0  2

 1 1 1  2

 1 1 2  2

 1 2 0  2

 1 2 1  2

 1 2 2  2

 2 0 0  2

 2 0 1  2

 2 0 2  2

 2 1 0  2

 2 1 1  2

 2 1 2  2

 2 2 0  2

 2 2 1  2

 2 2 2  2



 Axiom L3 

 A B  A->(B->(A&B)) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Axiom L4 

 A B  (A&B)->A 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Axiom L5 

 A B  (A&B)->B 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Axiom L6 

 A B  A->(AvB) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Axiom L7 

 A B  B->(AvB) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Axiom L8 

 A B C  (A->C)->((B->C)->((AvB)->C)) 

 0 0 0  2

 0 0 1  2

 0 0 2  2

 0 1 0  2

 0 1 1  2

 0 1 2  2

 0 2 0  2

 0 2 1  2

 0 2 2  2

 1 0 0  2

 1 0 1  2

 1 0 2  2

 1 1 0  2

 1 1 1  2

 1 1 2  2

 1 2 0  2

 1 2 1  2

 1 2 2  2

 2 0 0  2

 2 0 1  2

 2 0 2  2

 2 1 0  2

 2 1 1  2

 2 1 2  2

 2 2 0  2

 2 2 1  2

 2 2 2  2



 Axiom L9 

 A B  (A->B)->((A->(~B))->(~A)) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Axiom L10 

 A B  (~A)->(A->B) 

 0 0  2

 0 1  2

 0 2  2

 1 0  0

 1 1  2

 1 2  2

 2 0  0

 2 1  2

 2 2  2



 Axiom L11 

 A  Av(~A) 

 0  2

 1  2

 2  2



 Constructively provable formulas



 A B  (AvB)->((~A)->B) 

 0 0  2

 0 1  2

 0 2  2

 1 0  0

 1 1  2

 1 2  2

 2 0  0

 2 1  2

 2 2  2



 A B  ((~A)vB)->(A->B) 

 0 0  2

 0 1  2

 0 2  2

 1 0  0

 1 1  2

 1 2  2

 2 0  0

 2 1  2

 2 2  2



 A B  ((~~A)->(~~B))->(~~(A->B)) 

 0 0  2

 0 1  2

 0 2  2

 1 0  1

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  (~~A)->((~A)->A) 

 0 0  0

 0 1  0

 0 2  0

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  (Av(~A))->((~~A)->A) 

 0 0  0

 0 1  0

 0 2  0

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  ~~((~~A)->A) 

 0 0  1

 0 1  1

 0 2  1

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 Classically provable formulas



 A B  (~~(AvB))->((~~A)v(~~B)) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  (~(A&B))->((~A)v(~B)) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  (~~A)->A 

 0 0  0

 0 1  0

 0 2  0

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  ((~B)->(~A))->(A->B) 

 0 0  2

 0 1  2

 0 2  2

 1 0  0

 1 1  2

 1 2  2

 2 0  0

 2 1  2

 2 2  2



 A B  ((~A)->B)->((~B)->A) 

 0 0  2

 0 1  0

 0 2  0

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  ((~~A)->(~~B))->(A->B) 

 0 0  2

 0 1  2

 0 2  2

 1 0  0

 1 1  2

 1 2  2

 2 0  0

 2 1  2

 2 2  2



 A B  (A->B)->((~A)vB) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  ((A->B)->B)->(AvB) 

 0 0  2

 0 1  2

 0 2  2

 1 0  1

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  ((A->B)->A)->A 

 0 0  2

 0 1  2

 0 2  2

 1 0  1

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  (~(A&(~B)))->(A->B) 

 0 0  2

 0 1  2

 0 2  2

 1 0  0

 1 1  2

 1 2  2

 2 0  0

 2 1  2

 2 2  2



 A B  (A->B)->((~A->B)->B) 

 0 0  0

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  (~(A->B))->(A&(~B)) 

 0 0  0

 0 1  0

 0 2  0

 1 0  1

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  Av(A->B) 

 0 0  2

 0 1  2

 0 2  2

 1 0  1

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  (A->B)v(B->A) 

 0 0  2

 0 1  2

 0 2  2

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2



 A B  (A->B)->(((~A)->(~B))->(B->A)) 

 0 0  2

 0 1  0

 0 2  0

 1 0  2

 1 1  2

 1 2  2

 2 0  2

 2 1  2

 2 2  2