git @ Cat's Eye Technologies Eqthy / c5fa9bd
Finish the Propositional Algebra proof! Such yay, much rejoicing Chris Pressey 2 years ago
2 changed file(s) with 18 addition(s) and 12 deletion(s). Raw diff Collapse all Expand all
+6
-3
README.md less more
3131 tests, see **[doc/Eqthy.md](doc/Eqthy.md)**.
3232
3333 A number of proofs have been written in Eqthy to date. These can be found in
34 the **[eg/](eg/)** directory. In particular, there is a worked-out
35 proof of the [Socks and Shoes](eg/socks-and-shoes.eqthy.md) theorem in
36 group theory, with hopefully more coming soon.
34 the **[eg/](eg/)** directory. In particular, there are worked-out proofs:
35
36 * of the [Socks and Shoes](eg/socks-and-shoes.eqthy.md) theorem in group theory
37 * in [Propositional Algebra](eg/propositional-algebra.md)
38
39 with hopefully more to come in the future.
3740
3841 The Eqthy language is still at an early stage and is subject to change. However,
3942 since the idea is to accumulate a database of proofs which can be built upon,
+12
-9
eg/propositional-algebra.eqthy.md less more
00 Propositional Algebra
11 =====================
2
3 _NOTE: still under development_
42
53 This is a possible formulation of propositional algebra in Eqthy. For some background,
64 see Section II of [An Algebraic Introduction to Mathematical Logic][] (Barnes and Mack, 1975)
3129
3230 axiom (#MP) th(P, th(impl(P, Q), e)) = th(Q, e)
3331
32 (And, for convenience, a reversed version of it. FIXME make this work with #th-comm)
33
34 axiom (#MP-rev) th(impl(P, Q), th(P, e)) = th(Q, e)
35
3436 I believe this should work. So, let's pick a simple proof and write it up and see if
3537 the `eqthy` checker can confirm it. Example 4.5 on page 16 of Barnes and Mack:
3638
4042 set of theorems which contains this theorem.
4143
4244 theorem
43 // th(X, e) = th(X, th(impl(P, P), e))
44 th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)), e))
45 th(X, e) = th(X, th(impl(P, P), e))
4546
4647 The proof given in the book is
4748
5960 th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)), e)) [by substitution of impl(P, P) into Q]
6061
6162 th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
62 th(impl(impl(P, impl(Q, R)), impl(impl(P, Q), impl(P, R))), e)))
63 [by #A2]
63 th(impl(impl(P, impl(Q, R)), impl(impl(P, Q), impl(P, R))), e))) [by #A2]
6464
6565 th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
6666 th(impl(impl(P, impl(impl(P, P), R)), impl(impl(P, impl(P, P)), impl(P, R))), e)))
7474 th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))), e)))
7575 [by substitution of P into R]
7676
77 th(X, e) = th(X, th(impl(impl(P, impl(P, P)), impl(P, P)), e))
78 [by #MP]
79 // FIXME TODO
77 th(X, e) = th(X, th(impl(impl(P, impl(P, P)), impl(P, P)), e)) [by #MP]
78
79 th(X, e) = th(X, th(impl(impl(P, impl(P, P)), impl(P, P)), th(impl(P, impl(Q, P)), e))) [by #A1]
80 th(X, e) = th(X, th(impl(impl(P, impl(P, P)), impl(P, P)), th(impl(P, impl(P, P)), e)))
81 [by substitution of P into Q]
82 th(X, e) = th(X, th(impl(P, P), e)) [by #MP-rev]
8083 qed
8184
8285 [An Algebraic Introduction to Mathematical Logic]: https://archive.org/details/algebraicintrodu00barn_0