─────┬───── $𝖟𝕷𝖔𝖌𝖎𝖈/𝕾𝖒𝖚𝖑𝖑𝖞𝖆𝖓/𝕾𝖆𝖙𝖆𝖓-𝕮𝖆𝖓𝖙𝖔𝖗-𝖆𝖓𝖉-𝕴𝖓𝖋𝖎𝖓𝖎𝖙𝖞/𝖈𝖍1-𝖕𝖟1.𝖘𝖆𝖕𝖕𝖍𝖎𝖗𝖊 ──────────────────────────────
0┊-----------------------------| Satan, Cantor & Infinity ch I pz 1 |------------------------[sp]-
1┊--|∙Chapter∙I∙Puzzle∙1∙is∙asked∙on∙pg∙3
2┊
3┊--|∙A∙statement∙made∙by∙a∙resident∙of∙The∙Island∙of∙Knights∙and∙Knaves∙is∙true∙if∙and
4┊--|∙only∙if∙the∙resident∙is∙a∙knight.∙For∙this∙first∙problem
5┊
6┊--|∙a∙≡∙Arthur∙is∙a∙kinght∙∙∙b∙≡∙Bernard∙is∙a∙knight∙∙∙c∙≡∙Charles∙is∙a∙knight
7┊
8┊--|∙while∙⇒∙is∙used∙for∙implication,∙≡∙is∙used∙instead∙of∙⇐⇒∙for∙if∙and∙only∙if,∙to
9┊--|∙emphasize∙equivalence
10┊
11┊--|∙The∙statement∙that∙Bernard∙and∙Charles∙are∙both∙knights∙is∙translated∙as∙b∧c
12┊
13┊--|∙Either∙Arthur∙is∙a∙knight,∙and∙so∙are∙both∙Bernard∙and∙Charles,∙which∙is∙a∧(b∧c)
14┊--|∙or∙Arthur∙is∙a∙knave,∙and∙not∙both∙Bernard∙and∙Charles∙are∙knights∙is∙¬a∧¬(b∧c)
15┊
16┊--|∙Combined,∙a∧(b∧c)∨¬a∧¬(b∧c)
17┊
18┊--|∙We∙can∙also∙consider,∙the∙truth∙of∙a∙statement∙is∙equivalent∙to∙the∙speakers∙knightliness.
19┊--|∙Symbolically,∙a≡b∧c.∙The∙two∙forms∙are∙equivalent:
20┊
21┊taut:∙a∧(b∧c)∙∨∙¬a∧¬(b∧c)∙≡∙(a≡b∧c)
┊ a │✔│✘│✔│✘│✔│✘│✔│✘│
┊ b │✔│✔│✘│✘│✔│✔│✘│✘│
┊ c │✔│✔│✔│✔│✘│✘│✘│✘│
┊ ──────────────────────────┼─┼─┼─┼─┼─┼─┼─┼─┤
┊ b∧c │✔│✔│✘│✘│✘│✘│✘│✘│
┊ a∧(b∧c) │✔│✘│✘│✘│✘│✘│✘│✘│
┊ ¬a │✘│✔│✘│✔│✘│✔│✘│✔│
┊ ¬(b∧c) │✘│✘│✔│✔│✔│✔│✔│✔│
┊ ¬a∧¬(b∧c) │✘│✘│✘│✔│✘│✔│✘│✔│
┊ a∧(b∧c)∨¬a∧¬(b∧c) │✔│✘│✘│✔│✘│✔│✘│✔│
┊ a≡b∧c │✔│✘│✘│✔│✘│✔│✘│✔│
┊ ──────────────────────────┼─┼─┼─┼─┼─┼─┼─┼─┤
┊ a∧(b∧c)∨¬a∧¬(b∧c)≡(a≡b∧c) │✔│✔│✔│✔│✔│✔│✔│✔│
22┊
23┊--|∙Arthur∙denies∙Bernard∙is∙a∙knight:∙a∧¬b∙∨∙¬a∧¬(¬b),∙or∙a≡¬b
24┊
25┊taut:∙a∧¬b∙∨∙¬a∧¬¬b∙≡∙(a≡¬b)
┊ a │✔│✘│✔│✘│
┊ b │✔│✔│✘│✘│
┊ ───────────────────┼─┼─┼─┼─┤
┊ ¬b │✘│✘│✔│✔│
┊ a∧¬b │✘│✘│✔│✘│
┊ ¬a │✘│✔│✘│✔│
┊ ¬¬b │✔│✔│✘│✘│
┊ ¬a∧¬¬b │✘│✔│✘│✘│
┊ a∧¬b∨¬a∧¬¬b │✘│✔│✔│✘│
┊ a≡¬b │✘│✔│✔│✘│
┊ ───────────────────┼─┼─┼─┼─┤
┊ a∧¬b∨¬a∧¬¬b≡(a≡¬b) │✔│✔│✔│✔│
26┊
27┊--|∙we∙conclude∙Bernard∙is∙a∙knight∙and∙both∙Arthur∙and∙Charles∙are∙knaves:∙¬a∧b∧¬c
28┊
29┊--|∙Our∙solution∙satisfies∙Arthur's∙first∙statement
30┊taut:∙¬a∧b∧¬c∙⇒∙(a≡b∧c)
┊ a │✔│✘│✔│✘│✔│✘│✔│✘│
┊ b │✔│✔│✘│✘│✔│✔│✘│✘│
┊ c │✔│✔│✔│✔│✘│✘│✘│✘│
┊ ────────────────┼─┼─┼─┼─┼─┼─┼─┼─┤
┊ ¬a │✘│✔│✘│✔│✘│✔│✘│✔│
┊ ¬a∧b │✘│✔│✘│✘│✘│✔│✘│✘│
┊ ¬c │✘│✘│✘│✘│✔│✔│✔│✔│
┊ ¬a∧b∧¬c │✘│✘│✘│✘│✘│✔│✘│✘│
┊ b∧c │✔│✔│✘│✘│✘│✘│✘│✘│
┊ a≡b∧c │✔│✘│✘│✔│✘│✔│✘│✔│
┊ ────────────────┼─┼─┼─┼─┼─┼─┼─┼─┤
┊ ¬a∧b∧¬c⇒(a≡b∧c) │✔│✔│✔│✔│✔│✔│✔│✔│
31┊
32┊--|∙and∙Arthur's∙second∙statement
33┊taut:∙¬a∧b∧¬c∙⇒∙(a≡¬b)
┊ a │✔│✘│✔│✘│✔│✘│✔│✘│
┊ b │✔│✔│✘│✘│✔│✔│✘│✘│
┊ c │✔│✔│✔│✔│✘│✘│✘│✘│
┊ ───────────────┼─┼─┼─┼─┼─┼─┼─┼─┤
┊ ¬a │✘│✔│✘│✔│✘│✔│✘│✔│
┊ ¬a∧b │✘│✔│✘│✘│✘│✔│✘│✘│
┊ ¬c │✘│✘│✘│✘│✔│✔│✔│✔│
┊ ¬a∧b∧¬c │✘│✘│✘│✘│✘│✔│✘│✘│
┊ ¬b │✘│✘│✔│✔│✘│✘│✔│✔│
┊ a≡¬b │✘│✔│✔│✘│✘│✔│✔│✘│
┊ ───────────────┼─┼─┼─┼─┼─┼─┼─┼─┤
┊ ¬a∧b∧¬c⇒(a≡¬b) │✔│✔│✔│✔│✔│✔│✔│✔│
34┊
35┊--|∙and∙is∙in∙fact∙logically∙equivalent∙to∙Arthur's∙statements,∙taken∙together
36┊taut:∙¬a∧b∧¬c∙≡∙(a≡b∧c)∧(a≡¬b)
┊ a │✔│✘│✔│✘│✔│✘│✔│✘│
┊ b │✔│✔│✘│✘│✔│✔│✘│✘│
┊ c │✔│✔│✔│✔│✘│✘│✘│✘│
┊ ───────────────────────┼─┼─┼─┼─┼─┼─┼─┼─┤
┊ ¬a │✘│✔│✘│✔│✘│✔│✘│✔│
┊ ¬a∧b │✘│✔│✘│✘│✘│✔│✘│✘│
┊ ¬c │✘│✘│✘│✘│✔│✔│✔│✔│
┊ ¬a∧b∧¬c │✘│✘│✘│✘│✘│✔│✘│✘│
┊ b∧c │✔│✔│✘│✘│✘│✘│✘│✘│
┊ a≡b∧c │✔│✘│✘│✔│✘│✔│✘│✔│
┊ ¬b │✘│✘│✔│✔│✘│✘│✔│✔│
┊ a≡¬b │✘│✔│✔│✘│✘│✔│✔│✘│
┊ (a≡b∧c)∧(a≡¬b) │✘│✘│✘│✘│✘│✔│✘│✘│
┊ ───────────────────────┼─┼─┼─┼─┼─┼─┼─┼─┤
┊ ¬a∧b∧¬c≡(a≡b∧c)∧(a≡¬b) │✔│✔│✔│✔│✔│✔│✔│✔│
37┊
38┊
39┊proof:∙a≡b∧c∙a≡¬b∙∴∙¬a∧b∧¬c
40┊∙∙A∙⏵∙A∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙[rw]∙∙∙--|∙Simple∙Rewrite∙via∙Sapphire∙Normal∙Form
41┊∙∙P∧(P⇒Q)∙⏵∙Q∙∙∙∙∙∙∙∙∙∙∙∙∙∙[mp]∙∙∙--|∙Modus∙Ponens
42┊∙∙¬A∨B∙⏴⏵∙A⇒B∙∙∙∙∙∙∙∙∙∙∙∙∙∙[imp]∙∙--|∙Implication
43┊∙∙X⇒A∧B∙⏴⏵∙(X⇒A)∧(X⇒B)∙∙∙∙∙[cic]∙∙--|∙Composition∙of∙Implication∙over∙Conjunction
44┊∙∙A⇒B∙⏴⏵∙¬B⇒¬A∙∙∙∙∙∙∙∙∙∙∙∙∙[cp]∙∙∙--|∙Contrapositive
45┊∙∙(A⇒B)∧(A⇒¬B)∙⏴⏵∙¬A∙∙∙∙∙∙∙[cdct]∙--|∙Contradiction/Explosion
46┊∙∙¬(A∧B)∙⏴⏵∙¬A∨¬B∙∙∙∙∙∙∙∙∙∙[dna]∙∙--|∙Distribution∙of∙negation∙over∙and
47┊
48┊
49┊∙∙a≡¬b∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙[anb] - assumptions
50┊∙∙¬a⇒b∙∙∙∙∙∙∙∙∵∙cp∙⇑∙∙∙∙∙∙∙[nab] - A⇒B ⏴⏵ ¬B⇒¬A ⟪B→a A→¬b⟫
51┊
52┊∙∙a≡b∧c∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙∙[abc] - assumptions
53┊∙∙a⇒b∙∙∙∙∙∙∙∙∙∵∙cic∙⇑ - X⇒A∧B ⏴⏵ (X⇒A)∧(X⇒B) ⟪X→a A→c B→b⟫
54┊∙∙¬a∙∙∙∙∙∙∙∙∙∙∵∙cdct∙anb∙⇑∙[na] - (A⇒B)∧(A⇒¬B) ⏴⏵ ¬A ⟪A→a B→¬b⟫
55┊∙∙b∙∙∙∙∙∙∙∙∙∙∙∵∙mp∙⇑∙nab∙∙∙[b] - P∧(P⇒Q) ⏵ Q ⟪P→¬a Q→b⟫
56┊
57┊∙∙¬a⇒¬(b∧c)∙∙∙∵∙cp∙abc - A⇒B ⏴⏵ ¬B⇒¬A ⟪B→a A→b∧c⟫
58┊∙∙¬(b∧c)∙∙∙∙∙∙∵∙mp∙⇑∙na - P∧(P⇒Q) ⏵ Q ⟪P→¬a Q→¬(b∧c)⟫
59┊∙∙¬b∨¬c∙∙∙∙∙∙∙∵∙dna∙⇑ - ¬(A∧B) ⏴⏵ ¬A∨¬B ⟪A→c B→b⟫
60┊∙∙b⇒¬c∙∙∙∙∙∙∙∙∵∙imp∙⇑ - ¬A∨B ⏴⏵ A⇒B ⟪B→¬c A→b⟫
61┊∙∙¬c∙∙∙∙∙∙∙∙∙∙∵∙mp∙b∙⇑ - P∧(P⇒Q) ⏵ Q ⟪P→b Q→¬c⟫
62┊∙∙¬a∧b∧¬c∙∙∙∙∙∵∙rw∙na∙b∙⇑ - A ⏵ A ⟪A→b∧¬a∧¬c⟫
─────┴────────────────────────────────────────────────────────────────────────────────────────────────