git @ Cat's Eye Technologies Eqthy / aab0cde
Factor Group Theory out into its own document. Chris Pressey 1 year, 2 months ago
5 changed file(s) with 35 addition(s) and 21 deletion(s). Raw diff Collapse all Expand all
+4
-0
HISTORY.md less more
3535
3636 * Added a completed proof of De Morgan's Laws for Boolean
3737 algebra, contributed by Proloy Mishra (@pro465).
38 * Added a few other documents, including some basic theorems
39 in Interior Algebra, as well as refactoring some of the
40 existing documents to use the "Requires" facility to build
41 upon other documents.
3842 * Arranged the licensing information in accordance with
3943 the REUSE 3.0 convention.
4044
+6
-4
README.md less more
4343 A number of proofs have been written in Eqthy to date. These can be found in
4444 the **[eg/](eg/)** directory. In particular, there are worked-out proofs:
4545
46 * of the [Socks and Shoes](eg/socks-and-shoes.eqthy.md) theorem in group theory;
47 * in [Propositional Algebra](eg/propositional-algebra.eqthy.md);
46 * in [Group Theory](eg/group-theory.eqthy.md), including:
47 * some simple theorems about [the inverse element](eg/group-inverse.eqthy.md);
48 * the [Socks and Shoes](eg/socks-and-shoes.eqthy.md) theorem;
4849 * in [Boolean Algebra](eg/boolean-algebra.eqthy.md), including:
4950 * [De Morgan's laws](eg/boolean-algebra.eqthy.md);
5051 * the [Absorption laws](eg/absorption-laws.md) in an alternate axiomatization;
5152 * some properties of [set difference](eg/set-difference.eqthy.md);
52 * in [Interior Algebra](eg/interior-algebra.eqthy.md) (building on Boolean algebra); and
53 * in [Combinatory Logic](eg/combinatory-logic.eqthy.md),
53 * in [Interior Algebra](eg/interior-algebra.eqthy.md) (building on Boolean algebra);
54 * in [Propositional Algebra](eg/propositional-algebra.eqthy.md);
55 * in [Combinatory Logic](eg/combinatory-logic.eqthy.md);
5456
5557 with hopefully more to come in the future.
5658
+1
-5
eg/group-inverse.eqthy.md less more
1515 So other techniques need to be used when working in
1616 equational logic.
1717
18 axiom (#id-right) mul(A, e) = A
19 axiom (#id-left) mul(e, A) = A
20 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
21 axiom (#inv-right) mul(A, inv(A)) = e
22 axiom (#inv-left) mul(inv(A), A) = e
18 Requires [Group theory](group-theory.eqthy.md).
2319
2420 ### Inverse of Identity is Identity
2521
+23
-0
eg/group-theory.eqthy.md less more
0 Group Theory
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 Equational axioms for Group theory.
10
11 Various other documents require this document.
12
13 Note, we could define only `#id-right` and `#inv-right` as axioms,
14 and derive `#id-left` and `#inv-left` from them; see
15 [Right Inverse for All is Left Inverse](semigroup-right-inverse-is-left.eqthy.md), for instance.
16 But for brevity we'll just define them as axioms here.
17
18 axiom (#id-right) mul(A, e) = A
19 axiom (#id-left) mul(e, A) = A
20 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
21 axiom (#inv-right) mul(A, inv(A)) = e
22 axiom (#inv-left) mul(inv(A), A) = e
+1
-12
eg/socks-and-shoes.eqthy.md less more
1111
1212 Also see [Inverse of Product](https://proofwiki.org/wiki/Inverse_of_Product) on ProofWiki.
1313
14 First, the group axioms. Note, we could define only `#id-right` and `#inv-right` as axioms,
15 and derive `#id-left` and `#inv-left` from them; see
16 [Right Inverse for All is Left Inverse](semigroup-right-inverse-is-left.eqthy.md), for instance.
17 But for brevity we'll just define them as axioms here.
18
19 axiom (#id-right) mul(A, e) = A
20 axiom (#id-left) mul(e, A) = A
21 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
22 axiom (#inv-right) mul(A, inv(A)) = e
23 axiom (#inv-left) mul(inv(A), A) = e
24
25 Now, the theorem.
14 Requires [Group theory](group-theory.eqthy.md).
2615
2716 theorem (#socks-and-shoes)
2817 inv(mul(A, B)) = mul(inv(B), inv(A))