File: quant2.scm

package info (click to toggle)
minlog 4.0.99.20100221-6
  • links: PTS
  • area: main
  • in suites: buster, stretch
  • size: 7,060 kB
  • ctags: 4,293
  • sloc: lisp: 112,614; makefile: 257; sh: 11
file content (61 lines) | stat: -rw-r--r-- 604 bytes parent folder | download | duplicates (5) 
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
 
(add-var-name "x" (py "alpha"))
(add-predconst-name "Q" (make-arity (py "alpha")))
(add-predconst-name "P" (make-arity))

(set-goal (pf "(ex x Q x -> P) -> all x.Q x -> P"))







































(assume 1 "x" 2)
(use 1)
(ex-intro (pt "x"))
(use 2)

(dp)

; ....ex x Q x -> P by assumption Hyp0
; ......all x5.Q x5 -> ex x5 Q x5 by axiom Ex-Intro
; ......x
; .....Q x -> ex x5 Q x5 by all elim
; .....Q x by assumption Hyp1
; ....ex x5 Q x5 by imp elim
; ...P by imp elim
; ..Q x -> P by imp intro Hyp1
; .all x.Q x -> P by all intro
; (ex x Q x -> P) -> all x.Q x -> P by imp intro Hyp0