─────┬────────── $𝖘𝖕/𝖘𝖆𝖓𝖌𝖚𝖎𝖓𝖊/𝖕𝖗𝖔𝖔𝖋𝖘-0.𝖘𝖆𝖕𝖕𝖍𝖎𝖗𝖊 ──────────────────────────────────────────────────────
0┊---------------------|·Some·Propositional·Proofs·in·Sapphire·(Zero)·|---------------------------
1┊--|·Trivial,·but·valid
2┊proof:·x·y·∴·x∧y
3┊••A·B·⊢·A∧B·······[r]
4┊••x···············[0] - assumption
5┊••y···············[1] - assumption
6┊••x∧y·∵·r·0·1 - A B ⊢ A∧B {A→x B→y}
7┊
8┊--|·∨·commutivity
9┊proof:·x∨y·∴·y∨x
10┊••⊢·¬A∨A···············[r1]
11┊••A∨B·¬A∨C·⊢·B∨C·······[r2]
12┊••x∨y··················[0] - assumption
13┊••¬x∨x·∵·r1············[1] - ⊢ ¬A∨A {A→x}
14┊••y∨x·∵·r2·0·1 - A∨B ¬A∨C ⊢ B∨C {A→x B→y C→x}
15┊
16┊--|·Same·proof,·different·names
17┊proof:·p∨q·∴·q∨p
18┊••X∨Y·¬X∨Z·⊢·Y∨Z···[r1]
19┊••⊢·¬X∨X···········[r2]
20┊••p∨q··············[0] - assumption
21┊••¬p∨p·∵·r2········[1] - ⊢ ¬X∨X {X→p}
22┊••q∨p·∵·r1·0·1 - X∨Y ¬X∨Z ⊢ Y∨Z {X→p Y→q Z→p}
23┊
24┊--|·∨·associativity
25┊proof:·x∨y∨z·∴·x∨(y∨z)
26┊••A∨(B∨C)·⊢·A∨B∨C·········[r1]
27┊••A∨B·⊢·B∨A···············[r2]
28┊••x∨y∨z···················[0] - assumption
29┊••z∨(x∨y)·∵·r2·0··········[1] - A∨B ⊢ B∨A {A→x∨y B→z}
30┊••z∨x∨y·∵·r1·1············[2] - A∨(B∨C) ⊢ A∨B∨C {A→z B→x C→y}
31┊••y∨(z∨x)·∵·r2·2··········[3] - A∨B ⊢ B∨A {A→z∨x B→y}
32┊••y∨z∨x·∵·r1·3············[4] - A∨(B∨C) ⊢ A∨B∨C {A→y B→z C→x}
33┊••x∨(y∨z)·∵·r2·4 - A∨B ⊢ B∨A {A→y∨z B→x}
34┊
35┊--|·∧·commutivity
36┊proof:·p∧q·∴·q∧p
37┊••A∧B·⊢·A··········[r1]
38┊••A∧B·⊢·B··········[r2]
39┊••A·B·⊢·A∧B········[r3]
40┊••p∧q··············[0] - assumption
41┊••p·∵·r1·0·········[1] - A∧B ⊢ A {A→p B→q}
42┊••q·∵·r2·0·········[2] - A∧B ⊢ B {A→p B→q}
43┊••q∧p·∵·r3·2·1 - A B ⊢ A∧B {A→q B→p}
44┊
45┊proof:·p·(x∨y)·∴·(y∨x)
46┊••(P∨Q)·(¬P∨R)·⊢·(Q∨R)···[r1]
47┊••⊢·(¬P∨P)···············[r2]
48┊••(x∨y)··················[0] - assumption
49┊••(¬x∨x)·∵·r2············[1] - ⊢ ¬P∨P {P→x}
50┊••(y∨x)·∵·r1·0·1 - P∨Q ¬P∨R ⊢ Q∨R {P→x Q→y R→x}
51┊
52┊proof:·(x∨y)·∴·(y∨x)
53┊••p∨q·¬p∨r·⊢·q∨r······[r1]
54┊••⊢·(¬p∨p)············[r2]
55┊••(¬x∨x)·∵·r2·········[0] - ⊢ ¬p∨p {p→x}
56┊••(x∨y)···············[1] - assumption
57┊••(y∨x)·∵·r1·1·0 - p∨q ¬p∨r ⊢ q∨r {p→x q→y r→x}
58┊
59┊proof:·((x∨y)∨z)·∴·(x∨(y∨z))
60┊••(A∨B)·⊢·(B∨A)···········[r1]
61┊••(A∨(B∨C))·⊢·((A∨B)∨C)···[r2]
62┊••((x∨y)∨z)···············[0] - assumption
63┊••(z∨(x∨y))·∵·r1·0········[1] - A∨B ⊢ B∨A {A→x∨y B→z}
64┊••((z∨x)∨y)·∵·r2·1········[2] - A∨(B∨C) ⊢ A∨B∨C {A→z B→x C→y}
65┊••(y∨(z∨x))·∵·r1·2········[3] - A∨B ⊢ B∨A {A→z∨x B→y}
66┊••((y∨z)∨x)·∵·r2·3········[4] - A∨(B∨C) ⊢ A∨B∨C {A→y B→z C→x}
67┊••(x∨(y∨z))·∵·r1·4 - A∨B ⊢ B∨A {A→y∨z B→x}
68┊
69┊proof:·∴·(p⇒p)
70┊••A·(A⇒B)·⊢·B······························[r1]
71┊••⊢·((X⇒(Y⇒Z))⇒((X⇒Y)⇒(X⇒Z)))··············[r2]
72┊••⊢·(Q⇒(P⇒Q))······························[r3]
73┊••(p⇒((p⇒p)⇒p))·∵·r3·······················[0] - ⊢ Q⇒(P⇒Q) {Q→p P→p⇒p}
74┊••((p⇒((p⇒p)⇒p))⇒((p⇒(p⇒p))⇒(p⇒p)))·∵·r2···[1] - ⊢ (X⇒(Y⇒Z))⇒((X⇒Y)⇒(X⇒Z)) {X→p Y→p⇒p Z→p}
75┊••((p⇒(p⇒p))⇒(p⇒p))·∵·r1·0·1···············[2] - A A⇒B ⊢ B {A→p⇒((p⇒p)⇒p) B→(p⇒(p⇒p))⇒(p⇒p)}
76┊••(p⇒(p⇒p))·∵·r3···························[3] - ⊢ Q⇒(P⇒Q) {Q→p P→p}
77┊••(p⇒p)·∵·r1·3·2 - A A⇒B ⊢ B {A→p⇒(p⇒p) B→p⇒p}
78┊
79┊proof:·x∨y·∴·y∨x
80┊••⊢·¬p∨p·················[r1]
81┊••p∨q·¬p∨r·⊢·q∨r·········[r2]
82┊••x∨y····················[0] - assumption
83┊••¬x∨x·∵·r1··············[1] - ⊢ ¬p∨p {p→x}
84┊••y∨x·∵·r2·0·1 - p∨q ¬p∨r ⊢ q∨r {p→x q→y r→x}
85┊
86┊proof:·a⇒b·b⇒c·∴·a⇒c
87┊••A·(A⇒B)·⊢·B·················[mp]
88┊••⊢·Q⇒(P⇒Q)···················[r1]
89┊••⊢·(X⇒(Y⇒Z))⇒((X⇒Y)⇒(X⇒Z))···[r2]
90┊••a⇒b·····························[0] - assumption
91┊••b⇒c·····························[1] - assumption
92┊••(b⇒c)⇒(a⇒(b⇒c))··········∵·r1···[2] - ⊢ Q⇒(P⇒Q) {Q→b⇒c P→a}
93┊••(a⇒(b⇒c))⇒((a⇒b)⇒(a⇒c))··∵·r2···[3] - ⊢ (X⇒(Y⇒Z))⇒((X⇒Y)⇒(X⇒Z)) {X→a Y→b Z→c}
94┊••a⇒(b⇒c)··············∵·mp·1·2···[4] - A A⇒B ⊢ B {A→b⇒c B→a⇒(b⇒c)}
95┊••(a⇒b)⇒(a⇒c)··········∵·mp·4·3···[5] - A A⇒B ⊢ B {A→a⇒(b⇒c) B→(a⇒b)⇒(a⇒c)}
96┊••a⇒c··················∵·mp·0·5 - A A⇒B ⊢ B {A→a⇒b B→a⇒c}
97┊
98┊
99┊proof:·a⇒b·b⇒c·∴·a⇒c
100┊••A·(A⇒B)·⊢·B·················[mp]
101┊••⊢·Q⇒(P⇒Q)···················[r1]
102┊••⊢·(X⇒(Y⇒Z))⇒((X⇒Y)⇒(X⇒Z))···[r2]
103┊••M⇒N·O·⊢·M⇒(N∧O)·············[r3]
104┊••a⇒b·····························[0] - assumption
105┊••b⇒c·····························[1] - assumption
106┊••(b⇒c)⇒(a⇒(b⇒c))··········∵·r1···[2] - ⊢ Q⇒(P⇒Q) {Q→b⇒c P→a}
107┊••(a⇒(b⇒c))⇒((a⇒b)⇒(a⇒c))··∵·r2···[3] - ⊢ (X⇒(Y⇒Z))⇒((X⇒Y)⇒(X⇒Z)) {X→a Y→b Z→c}
108┊••a⇒(b⇒c)··············∵·mp·1·2···[4] - A A⇒B ⊢ B {A→b⇒c B→a⇒(b⇒c)}
109┊••(a⇒b)⇒(a⇒c)··········∵·mp·4·3···[5] - A A⇒B ⊢ B {A→a⇒(b⇒c) B→(a⇒b)⇒(a⇒c)}
110┊••a⇒c··················∵·mp·0·5 - A A⇒B ⊢ B {A→a⇒b B→a⇒c}
─────┴────────────────────────────────────────────────────────────────────────────────────────────────