associativity_of_biconditional_bryan_kok

associativity_of_biconditional_bryan_kok

proof

1     (p <=> q) <=> r                                 Hypothesis         %  ok                        
2     (p <=> q) => r                                  AndEL 1            %  ok                        
3     r => (p <=> q)                                  AndER 1            %  ok                        
4     [ p                                             Assumption         %  ok                        
5       [ r                                           Assumption         %  ok                        
6         p <=> q                                     ImpE 3,5           %  ok                        
7         p => q                                      AndEL 6            %  ok                        
8         q ]                                         ImpE 7,4           %  ok                        
9       r => q                                        ImpI 5-8           %  ok                        
10      [ q                                           Assumption         %  ok                        
11        [ p                                         Assumption         %  ok                        
12          q ]                                       Hyp 10             %  ok                        
13        p => q                                      ImpI 11-12         %  ok                        
14        [ q                                         Assumption         %  ok                        
15          p ]                                       Hyp 4              %  ok                        
16        q => p                                      ImpI 14-15         %  ok                        
17        p <=> q                                     AndI 13,16         %  ok                        
18        r ]                                         ImpE 2,17          %  ok                        
19      q => r                                        ImpI 10-18         %  ok                        
20      q <=> r ]                                     AndI 19,9          %  ok                        
21    p => (q <=> r)                                  ImpI 4-20          %  ok
                        
22    [ q <=> r                                       Assumption         %  ok                        
23      [ ~p                                          Assumption         %  ok 

# By proving ~r from the assumption of ~p, we would implicitly show ~(p <=> q) by modus tollens,
# which is not the case..
                       
24        [ r                                         Assumption         %  ok                        
25          r => q                                    AndER 22           %  ok                        
26          q                                         ImpE 25,24         %  ok                        
27          p <=> q                                   ImpE 3,24          %  ok                        
28          q => p                                    AndER 27           %  ok                        
29          p                                         ImpE 28,26         %  ok                        
30          F ]                                       ImpE 23,29         %  ok                        
31        ~r                                          ImpI 24-30         %  ok                        
32        q => r                                      AndEL 22           %  ok                        
33        [ q                                         Assumption         %  ok                        
34          r                                         ImpE 32,33         %  ok                        
35          F ]                                       ImpE 31,34         %  ok                        
36        ~q                                          ImpI 33-35         %  ok 

# Because p <=> q is True when both p and q are False.                        
37        [ p                                         Assumption         %  ok                        
38          F                                         ImpE 23,37         %  ok                        
39          q ]                                       FalseE 38          %  ok                        
40        p => q                                      ImpI 37-39         %  ok                        
41        [ q                                         Assumption         %  ok                        
42          F                                         ImpE 36,41         %  ok                        
43          p ]                                       FalseE 42          %  ok                        
44        q => p                                      ImpI 41-43         %  ok                        
45        p <=> q                                     AndI 40,44         %  ok                        
46        r                                           ImpE 2,45          %  ok                        
47        F ]                                         ImpE 31,46         %  ok                        
48      p ]                                           Class 23-47        %  ok                        
49    (q <=> r) => p                                  ImpI 22-48         %  ok                        
50    p <=> (q <=> r)                                 AndI 21,49         %  ok