─────┬───── $𝖟𝕷𝖔𝖌𝖎𝖈/𝕾𝖒𝖚𝖑𝖑𝖞𝖆𝖓/𝕾𝖆𝖙𝖆𝖓-𝕮𝖆𝖓𝖙𝖔𝖗-𝖆𝖓𝖉-𝕴𝖓𝖋𝖎𝖓𝖎𝖙𝖞/𝖎-𝖘𝖆𝖙𝖆𝖓.𝖘𝖆𝖕𝖕𝖍𝖎𝖗𝖊 ──────────────────────────────
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⟫
─────┴────────────────────────────────────────────────────────────────────────────────────────────────