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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(add-var-name "x" "y" (py "alpha"))
(add-predconst-name "Q" (make-arity (py "alpha")))
(set-goal (pf "(all y.((Q y -> F) -> F) -> Q y) ->
exca x.Q x -> all y Q y"))
; Automated proof search for minimal quantifier logic (Miller)
(search)
(dp)
(dpe)
(lambda (u2)
(lambda (u3)
((u3 x) (lambda (u4)
(lambda (y)
((u2 y) (lambda (u5)
((u3 y) (lambda (u8)
(lambda (y17)
((u2 y17) (lambda (u9)
(u5 u8)))))))))))))>
(dp)
; ....all x.(Q x -> all y Q y) -> F by assumption Hyp3
; ....x
; ...(Q x -> all y Q y) -> F by all elim
; .......all y.((Q y -> F) -> F) -> Q y by assumption Hyp2
; .......y
; ......((Q y -> F) -> F) -> Q y by all elim
; .........all x.(Q x -> all y Q y) -> F by assumption Hyp3
; .........y
; ........(Q y -> all y Q y) -> F by all elim
; ............all y.((Q y -> F) -> F) -> Q y by assumption Hyp2
; ............y17
; ...........((Q y17 -> F) -> F) -> Q y17 by all elim
; .............Q y -> F by assumption Hyp5
; .............Q y by assumption Hyp8
; ............F by imp elim
; ...........(Q y17 -> F) -> F by imp intro Hyp9
; ..........Q y17 by imp elim
; .........all y17 Q y17 by all intro
; ........Q y -> all y17 Q y17 by imp intro Hyp8
; .......F by imp elim
; ......(Q y -> F) -> F by imp intro Hyp5
; .....Q y by imp elim
; ....all y Q y by all intro
; ...Q x -> all y Q y by imp intro Hyp4
; ..F by imp elim
; .exca x.Q x -> all y Q y by imp intro Hyp3
; (all y.((Q y -> F) -> F) -> Q y) -> exca x.Q x -> all y Q y by imp intro Hyp2
(dpe)
; (lambda (u2)
; (lambda (u3)
; ((u3 x) (lambda (u4)
; (lambda (y)
; ((u2 y) (lambda (u5)
; ((u3 y) (lambda (u8)
; (lambda (y17)
; ((u2 y17) (lambda (u9)
; (u5 u8)))))))))))))
(set-goal (pf "exca x.Q x -> all y Q y"))
(assume 1)
(use 1 (pt "x"))
(assume 2 "y")
(use "Stab")
(assume 3)
(use 1 (pt "y"))
(assume 4)
(use "Efq")
(use-with 3 4)
(dp)
; ...all x.(Q x -> all y Q y) -> F by assumption Hyp0
; ...x
; ..(Q x -> all y Q y) -> F by all elim
; ......all y.((Q y -> F) -> F) -> Q y by global assumption Stab-Log
; ......y
; .....((Q y -> F) -> F) -> Q y by all elim
; ........all x.(Q x -> all y Q y) -> F by assumption Hyp0
; ........y
; .......(Q y -> all y Q y) -> F by all elim
; .........F -> all y Q y by global assumption Efq-Log
; ..........Q y -> F by assumption Hyp2
; ..........Q y by assumption Hyp3
; .........F by imp elim
; ........all y Q y by imp elim
; .......Q y -> all y Q y by imp intro Hyp3
; ......F by imp elim
; .....(Q y -> F) -> F by imp intro Hyp2
; ....Q y by imp elim
; ...all y Q y by all intro
; ..Q x -> all y Q y by imp intro Hyp1
; .F by imp elim
; excl x.Q x -> all y Q y by imp intro Hyp0
|
