Checkpoint propositional algebra proof (take different tack on MP.)
Chris Pressey
2 years ago
| 14 | 14 | axiom (#th-comm) th(X, Y) = th(Y, X) |
| 15 | 15 | |
| 16 | 16 | The logic system is a Hilbert-style system. There are three statements that are axioms. |
| 17 | In the book, they are given "semantically", using set comprehensions. | |
| 18 | ||
| 19 | > A1 = {p => (q => p) | p, q elem P(X)} | |
| 20 | > A2 = {(p => (q => r)) => ((p => q) => (p => r)) | p, q, r elem P(X)} | |
| 21 | > A3 = {~~p => p | p elem P(X)} | |
| 22 | ||
| 17 | 23 | We model this by saying that any set of theorems T is equal to T with any of these |
| 18 | 24 | extra axiomatic statements added to it. |
| 19 | 25 | |
| 21 | 27 | axiom (#A2) th(X, e) = th(X, th(impl(impl(P, impl(Q, R)), impl(impl(P, Q), impl(P, R)), e))) |
| 22 | 28 | axiom (#A3) th(X, e) = th(X, th(impl(not(not(P)), P), e)) |
| 23 | 29 | |
| 24 | In addition, we have modus ponens. | |
| 30 | In addition, we have modus ponens ("from p and p => q, deduce q"): | |
| 25 | 31 | |
| 26 | axiom (#MP) th(P, th(impl(P, Q), e)) = th(Q, th(P, th(impl(P, Q), e))) | |
| 32 | axiom (#MP) th(P, th(impl(P, Q), e)) = th(Q, e) | |
| 27 | 33 | |
| 28 | 34 | I believe this should work. So, let's pick a simple proof and write it up and see if |
| 29 | 35 | the `eqthy` checker can confirm it. Example 4.5 on page 16 of Barnes and Mack: |
| 49 | 55 | |
| 50 | 56 | proof |
| 51 | 57 | th(X, e) = th(X, e) |
| 52 | th(X, e) = th(X, th(impl(P, impl(Q, P)), e)) [by #A1] | |
| 53 | th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)), e)) [by substitution of impl(P, P) into Q] | |
| 58 | th(X, e) = th(X, th(impl(P, impl(Q, P)), e)) [by #A1] | |
| 59 | th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)), e)) [by substitution of impl(P, P) into Q] | |
| 60 | ||
| 61 | 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] | |
| 64 | ||
| 65 | th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)), | |
| 66 | th(impl(impl(P, impl(impl(P, P), R)), impl(impl(P, impl(P, P)), impl(P, R)), e)))) | |
| 67 | [by substitution of impl(P, P) into Q] | |
| 68 | ||
| 69 | th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)), | |
| 70 | th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P)), e)))) | |
| 71 | [by substitution of P into R] | |
| 72 | ||
| 73 | // th(X, e) = th(X, th(impl(impl(P, impl(P, P)), impl(P, P)), e)) | |
| 74 | // [by #MP] | |
| 54 | 75 | // FIXME TODO |
| 55 | 76 | qed |
| 56 | 77 | |