; Proof that a variant of the Russell class cannot be a set.
; Exercise 12, SS 2010
; 2010-05-25
(load "~/minlog/init.scm")
(add-var-name "x" "y" "z" (py "alpha"))
(add-predconst-name "ee" (make-arity (py "alpha") (py "alpha")))
(add-token
"in"
'pred-infix
(lambda (x y)
((string-and-arity-to-predconst-parse-function
"ee" (make-arity (py "alpha") (py "alpha")))
(- 1) x y)))
(add-predconst-display "ee" 'pred-infix "in")
; We prove that { x | all y(x in y -> y in x -> F) } cannot be a set.
(set-goal
(pf "all z0(
all x(x in z0 -> all y(x in y -> y in x -> F)) ->
all x(all y(x in y -> y in x -> F) -> x in z0) ->
F)"))
(search)
; Proof finished.
(proof-to-expr-with-formulas)
(check-and-display-proof)
; Hand proof
(set-goal
(pf "all z0(
all x(x in z0 -> all y(x in y -> y in x -> F)) ->
all x(all y(x in y -> y in x -> F) -> x in z0) ->
F)"))
(assume "z0" "LR" "RL")
(assert (pf "z0 in z0"))
(use-with "RL" (pt "z0") "?")
(assume "y" "u" "v")
(use-with "LR" (pt "y") "v" (pt "z0") "v" "u")
(assume "w")
(use-with "LR" (pt "z0") "w" (pt "z0") "w" "w")
; Proof finished.
(check-and-display-proof)
; ..........all x(x in z0 -> all y(x in y -> y in x -> F)) by assumption LR226
; ..........z0
; .........z0 in z0 -> all y(z0 in y -> y in z0 -> F) by all elim
; .........z0 in z0 by assumption w233
; ........all y(z0 in y -> y in z0 -> F) by imp elim
; ........z0
; .......z0 in z0 -> z0 in z0 -> F by all elim
; .......z0 in z0 by assumption w233
; ......z0 in z0 -> F by imp elim
; ......z0 in z0 by assumption w233
; .....F by imp elim
; ....z0 in z0 -> F by imp intro w233
; ......all x(all y(x in y -> y in x -> F) -> x in z0) by assumption RL227
; ......z0
; .....all y(z0 in y -> y in z0 -> F) -> z0 in z0 by all elim
; .............all x(x in z0 -> all y(x in y -> y in x -> F)) by assumption LR226
; .............y
; ............y in z0 -> all y168(y in y168 -> y168 in y -> F) by all elim
; ............y in z0 by assumption v232
; ...........all y168(y in y168 -> y168 in y -> F) by imp elim
; ...........z0
; ..........y in z0 -> z0 in y -> F by all elim
; ..........y in z0 by assumption v232
; .........z0 in y -> F by imp elim
; .........z0 in y by assumption u231
; ........F by imp elim
; .......y in z0 -> F by imp intro v232
; ......z0 in y -> y in z0 -> F by imp intro u231
; .....all y(z0 in y -> y in z0 -> F) by all intro
; ....z0 in z0 by imp elim
; ...F by imp elim
; ..all x(all y(x in y -> y in x -> F) -> x in z0) -> F by imp intro RL227
; .all x(x in z0 -> all y(x in y -> y in x -> F)) -> all x(all y(x in y -> y in x -> F) -> x in z0) -> F by imp intro LR226
; all z0(all x(x in z0 -> all y(x in y -> y in x -> F)) -> all x(all y(x in y -> y in x -> F) -> x in z0) -> F) by all intro
(proof-to-expr-with-formulas)
; LR226: all x(x in z0 -> all y(x in y -> y in x -> F))
; RL227: all x(all y(x in y -> y in x -> F) -> x in z0)
; w233: z0 in z0
; u231: z0 in y
; v232: y in z0
(lambda (z0)
(lambda (|LR226|)
(lambda (|RL227|)
((lambda (w233) (((((|LR226| z0) w233) z0) w233) w233))
((|RL227| z0)
(lambda (y)
(lambda (u231)
(lambda (v232) (((((|LR226| y) v232) z0) v232) u231)))))))))