git @ Cat's Eye Technologies Eqthy / c0df531
Add Johnson's axiom system and proof of Rule of Constancy. Chris Pressey 4 months ago
3 changed file(s) with 128 addition(s) and 2 deletion(s). Raw diff Collapse all Expand all
+7
-0
HISTORY.md less more
1919 * "on LHS", "on RHS" in hints are correctly handled.
2020 * Correct line number is now reported in error messages when
2121 the source Eqthy document is embedded in Markdown.
22
23 Distribution:
24
25 * Added an Eqthy formulation of Johnson's 1892 axiom system for
26 propositional logic, given in Meredith and Prior's 1967 paper
27 [Equational Logic](https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093893457),
28 and, using it, a proof of the Rule of Constancy.
2229
2330 0.4
2431 ---
+2
-2
README.md less more
5353 * some properties of [set difference](eg/set-difference.eqthy.md);
5454 * in [Interior Algebra](eg/interior-algebra.eqthy.md) (building on Boolean algebra);
5555 * in [Propositional Algebra](eg/propositional-algebra.eqthy.md);
56 * of the [Rule of Constancy](eg/rule-of-constancy.eqthy.md) in Johnson's 1892
57 equational axiom system for propositional logic;
5658 * in [Combinatory Logic](eg/combinatory-logic.eqthy.md);
5759
5860 with hopefully more to come in the future.
121123 ### Desired Examples
122124
123125 * [Relation algebra](https://en.wikipedia.org/wiki/Relation_algebra)
124 * Johnson's 1892 axiom system given in Meredith and Prior's 1967 paper
125 [Equational Logic](https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093893457)
126126 * The theorem of ring theory given in [Equational Logic, Spring 2017](https://people.math.sc.edu/mcnulty/alglatvar/equationallogic.pdf)
127127 by George McNulty (but it's a bit of a monster all right)
128128
+119
-0
eg/rule-of-constancy.eqthy.md less more
0 Rule of Constancy
1 =================
2
3 <!--
4 SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
5 For more information, please refer to <https://unlicense.org/>
6 SPDX-License-Identifier: Unlicense
7 -->
8
9 Here we take Johnson's 1892 equational axiom system for propositional logic, as
10 related in Meredith and Prior's 1967 paper [Equational Logic](https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093893457),
11 and write it in Eqthy:
12
13 axiom (#conj-comm) conj(X, Y) = conj(Y, X)
14 axiom (#conj-assoc) conj(X, conj(Y, Z)) = conj(conj(X, Y), Z)
15 axiom (#conj-idem) conj(X, X) = X
16 axiom (#neg-invol) not(not(X)) = X
17 axiom (#implication) not(X) = conj(not(conj(X, Y)), not(conj(X, not(Y))))
18
19 I don't have a good reason for calling axiom 5 "implication", only that it's
20 plausible that it serves a function similar to implication in this system,
21 and it's a nicer name than "axiom5".
22
23 Anyway, with these we can prove the "Rule of Constancy".
24
25 But first we're going to introduce a lemma to make this less tiresome.
26 We really should introduce this as its own theorem, and prove it. But
27 because it's "obvious", and tiresome, we'll cheat and assert it as an axiom.
28
29 axiom (#conj-perm) conj(A, conj(B, conj(C, D))) = conj(D, conj(B, conj(C, A)))
30
31 OK, now the theorem.
32
33 theorem (#rule-of-constancy)
34 conj(A, not(A)) = conj(C, not(C))
35 proof
36 A = A
37 conj(A, not(A)) = conj(A, not(A)) [by substitution of conj(A, not(A)) into A]
38 conj(A, not(A)) = conj(not(not(A)), not(A))
39 conj(A, not(A)) = conj(
40 not(not(A)),
41 conj(not(conj(A, C)), not(conj(A, not(C))))
42 ) [by #implication with X=A, Y=C]
43 conj(A, not(A)) = conj(
44 conj(not(conj(not(A), C)), not(conj(not(A), not(C)))),
45 conj(not(conj(A, C)), not(conj(A, not(C))))
46 ) [by #implication with X=A, Y=C]
47
48 conj(A, not(A)) = conj(
49 conj(not(conj(not(A), C)), not(conj(not(A), not(C)))),
50 conj(not(conj(A, C)), not(conj(not(C), A)))
51 ) [by #conj-comm]
52 conj(A, not(A)) = conj(
53 conj(not(conj(not(A), C)), not(conj(not(A), not(C)))),
54 conj(not(conj(C, A)), not(conj(not(C), A)))
55 ) [by #conj-comm]
56 conj(A, not(A)) = conj(
57 conj(not(conj(not(A), C)), not(conj(not(C), not(A)))),
58 conj(not(conj(C, A)), not(conj(not(C), A)))
59 ) [by #conj-comm]
60 conj(A, not(A)) = conj(
61 conj(not(conj(C, not(A))), not(conj(not(C), not(A)))),
62 conj(not(conj(C, A)), not(conj(not(C), A)))
63 ) [by #conj-comm]
64
65 conj(A, not(A)) = conj(
66 not(conj(C, not(A))),
67 conj(
68 not(conj(not(C), not(A))),
69 conj(
70 not(conj(C, A)),
71 not(conj(not(C), A))
72 )
73 )
74 )
75
76 conj(A, not(A)) = conj(
77 not(conj(not(C), A)),
78 conj(
79 not(conj(not(C), not(A))),
80 conj(
81 not(conj(C, A)),
82 not(conj(C, not(A)))
83 )
84 )
85 ) [by #conj-perm]
86
87 conj(A, not(A)) = conj(
88 conj(
89 not(conj(not(C), A)),
90 not(conj(not(C), not(A)))
91 ),
92 conj(
93 not(conj(C, A)),
94 not(conj(C, not(A)))
95 )
96 ) [by #conj-assoc]
97
98 conj(A, not(A)) = conj(
99 not(not(C)),
100 conj(not(conj(C, A)), not(conj(C, not(A))))
101 ) [by #implication with X=C, Y=A]
102
103 conj(A, not(A)) = conj(not(not(C)), not(C)) [by #implication with X=C, Y=A]
104
105 conj(A, not(A)) = conj(C, not(C))
106 qed
107
108 Now a question: Why did Johnson feel the need to do this? To show that
109 `conj(A, not(A))` is invariant, no matter one's choice of A. And thus,
110 it's a constant, and we can call this constant "Falsum".
111
112 But is this whole rigamarole necessary? Didn't Johnson allow substitution
113 as a rule? Yes, but uniform substition won't get us there: if you
114 substitute `C` for `A` you just get `conj(C, not(C)) = conj(C, not(C))`,
115 which doesn't tell you anything. The "implication" step really does
116 pull an arbitrary value out of the air, of the form `conj(C, not(C))`,
117 which gets folded, spindled, and mutilated, and shown to be equal to
118 `conj(A, not(A))`.