数理逻辑的规则与定理

1、一、命题逻辑推理规则：1. A1，A2 .An Ai (i=1,2,.,n) （Î）（包含律）2. 如果D(D¹Æ)且DA，则 A（）（传递律）3. 如果A，则，D A（0）（增加前提律）4. 如果，AB，B，则 A（）（反证律）5. A®B，AB（®-）（®消去律）6. 如果，A B，则 A®B（®+）（®引入律）7. ABA，B（-）（消去律）8. A，BAB（+）（引入律）9. 如果,A C且,BC，则,ABC（-）（消去律）10. AAB，BA（+）（引入律）11. A«B，AB 以及

2、A«B，BA（«-）（«消去律）12. 如果，AB且，BA，则A«B（«+）（«引入律）二、谓词逻辑推理规则：13. "xA(x)A(a)（"-）（"消去律）14. 如果 A(a) 且a不在中出现，则 "xA(x)（"+）（"引入律）15. ,A(a) B 且a不在和B中出现，则,$xA(x) B（$-）（"消去律）16. A(a) $xA(x),A(x)是由A(a)中a的部分出现替换为x而得 ($+)三、斜形证明：1. A1 (前提或假设) 2. A2 (前提或假

3、设) 3. A3 (前提或假设) 4. B1 (A1,A2,A3 B1)5. B2 (A1,A2,A3 B2)6. B3 (A1,A2 B3)7. B4 (A1,A2 B4)8. B5 (A1 B5)四、命题逻辑的定理：1. A A2. A B®A（肯定后件律）3. A®B，B®C A®C（®传递律）4. A®（B®C），A®B A®C5. A，A B（矛盾推出一切）6. A A®B（否定前件律）7. A A®B8. AA9. 如果，A B，B，则 A（+）（归缪律）10. A

4、4;B，B A11. A®B B®A（逆否命题）12. A®B，BA13. A®B B®A14. A®B，B A15. A®B B®A16. A®B，BA17. A®B B®A18. A®AA19. A®A A20. A®B，A®B A21. A®B，A®B B22. (A®B) A, B23. 如果，A C且，B C，则，AB C（-）24. ABBA25. (AB)CA(BC)26. AB (A®B)2

5、7. (AB)A®B28. A®B (AB)29. (A®B)AB30. (AA)31. ABBA32. (AB)CA(BC)33. ABA®B34. A®BAB35. AA36. (AB) AB 摩根律37. (AB) AB38. A(BC)(AB)(AC)39. (AB)C(AC)(BC)40. A(BC)(AB)(AC)41. (AB)C(AC)(BC)42. A®BC(A®B)(A®C)43. A®BC(A®B)(A®C)44. AB®C(A®C)(B

6、74;C)45. AB®C(A®C)(B®C)46. A«B(A®B)(B®A)47. A«A B48. A«B, B«C A«C49. A«BA«B50. A«BA«B 51. A«B(A«B)52. A«B(AB)(AB)53. A«B(AB)(AB)54. (A«B)«CA«(B«C)55. (A«B)(A«B)56. A AB«B57. A

7、®(B®C)B«(B(A«AC)58. A«(B®C)® AC59. (A«B)(C«D) AC«BD五、谓词逻辑的定理：1. ,A(a) B 且a不在和B中出现，则,$xA(x) B (即$-)2. "xA(x)"yA(y)3. $xA(x)$yA(y)4. "x"yA(x,y)"y"xA(x,y)5. $x$yA(x,y)$y$xA(x,y)6. "xA(x) $xA(x)7. $x"yA(x,y) "

8、y$xA(x,y)8. "xA(x)$xA(x)9. $xA(x)"xA(x)10. "xA(x)$xA(x)11. $xA(x)"xA(x)12. "x(A(x)®B(x),"xA(x) "xB(x)13. "x(A(x)®B(x),$xA(x) $xB(x)14. "x(A(x)®B(x),"x(B(x)®C(x) "x(A(x)®C(x)15. A®"xB(x)"x(A®B(x) x

9、7;A16. A®$xB(x)$x(A®B(x) xÏA17. "xA(x)®B$x(A(x)®B) xÏB18. $xA(x)®B"x(A(x)®B) xÏB19. A"xB(x)"x(AB(x) xÏA20. A$xB(x)$x(AB(x) xÏA21. "xA(x)"xB(x)"x(A(x)B(x)22. $x(A(x)B(x) $xA(x)$xB(x)23. $xA(x)$yB(y)$x$y(A(x)B(y)

10、24. "xA(x)"yB(y)"x"y(A(x)B(y)25. "xA(x)$yB(y)"x$y(A(x)B(y)26. $xA(x)"yB(y)$x"y(A(x)B(y)27. A"xB(x)"x(AB(x) xÏA28. A$xB(x)$x(AB(x) xÏA29. "xA(x)"xB(x) "x(A(x)B(x)30. $xA(x)$xB(x) $x(A(x)B(x)31. $xA(x)$yB(y) $x$y(A(x)B(y)32. "xA(x)"yB(y) "x"y(A(x)B(y)33. "xA(x)$yB(y) "x$y(A(x)B(y)34. $xA(x)"yB(y)$x"y(A(x)B(y)35. "x(A(x)«B(x) "xA(x)«"xB(x)36. $x(A(x)«B(x) $xA(x)«$xB(x)37. "x(A(x)«B(x),"x(B(x)«C(x) "x(A(