
1 (* Title: FOL/ex/quant 

2 ID: $Id$ 

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 Copyright 1991 University of Cambridge 

5 

6 FirstOrder Logic: quantifier examples (intuitionistic and classical) 

7 Needs declarations of the theory "thy" and the tactic "tac" 

8 *) 

9 

10 writeln"File FOL/ex/quant."; 

11 

12 goal thy "?p : (ALL x y.P(x,y)) > (ALL y x.P(x,y))"; 

13 by tac; 

14 result(); 

15 

16 

17 goal thy "?p : (EX x y.P(x,y)) > (EX y x.P(x,y))"; 

18 by tac; 

19 result(); 

20 

21 

22 (*Converse is false*) 

23 goal thy "?p : (ALL x.P(x))  (ALL x.Q(x)) > (ALL x. P(x)  Q(x))"; 

24 by tac; 

25 result(); 

26 

27 goal thy "?p : (ALL x. P>Q(x)) <> (P> (ALL x.Q(x)))"; 

28 by tac; 

29 result(); 

30 

31 

32 goal thy "?p : (ALL x.P(x)>Q) <> ((EX x.P(x)) > Q)"; 

33 by tac; 

34 result(); 

35 

36 

37 writeln"Some harder ones"; 

38 

39 goal thy "?p : (EX x. P(x)  Q(x)) <> (EX x.P(x))  (EX x.Q(x))"; 

40 by tac; 

41 result(); 

42 (*6 secs*) 

43 

44 (*Converse is false*) 

45 goal thy "?p : (EX x. P(x)&Q(x)) > (EX x.P(x)) & (EX x.Q(x))"; 

46 by tac; 

47 result(); 

48 

49 

50 writeln"Basic test of quantifier reasoning"; 

51 (*TRUE*) 

52 goal thy "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"; 

53 by tac; 

54 result(); 

55 

56 

57 goal thy "?p : (ALL x. Q(x)) > (EX x. Q(x))"; 

58 by tac; 

59 result(); 

60 

61 

62 writeln"The following should fail, as they are false!"; 

63 

64 goal thy "?p : (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))"; 

65 by tac handle ERROR => writeln"Failed, as expected"; 

66 (*Check that subgoals remain: proof failed.*) 

67 getgoal 1; 

68 

69 goal thy "?p : (EX x. Q(x)) > (ALL x. Q(x))"; 

70 by tac handle ERROR => writeln"Failed, as expected"; 

71 getgoal 1; 

72 

73 goal thy "?p : P(?a) > (ALL x.P(x))"; 

74 by tac handle ERROR => writeln"Failed, as expected"; 

75 (*Check that subgoals remain: proof failed.*) 

76 getgoal 1; 

77 

78 goal thy 

79 "?p : (P(?a) > (ALL x.Q(x))) > (ALL x. P(x) > Q(x))"; 

80 by tac handle ERROR => writeln"Failed, as expected"; 

81 getgoal 1; 

82 

83 

84 writeln"Back to things that are provable..."; 

85 

86 goal thy "?p : (ALL x.P(x)>Q(x)) & (EX x.P(x)) > (EX x.Q(x))"; 

87 by tac; 

88 result(); 

89 

90 

91 (*An example of why exI should be delayed as long as possible*) 

92 goal thy "?p : (P > (EX x.Q(x))) & P > (EX x.Q(x))"; 

93 by tac; 

94 result(); 

95 

96 goal thy "?p : (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)"; 

97 by tac; 

98 (*Verify that no subgoals remain.*) 

99 uresult(); 

100 

101 

102 goal thy "?p : (ALL x. Q(x)) > (EX x. Q(x))"; 

103 by tac; 

104 result(); 

105 

106 

107 writeln"Some slow ones"; 

108 

109 

110 (*Principia Mathematica *11.53 *) 

111 goal thy "?p : (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))"; 

112 by tac; 

113 result(); 

114 (*6 secs*) 

115 

116 (*Principia Mathematica *11.55 *) 

117 goal thy "?p : (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))"; 

118 by tac; 

119 result(); 

120 (*9 secs*) 

121 

122 (*Principia Mathematica *11.61 *) 

123 goal thy "?p : (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))"; 

124 by tac; 

125 result(); 

126 (*3 secs*) 

127 

128 writeln"Reached end of file."; 

129 