; 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)))))))))