-
Notifications
You must be signed in to change notification settings - Fork 1
/
propositional-algebra.eqthy.md
86 lines (60 loc) · 4.03 KB
/
propositional-algebra.eqthy.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
Propositional Algebra
=====================
This is one possible formulation of propositional algebra in Eqthy. For some background,
see Section II of [An Algebraic Introduction to Mathematical Logic][] (Barnes and Mack, 1975)
but note that, while this follows the general ideas there, it might not follow them very closely.
`th(X, ...)` indicates that X is in the list of theorems. There may be more theorems
in the ..., i.e. it is like a cons list. `e` indicates the empty set of theorems.
The order that the theorems appear in the list does not matter.
axiom (#th-assoc) th(X, th(Y, Z)) = th(th(X, Y), Z)
axiom (#th-comm) th(X, th(Y, Z)) = th(Y, th(X, Z))
The logic system is a Hilbert-style system, with three axioms.
In Barnes and Mack, the axioms are given "semantically", using set comprehensions:
> A1 = {p => (q => p) | p, q elem P(X)}
> A2 = {(p => (q => r)) => ((p => q) => (p => r)) | p, q, r elem P(X)}
> A3 = {~~p => p | p elem P(X)}
We model this by saying that any set of theorems T is equal to T with any of these
extra axiomatic statements added to it.
axiom (#A1) th(X, e) = th(X, th(impl(P, impl(Q, P)), e))
axiom (#A2) th(X, e) = th(X, th(impl(impl(P, impl(Q, R)), impl(impl(P, Q), impl(P, R))), e))
axiom (#A3) th(X, e) = th(X, th(impl(not(not(P)), P), e))
In addition, we have modus ponens ("from p and p => q, deduce q"):
axiom (#MP) th(P, th(impl(P, Q), e)) = th(Q, e)
I believe this is all we need to make this work. So, let's pick a simple proof and write it up
and see if the `eqthy` checker can confirm it. Example 4.5 on page 16 of Barnes and Mack:
> |- p => p
We write this in equational logic by saying that any set of theorems is equal to a
set of theorems which contains this theorem.
theorem
th(X, e) = th(X, th(impl(P, P), e))
The proof given in the book is
> p1 = p => ((p => p) => p) [by #axiom-1]
> p2 = (p => ((p => p) => p)) => ((p => (p => p)) => (p=>p)) [by #axiom-2]
> p3 = (p => (p => p)) => (p => p) [p2 = p1 => p3]
> p4 = p => (p => p) [by #axiom-1]
> p5 = p => p [p3 = p4 => p5]
And now we... mechanically translate that...
proof
th(X, e) = th(X, e)
th(X, e) = th(X, th(impl(P, impl(Q, P)), e)) [by #A1]
th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)), e)) [by substitution of impl(P, P) into Q]
th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
th(impl(impl(P, impl(Q, R)), impl(impl(P, Q), impl(P, R))), e))) [by #A2]
th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
th(impl(impl(P, impl(impl(P, P), R)), impl(impl(P, impl(P, P)), impl(P, R))), e)))
[by substitution of impl(P, P) into Q]
th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))), e)))
[by substitution of P into R]
th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))), e)))
[by substitution of P into R]
th(X, e) = th(X, th(impl(impl(P, impl(P, P)), impl(P, P)), e)) [by #MP]
th(X, e) = th(X, th(impl(impl(P, impl(P, P)), impl(P, P)), th(impl(P, impl(Q, P)), e))) [by #A1]
th(X, e) = th(X, th(impl(impl(P, impl(P, P)), impl(P, P)), th(impl(P, impl(P, P)), e)))
[by substitution of P into Q]
th(X, e) = th(X, th(impl(P, impl(P, P)), th(impl(impl(P, impl(P, P)), impl(P, P)), e)))
[by #th-comm]
th(X, e) = th(X, th(impl(P, P), e)) [by #MP]
qed
[An Algebraic Introduction to Mathematical Logic]: https://archive.org/details/algebraicintrodu00barn_0