Commit f916b67b446e64e25c233607302492a56da7e078 - Eqthy

remove extraneous theorems Proloy Mishra 1 year, 9 months ago

1 changed file(s) with 52 addition(s) and 10 deletion(s). Raw diff Collapse all Expand all

+52

-10

eg/propositional-algebra.eqthy.md less more

40	40
41	41	Unfortunately, with the machinery that we've got so far, even though we
42	42	only care that the resulting set contains `impl(P, P)`, we show much more than
43		that -- we show all the intermediate results in getting there.
	43	that -- we show all the intermediate results in getting there. So, we have to work backwards -- removing the inetermediate results using the same axioms used to add them -- for all the theorems except the desired theorem (`impl(P, P)`).
44	44
45	45	theorem
46		th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
47		th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))),
48		th(impl(P, P),
49		th(impl(P, impl(P, P)),
50		th(impl(impl(P, impl(P, P)), impl(P, P)), e))))))
	46	th(X, e) = th(X, th(impl(P, P), e))
51	47
52	48	The proof given in the book is
53	49

70	66	th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
71	67	th(impl(impl(P, impl(impl(P, P), R)), impl(impl(P, impl(P, P)), impl(P, R))), e)))
72	68	[by substitution of impl(P, P) into Q]
73
74		th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
75		th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))), e)))
76		[by substitution of P into R]
77	69
78	70	th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
79	71	th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))), e)))

118	110	th(impl(P, impl(P, P)),
119	111	th(impl(impl(P, impl(P, P)), impl(P, P)), e))))))
120	112	[by #MP]
	113
	114	th(X, e) = th(X, th(impl(P, impl(impl(P, P), P)),
	115	th(impl(P, P),
	116	th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))),
	117	th(impl(P, impl(P, P)),
	118	th(impl(impl(P, impl(P, P)), impl(P, P)), e))))))
	119	[by #th-comm]
	120
	121	th(X, e) = th(X, th(impl(P, P),
	122	th(impl(P, impl(impl(P, P), P)),
	123	th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))),
	124	th(impl(P, impl(P, P)),
	125	th(impl(impl(P, impl(P, P)), impl(P, P)), e))))))
	126	[by #th-comm]
	127
	128	th(X, e) = th(X, th(impl(P, P),
	129	th(impl(P, impl(impl(P, P), P)),
	130	th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))),
	131	th(impl(impl(P, impl(P, P)), impl(P, P)),
	132	th(impl(P, impl(P, P)), e))))))
	133	[by #th-comm]
	134
	135	th(X, e) = th(X, th(impl(P, P),
	136	th(impl(P, impl(impl(P, P), P)),
	137	th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))),
	138	th(impl(impl(P, impl(P, P)), impl(P, P)), e)))))
	139	[by #A1]
	140
	141	th(X, e) = th(X, th(impl(P, P),
	142	th(impl(P, impl(impl(P, P), P)),
	143	th(impl(impl(P, impl(P, P)), impl(P, P)),
	144	th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))), e)))))
	145	[by #th-comm]
	146
	147	th(X, e) = th(X, th(impl(P, P),
	148	th(impl(impl(P, impl(P, P)), impl(P, P)),
	149	th(impl(P, impl(impl(P, P), P)),
	150	th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))), e)))))
	151	[by #th-comm]
	152
	153	th(X, e) = th(X, th(impl(P, P),
	154	th(impl(P, impl(impl(P, P), P)),
	155	th(impl(impl(P, impl(impl(P, P), P)), impl(impl(P, impl(P, P)), impl(P, P))), e))))
	156	[by #MP]
	157
	158	th(X, e) = th(X, th(impl(P, P),
	159	th(impl(P, impl(impl(P, P), P)), e)))
	160	[by #A2]
	161
	162	th(X, e) = th(X, th(impl(P, P), e)) [by #A1]
121	163	qed
122	164
123	165	[An Algebraic Introduction to Mathematical Logic]: https://archive.org/details/algebraicintrodu00barn_0