─────┬───── $𝖟𝕷𝖔𝖌𝖎𝖈/𝕾𝖒𝖚𝖑𝖑𝖞𝖆𝖓/𝕾𝖆𝖙𝖆𝖓-𝕮𝖆𝖓𝖙𝖔𝖗-𝖆𝖓𝖉-𝕴𝖓𝖋𝖎𝖓𝖎𝖙𝖞/𝖎-𝖘𝖆𝖙𝖆𝖓.𝖘𝖆𝖕𝖕𝖍𝖎𝖗𝖊 ──────────────────────────────

    0┊---------------------------------|·Satan,·Cantor·&·Infinity·I·|---------------------------------

    1┊--|·problem·on·Page·3:·a→Arthur·b→Bernard·c→Charles                                            

    2┊--|·Arthur·confirms·Bernard·and·Charles·are·both·knights                                       

    3┊a∧(b∧c)∨¬a∧¬(b∧c)                                                                              

    4┊--|·Arthur·denies·Bernard·is·a·knight                                                          

    5┊a∧¬b∨¬a∧b                                                                                      

    6┊                                                                                               

    7┊proof:·a∧(b∧c)∨¬a∧(¬b∨¬c)·a∧¬b∨¬a∧b·∴·¬a∧b∧¬c                                                  

    8┊∙∙A·≡·A····································[eqsp]·--|·Equivalent·Sapphire·Normal·Forms         

    9┊∙∙(A∨X)∧(¬A∨Y)·≡·X∨Y·······················[r]                                                 

   10┊∙∙A∧B·⊢·A··································[cind]·--|·Conjunctive·Independence                 

   11┊∙∙P∧(P⇒Q)·⊢·Q······························[mp]···--|·Modus·Ponens                             

   12┊∙∙⊢·P∨¬P···································[lem]··--|·The·Law·of·Excluded·Middle               

   13┊∙∙A∧(X∨Y)·≡·A∧X∨A∧Y························[ado]··--|·And·Distribution·over·Or                 

   14┊∙∙B∨Z∧W·≡·(B∨Z)∧(B∨W)······················[oda]··--|·Or·Distribution·over·And                 

   15┊∙∙¬A∨B·≡·A⇒B·······························[imp]··--|·Implication                              

   16┊∙∙A∨B·≡·¬A⇒B·······························[imp2]·--|·Implication                              

   17┊∙∙A⇒B·≡·¬B⇒¬A······························[cp]···--|·Contrapositive                           

   18┊∙∙(X⇒A)∧(X⇒B)·≡·X⇒A∧B······················[cc]···--|·Composition·of·Conjunction               

   19┊∙∙X⇒A∧B·⊢·X⇒A······························[dcc]··--|·Decomposition·of·Conjunction             

   20┊∙∙⊢·¬(A∧¬A)································[con]··--|·Consistency                              

   21┊∙∙A·≡·¬¬A··································[dneg]·--|·Double·Negation                          

   22┊                                                                                               

   23┊∙∙a∧(b∧c)∨¬a∧(¬b∨¬c)·······················[0] - assumption                                    

   24┊∙∙a∧¬b∨¬a∧b································[1] - assumption                                    

   25┊                                                                                               

   26┊∙∙(a∧¬b∨¬a)∧(a∧¬b∨b)·∵·oda·1···············[2] - B∨Z∧W ≡ (B∨Z)∧(B∨W) ⟪B→a∧¬b W→¬a Z→b⟫         

   27┊∙∙(a∧(b∧c)∨¬a)∧(a∧(b∧c)∨(¬b∨¬c))·∵·oda·0···[3] - B∨Z∧W ≡ (B∨Z)∧(B∨W) ⟪B→a∧b∧c W→¬b∨¬c Z→¬a⟫    

   28┊∙∙a∧¬b∨¬a·∵·cind·2·························[4] - A∧B ⊢ A ⟪A→¬a∨a∧¬b B→b∨a∧¬b⟫                  

   29┊∙∙a∨¬a·∵·lem                                   - ⊢ P∨¬P ⟪P→a⟫                                  

   30┊∙∙(¬a∨a)∧(¬a∨¬b)·∵·oda·4···················[6] - B∨Z∧W ≡ (B∨Z)∧(B∨W) ⟪B→¬a W→¬b Z→a⟫           

   31┊∙∙a∨¬a·∵·lem                                   - ⊢ P∨¬P ⟪P→a⟫                                  

   32┊∙∙¬a∨¬b·∵·cind·6···························[8] - A∧B ⊢ A ⟪A→¬a∨¬b B→a∨¬a⟫                      

   33┊∙∙a⇒¬b·∵·imp·8·····························[9] - ¬A∨B ≡ A⇒B ⟪A→a B→¬b⟫                         

   34┊∙∙a∧(b∧c)∨¬a·∵·cind·3······················[10] - A∧B ⊢ A ⟪A→¬a∨a∧b∧c B→¬b∨¬c∨a∧b∧c⟫           

   35┊∙∙a∨¬a·∵·lem                                    - ⊢ P∨¬P ⟪P→a⟫                                 

   36┊∙∙a⇒a∧(b∧c)·∵·imp·10·······················[12] - ¬A∨B ≡ A⇒B ⟪A→a B→a∧b∧c⟫                     

   37┊∙∙a⇒b∧c·∵·dcc·12···························[13] - X⇒A∧B ⊢ X⇒A ⟪X→a A→b∧c B→a⟫                  

   38┊∙∙a⇒b·∵·dcc·13·····························[14] - X⇒A∧B ⊢ X⇒A ⟪X→a A→b B→c⟫                    

   39┊∙∙a⇒b∧¬b·∵·cc·9·14·························[15] - (X⇒A)∧(X⇒B) ≡ X⇒A∧B ⟪X→a A→¬b B→b⟫           

   40┊∙∙¬(b∧¬b)⇒¬a·∵·cp·15·······················[16] - A⇒B ≡ ¬B⇒¬A ⟪B→b∧¬b A→a⟫                     

   41┊∙∙¬(b∧¬b)·∵·con····························[17] - ⊢ ¬(A∧¬A) ⟪A→b⟫                              

   42┊∙∙¬a·∵·mp·17·16····························[18] - P∧(P⇒Q) ⊢ Q ⟪Q→¬a P→¬(b∧¬b)⟫                 

   43┊∙∙a∨¬a·∵·lem                                    - ⊢ P∨¬P ⟪P→a⟫                                 

   44┊∙∙a∧¬b∨b·∵·cind·2··························[20] - A∧B ⊢ A ⟪A→b∨a∧¬b B→¬a∨a∧¬b⟫                 

   45┊∙∙a∨¬a·∵·lem                                    - ⊢ P∨¬P ⟪P→a⟫                                 

   46┊∙∙(b∨a)∧(b∨¬b)·∵·oda·20····················[22] - B∨Z∧W ≡ (B∨Z)∧(B∨W) ⟪B→b W→¬b Z→a⟫           

   47┊∙∙b∨a·∵·cind·22····························[23] - A∧B ⊢ A ⟪A→a∨b B→b∨¬b⟫                       

   48┊∙∙a∨¬a·∵·lem                                    - ⊢ P∨¬P ⟪P→a⟫                                 

   49┊∙∙¬a⇒b·∵·imp2··23··························[25] - A∨B ≡ ¬A⇒B ⟪A→a B→b⟫                         

   50┊∙∙b·∵·mp·18·25·····························[26] - P∧(P⇒Q) ⊢ Q ⟪Q→b P→¬a⟫                       

   51┊∙∙a∨¬a·∵·lem                                    - ⊢ P∨¬P ⟪P→a⟫                                 

   52┊∙∙a∧(b∧c)∨(¬b∨¬c)·∵·cind·3·················[28] - A∧B ⊢ A ⟪A→¬b∨¬c∨a∧b∧c B→¬a∨a∧b∧c⟫           

   53┊∙∙a∨¬a·∵·lem                                    - ⊢ P∨¬P ⟪P→a⟫                                 

   54┊∙∙((¬b∨¬c)∨a)∧((¬b∨¬c)∨(b∧c))·∵·oda·28·····[30] - B∨Z∧W ≡ (B∨Z)∧(B∨W) ⟪B→¬b∨¬c W→b∧c Z→a⟫      

   55┊∙∙(¬b∨¬c)∨a·∵·cind·30······················[31] - A∧B ⊢ A ⟪A→a∨¬b∨¬c B→¬b∨¬c∨b∧c⟫              

   56┊∙∙a∨¬a·∵·lem                                    - ⊢ P∨¬P ⟪P→a⟫                                 

   57┊∙∙¬a⇒(¬b∨¬c)·∵·imp2·31·····················[33] - A∨B ≡ ¬A⇒B ⟪A→a B→¬b∨¬c⟫                     

   58┊∙∙¬b∨¬c·∵·mp·18·33·························[34] - P∧(P⇒Q) ⊢ Q ⟪Q→¬b∨¬c P→¬a⟫                   

   59┊∙∙b⇒¬c·∵·imp·34····························[35] - ¬A∨B ≡ A⇒B ⟪A→b B→¬c⟫                        

   60┊∙∙¬c·∵·mp·26·35····························[36] - P∧(P⇒Q) ⊢ Q ⟪Q→¬c P→b⟫                       

   61┊∙∙¬a∧b∧¬c·∵·eqsp·18·26·36                       - A ≡ A ⟪A→b∧¬a∧¬c⟫                            

─────┴────────────────────────────────────────────────────────────────────────────────────────────────